---

Step * 1 of Lemma free-dlwc-1


1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. x : {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} 
5. {} ∈ x
⊢ x = {{}} ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))} 
BY
{ (DVar `x' THEN ExRepD THEN EqTypeCD THEN Auto THEN (RWO "assert-fset-antichain" 5  THENA Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. Cs : T ⟶ fset(fset(T))
4. x : fset(fset(T))
5. ∀xs,ys:fset(T).  (¬xs ⊆≠ ys) supposing (xs ∈ x and ys ∈ x)
6. fset-all(x;a.fset-contains-none(eq;a;x.Cs[x]))
7. {} ∈ x
⊢ x = {{}} ∈ fset(fset(T))

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  Cs  :  T  {}\mrightarrow{}  fset(fset(T))
4.  x  :  \{ac:fset(fset(T))| 
                (\muparrow{}fset-antichain(eq;ac))  \mwedge{}  fset-all(ac;a.fset-contains-none(eq;a;x.Cs[x]))\} 
5.  \{\}  \mmember{}  x
\mvdash{}  x  =  \{\{\}\}


By

---

Latex:
(DVar  `x'  THEN  ExRepD  THEN  EqTypeCD  THEN  Auto  THEN  (RWO  "assert-fset-antichain"  5    THENA  Auto))

---

Home Index