---

Step * 1 of Lemma constrained-antichain-lattice_wf

.....wf..... 
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. ∀x,y:fset(T).  (y ⊆ x ⇒ (↑(P x)) ⇒ (↑(P y)))
5. ↑(P {})
⊢ {{}} ∈ {ac:fset(fset(T))| (↑fset-antichain(eq;ac)) ∧ fset-all(ac;x.P x)} 
BY
{ ((Assert {{}} ∈ fset(fset(T)) BY
          Auto)
   THEN MemTypeCD
   THEN Auto
   THEN (InstLemma `fset-all-iff` [⌜fset(T)⌝;⌜deq-fset(eq)⌝]⋅ THENA Auto)
   THEN BHyp -1
   THEN Auto
   THEN (RWO "member-fset-singleton" (-1) THENA Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. P : fset(T) ⟶ 𝔹
4. ∀x,y:fset(T).  (y ⊆ x ⇒ (↑(P x)) ⇒ (↑(P y)))
5. ↑(P {})
6. {{}} ∈ fset(fset(T))
7. ↑fset-antichain(eq;{{}})
8. ∀[P:fset(T) ⟶ 𝔹]. ∀[s:fset(fset(T))].  uiff(fset-all(s;x.P[x]);∀[x:fset(T)]. ↑P[x] supposing x ∈ s)
9. x : fset(T)
10. x = {} ∈ fset(T)
⊢ ↑(P x)

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  P  :  fset(T)  {}\mrightarrow{}  \mBbbB{}
4.  \mforall{}x,y:fset(T).    (y  \msubseteq{}  x  {}\mRightarrow{}  (\muparrow{}(P  x))  {}\mRightarrow{}  (\muparrow{}(P  y)))
5.  \muparrow{}(P  \{\})
\mvdash{}  \{\{\}\}  \mmember{}  \{ac:fset(fset(T))|  (\muparrow{}fset-antichain(eq;ac))  \mwedge{}  fset-all(ac;x.P  x)\} 


By

---

Latex:
((Assert  \{\{\}\}  \mmember{}  fset(fset(T))  BY
                Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  (InstLemma  `fset-all-iff`  [\mkleeneopen{}fset(T)\mkleeneclose{};\mkleeneopen{}deq-fset(eq)\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  BHyp  -1
  THEN  Auto
  THEN  (RWO  "member-fset-singleton"  (-1)  THENA  Auto))

---

Home Index