---

Step * of Lemma set-axiom-of-choice-implies-xmiddle

Set-AC ⇒ (∀P:ℙ. ((↓P) ∨ (¬P)))
BY
{ (Auto
   THEN Unfold `set-axiom-of-choice` 1
   THEN (InstHyp [⌜ℕ2⌝;⌜λi.if (i =z 0) then {x:ℕ2| (x = 0 ∈ ℤ) ∨ P}  else {x:ℕ2| (x = 1 ∈ ℤ) ∨ P}  fi ⌝] 1⋅
         THENA (Reduce 0 THEN Auto)
         )) }

1
1. ∀T:Type. ∀S:T ⟶ Type.  ((∀x:T. (S x)) ⇒ (∃f:x:T ⟶ (S x). ∀x,y:T.  (S x ≡ S y ⇒ ((f x) = (f y) ∈ (S x)))))
2. P : ℙ
3. x : ℕ2
⊢ if (x =z 0) then {x:ℕ2| (x = 0 ∈ ℤ) ∨ P}  else {x:ℕ2| (x = 1 ∈ ℤ) ∨ P}  fi 

2
1. ∀T:Type. ∀S:T ⟶ Type.  ((∀x:T. (S x)) ⇒ (∃f:x:T ⟶ (S x). ∀x,y:T.  (S x ≡ S y ⇒ ((f x) = (f y) ∈ (S x)))))
2. P : ℙ
3. ∃f:x:ℕ2 ⟶ ((λi.if (i =z 0) then {x:ℕ2| (x = 0 ∈ ℤ) ∨ P}  else {x:ℕ2| (x = 1 ∈ ℤ) ∨ P}  fi ) x)
    ∀x,y:ℕ2.
      ((λi.if (i =z 0) then {x:ℕ2| (x = 0 ∈ ℤ) ∨ P}  else {x:ℕ2| (x = 1 ∈ ℤ) ∨ P}  fi ) x ≡ (λi.if (i =z 0)
                                                                                              then {x:ℕ2| 
                                                                                                    (x = 0 ∈ ℤ) ∨ P} 
                                                                                              else {x:ℕ2| 
                                                                                                    (x = 1 ∈ ℤ) ∨ P} 
                                                                                              fi ) 
                                                                                          y
      ⇒ ((f x) = (f y) ∈ ((λi.if (i =z 0) then {x:ℕ2| (x = 0 ∈ ℤ) ∨ P}  else {x:ℕ2| (x = 1 ∈ ℤ) ∨ P}  fi ) x)))
⊢ (↓P) ∨ (¬P)

---

Latex:

---

Latex:
Set-AC  {}\mRightarrow{}  (\mforall{}P:\mBbbP{}.  ((\mdownarrow{}P)  \mvee{}  (\mneg{}P)))


By

---

Latex:
(Auto
  THEN  Unfold  `set-axiom-of-choice`  1
  THEN  (InstHyp  [\mkleeneopen{}\mBbbN{}2\mkleeneclose{};\mkleeneopen{}\mlambda{}i.if  (i  =\msubz{}  0)  then  \{x:\mBbbN{}2|  (x  =  0)  \mvee{}  P\}    else  \{x:\mBbbN{}2|  (x  =  1)  \mvee{}  P\}    fi  \mkleeneclose{}]  1\mcdot{}
              THENA  (Reduce  0  THEN  Auto)
              ))

---

Home Index