---

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

.....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))
BY
{ (ParallelOp -5 THEN ParallelLast THEN Auto) }

1
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. a1 ∈ s
12. y : fset(T)
13. y ∈ s
14. y ⊆≠ a1
15. z : fset(T)
16. z ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s)
17. z ⊆≠ y
18. z ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s)
⊢ z ⊆≠ a1

---

Latex:

---

Latex:
.....antecedent..... 
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{}  \mneg{}(\mexists{}z:fset(T).  (z  \mmember{}  fset-minimals(x,y.f-proper-subset-dec(eq;x;y);  s)  \mwedge{}  z  \msubseteq{}\mneq{}  y))


By

---

Latex:
(ParallelOp  -5  THEN  ParallelLast  THEN  Auto)

---

Home Index