Step
*
2
of Lemma
set-axiom-of-choice-implies-xmiddle
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)
BY
{ (Reduce -1 THEN ExRepD) }
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. f : x:ℕ2 ⟶ if (x =z 0) then {x:ℕ2| (x = 0 ∈ ℤ) ∨ P} else {x:ℕ2| (x = 1 ∈ ℤ) ∨ P} fi
4. ∀x,y:ℕ2.
(if (x =z 0) then {x:ℕ2| (x = 0 ∈ ℤ) ∨ P} else {x:ℕ2| (x = 1 ∈ ℤ) ∨ P} fi ≡ if (y =z 0)
then {x:ℕ2| (x = 0 ∈ ℤ) ∨ P}
else {x:ℕ2| (x = 1 ∈ ℤ) ∨ P}
fi
⇒ ((f x) = (f y) ∈ if (x =z 0) then {x:ℕ2| (x = 0 ∈ ℤ) ∨ P} else {x:ℕ2| (x = 1 ∈ ℤ) ∨ P} fi ))
⊢ (↓P) ∨ (¬P)
Latex:
Latex:
1. \mforall{}T:Type. \mforall{}S:T {}\mrightarrow{} Type.
((\mforall{}x:T. (S x)) {}\mRightarrow{} (\mexists{}f:x:T {}\mrightarrow{} (S x). \mforall{}x,y:T. (S x \mequiv{} S y {}\mRightarrow{} ((f x) = (f y)))))
2. P : \mBbbP{}
3. \mexists{}f:x:\mBbbN{}2 {}\mrightarrow{} ((\mlambda{}i.if (i =\msubz{} 0) then \{x:\mBbbN{}2| (x = 0) \mvee{} P\} else \{x:\mBbbN{}2| (x = 1) \mvee{} P\} fi ) x)
\mforall{}x,y:\mBbbN{}2.
((\mlambda{}i.if (i =\msubz{} 0) then \{x:\mBbbN{}2| (x = 0) \mvee{} P\} else \{x:\mBbbN{}2| (x = 1) \mvee{} P\} fi ) x \mequiv{} (\mlambda{}i.if (i =\msubz{} 0)
then \{x:\mBbbN{}2|
(x = 0)
\mvee{} P\}
else \{x:\mBbbN{}2|
(x = 1)
\mvee{} P\}
fi )
y
{}\mRightarrow{} ((f x) = (f y)))
\mvdash{} (\mdownarrow{}P) \mvee{} (\mneg{}P)
By
Latex:
(Reduce -1 THEN ExRepD)
Home
Index