---

Step * 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))
⊢ a1 ∈ fset-minimals(x,y.f-proper-subset-dec(eq;x;y); s)
BY
{ (BLemma `member-fset-minimals`
   THEN Auto
   THEN (Using [`eq',⌜deq-fset(eq)⌝] (BLemma  `fset-all-iff`)⋅ THEN Auto)
   THEN (D 0 THENA 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. ¬(∃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

---

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))
\mvdash{}  a1  \mmember{}  fset-minimals(x,y.f-proper-subset-dec(eq;x;y);  s)


By

---

Latex:
(BLemma  `member-fset-minimals`
  THEN  Auto
  THEN  (Using  [`eq',\mkleeneopen{}deq-fset(eq)\mkleeneclose{}]  (BLemma    `fset-all-iff`)\mcdot{}  THEN  Auto)
  THEN  (D  0  THENA  Auto))

---

Home Index