---

Step * 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]} 
6. (xm {y:T| P[y]} ) = (inr y ) ∈ ({y:T| P[y]}  ∨ (¬{y:T| P[y]} ))
⊢ "???" ∈ T
BY
{ (D 5 THENA Auto) }

1
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]} 

---

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  :  \mneg{}\{y:T|  P[y]\} 
6.  (xm  \{y:T|  P[y]\}  )  =  (inr  y  )
\mvdash{}  "???"  \mmember{}  T


By

---

Latex:
(D  5  THENA  Auto)

---

Home Index