---

Step * 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 ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s)
7. xs ∈ fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys); s)
8. xs ⊆ ys@i
9. ¬(xs = ys ∈ fset(T))@i
⊢ False
BY
{ ((RWO "member-fset-minimals" (-4) THENA Auto) THEN (RWO "member-fset-minimals" (-3) THENA 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 ∧ fset-all(s;y1.¬bf-proper-subset-dec(eq;y1;ys))
7. xs ∈ s ∧ fset-all(s;ys.¬bf-proper-subset-dec(eq;ys;xs))
8. xs ⊆ ys@i
9. ¬(xs = ys ∈ fset(T))@i
⊢ 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{}  fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys);  s)
7.  xs  \mmember{}  fset-minimals(xs,ys.f-proper-subset-dec(eq;xs;ys);  s)
8.  xs  \msubseteq{}  ys@i
9.  \mneg{}(xs  =  ys)@i
\mvdash{}  False


By

---

Latex:
((RWO  "member-fset-minimals"  (-4)  THENA  Auto)  THEN  (RWO  "member-fset-minimals"  (-3)  THENA  Auto))

---

Home Index