---

Step * of Lemma implies-member-fset-minimals

∀[T:Type]
  ∀eq:EqDecider(T). ∀s:fset(fset(T)). ∀a:fset(T).
    (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))
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN (Assert ⌜∀n:ℕ. ∀a:fset(T).
                   (||a|| < n
                   ⇒ 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))⌝⋅
   THENM (Auto THEN InstHyp [⌜||a|| + 1⌝;⌜a⌝] 5⋅ THEN Auto)
   )
   THEN InductionOnNat
   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. ¬(∃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)

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}s:fset(fset(T)).  \mforall{}a:fset(T).
        (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))


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  (Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}a:fset(T).
                                  (||a||  <  n
                                  {}\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))\mkleeneclose{}\mcdot{}
  THENM  (Auto  THEN  InstHyp  [\mkleeneopen{}||a||  +  1\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  5\mcdot{}  THEN  Auto)
  )
  THEN  InductionOnNat
  THEN  Auto')

---

Home Index