---

Step * 1 1 of Lemma implies-member-fset-minimals


1. T : Type
2. eq : EqDecider(T)
3. s : fset(fset(T))
4. a : fset(T)
5. n : ℤ
6. 0 < n
7. ∀a:fset(T)
     (||a|| < n - 1
     ⇒ a ∈ s
     ⇒ (¬(∃z:fset(T). (z ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s) ∧ z ⊆≠ a)))
     ⇒ a ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s))
8. a1 : fset(T)
9. ||a1|| < n
10. a1 ∈ s
11. ¬(∃z:fset(T). (z ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s) ∧ z ⊆≠ a1))
12. a1 ∈ s
13. y : fset(T)
14. y ∈ s
15. y ⊆≠ a1
⊢ False
BY
{ (InstHyp [⌜y⌝] 7⋅ THEN Auto) }

1
.....antecedent..... 
1. T : Type
2. eq : EqDecider(T)
3. s : fset(fset(T))
4. a : fset(T)
5. n : ℤ
6. 0 < n
7. ∀a:fset(T)
     (||a|| < n - 1
     ⇒ a ∈ s
     ⇒ (¬(∃z:fset(T). (z ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s) ∧ z ⊆≠ a)))
     ⇒ a ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s))
8. a1 : fset(T)
9. ||a1|| < n
10. a1 ∈ s
11. ¬(∃z:fset(T). (z ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s) ∧ z ⊆≠ a1))
12. a1 ∈ s
13. y : fset(T)
14. y ∈ s
15. y ⊆≠ a1
⊢ ||y|| < n - 1

2
.....antecedent..... 
1. T : Type
2. eq : EqDecider(T)
3. s : fset(fset(T))
4. a : fset(T)
5. n : ℤ
6. 0 < n
7. ∀a:fset(T)
     (||a|| < n - 1
     ⇒ a ∈ s
     ⇒ (¬(∃z:fset(T). (z ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s) ∧ z ⊆≠ a)))
     ⇒ a ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s))
8. a1 : fset(T)
9. ||a1|| < n
10. a1 ∈ s
11. ¬(∃z:fset(T). (z ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s) ∧ z ⊆≠ a1))
12. a1 ∈ s
13. y : fset(T)
14. y ∈ s
15. y ⊆≠ a1
⊢ ¬(∃z:fset(T). (z ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s) ∧ z ⊆≠ y))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  s  :  fset(fset(T))
4.  a  :  fset(T)
5.  n  :  \mBbbZ{}
6.  0  <  n
7.  \mforall{}a:fset(T)
          (||a||  <  n  -  1
          {}\mRightarrow{}  a  \mmember{}  s
          {}\mRightarrow{}  (\mneg{}(\mexists{}z:fset(T).  (z  \mmember{}  fset-minimals(x,y.f-proper-subset-dec(eq;x;y);  s)  \mwedge{}  z  \msubseteq{}\mneq{}  a)))
          {}\mRightarrow{}  a  \mmember{}  fset-minimals(x,y.f-proper-subset-dec(eq;x;y);  s))
8.  a1  :  fset(T)
9.  ||a1||  <  n
10.  a1  \mmember{}  s
11.  \mneg{}(\mexists{}z:fset(T).  (z  \mmember{}  fset-minimals(x,y.f-proper-subset-dec(eq;x;y);  s)  \mwedge{}  z  \msubseteq{}\mneq{}  a1))
12.  a1  \mmember{}  s
13.  y  :  fset(T)
14.  y  \mmember{}  s
15.  y  \msubseteq{}\mneq{}  a1
\mvdash{}  False


By

---

Latex:
(InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  7\mcdot{}  THEN  Auto)

---

Home Index