---

Step * 1 1 1 1 of Lemma choicef_wf


1. xm : ∀P:ℙ. (P ∨ (¬P))
2. T : Type
3. P : T ⟶ ℙ
4. ∃a:T. P[a]
5. y : {y:T| P[y]}  ⟶ False
6. (xm {y:T| P[y]} ) = (inr y ) ∈ ({y:T| P[y]}  ∨ (¬{y:T| P[y]} ))
⊢ {y:T| P[y]} 
BY
{ ((D 4 THEN With ⌜a⌝ (D 0)) THEN Auto) }

---

Latex:

---

Latex:

1.  xm  :  \mforall{}P:\mBbbP{}.  (P  \mvee{}  (\mneg{}P))
2.  T  :  Type
3.  P  :  T  {}\mrightarrow{}  \mBbbP{}
4.  \mexists{}a:T.  P[a]
5.  y  :  \{y:T|  P[y]\}    {}\mrightarrow{}  False
6.  (xm  \{y:T|  P[y]\}  )  =  (inr  y  )
\mvdash{}  \{y:T|  P[y]\} 


By

---

Latex:
((D  4  THEN  With  \mkleeneopen{}a\mkleeneclose{}  (D  0))  THEN  Auto)

---

Home Index