---

Step * 1 1 1 1 of Lemma fset-minimals-antichain


1. T : Type
2. eq : EqDecider(T)@i
3. s : fset(fset(T))@i
4. xs : fset(T)@i
5. ys : fset(T)@i
6. ys ∈ s
7. ∀[y1:fset(T)]. ↑¬bf-proper-subset-dec(eq;y1;ys) supposing y1 ∈ s
8. xs ∈ s
9. fset-all(s;ys.¬bf-proper-subset-dec(eq;ys;xs))
10. xs ⊆ ys@i
11. ¬(xs = ys ∈ fset(T))@i
12. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))].  uiff(fset-all(s;x.P[x]);∀[x:fset(T)]. ↑P[x] supposing x ∈ s)
⊢ False
BY
{ (InstHyp [⌜xs⌝] (-6)⋅ THEN Auto) }

1
1. T : Type
2. eq : EqDecider(T)@i
3. s : fset(fset(T))@i
4. xs : fset(T)@i
5. ys : fset(T)@i
6. ys ∈ s
7. ∀[y1:fset(T)]. ↑¬bf-proper-subset-dec(eq;y1;ys) supposing y1 ∈ s
8. xs ∈ s
9. fset-all(s;ys.¬bf-proper-subset-dec(eq;ys;xs))
10. xs ⊆ ys@i
11. ¬(xs = ys ∈ fset(T))@i
12. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))].  uiff(fset-all(s;x.P[x]);∀[x:fset(T)]. ↑P[x] supposing x ∈ s)
13. ↑¬bf-proper-subset-dec(eq;xs;ys)
⊢ False

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)@i
3.  s  :  fset(fset(T))@i
4.  xs  :  fset(T)@i
5.  ys  :  fset(T)@i
6.  ys  \mmember{}  s
7.  \mforall{}[y1:fset(T)].  \muparrow{}\mneg{}\msubb{}f-proper-subset-dec(eq;y1;ys)  supposing  y1  \mmember{}  s
8.  xs  \mmember{}  s
9.  fset-all(s;ys.\mneg{}\msubb{}f-proper-subset-dec(eq;ys;xs))
10.  xs  \msubseteq{}  ys@i
11.  \mneg{}(xs  =  ys)@i
12.  \mforall{}[P:fset(T)  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[s:fset(fset(T))].
            uiff(fset-all(s;x.P[x]);\mforall{}[x:fset(T)].  \muparrow{}P[x]  supposing  x  \mmember{}  s)
\mvdash{}  False


By

---

Latex:
(InstHyp  [\mkleeneopen{}xs\mkleeneclose{}]  (-6)\mcdot{}  THEN  Auto)

---

Home Index