---

Step * 2 1 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 ⟶ 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)
BY
{ (Assert ⌜∀x:ℕ2. (f x ∈ ℕ2)⌝⋅ THENA 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. 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 ))
5. ∀x:ℕ2. (f x ∈ ℕ2)
⊢ (↓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.  f  :  x:\mBbbN{}2  {}\mrightarrow{}  if  (x  =\msubz{}  0)  then  \{x:\mBbbN{}2|  (x  =  0)  \mvee{}  P\}    else  \{x:\mBbbN{}2|  (x  =  1)  \mvee{}  P\}    fi 
4.  \mforall{}x,y:\mBbbN{}2.
          (if  (x  =\msubz{}  0)  then  \{x:\mBbbN{}2|  (x  =  0)  \mvee{}  P\}    else  \{x:\mBbbN{}2|  (x  =  1)  \mvee{}  P\}    fi    \mequiv{}  if  (y  =\msubz{}  0)
            then  \{x:\mBbbN{}2|  (x  =  0)  \mvee{}  P\} 
            else  \{x:\mBbbN{}2|  (x  =  1)  \mvee{}  P\} 
            fi 
          {}\mRightarrow{}  ((f  x)  =  (f  y)))
\mvdash{}  (\mdownarrow{}P)  \mvee{}  (\mneg{}P)


By

---

Latex:
(Assert  \mkleeneopen{}\mforall{}x:\mBbbN{}2.  (f  x  \mmember{}  \mBbbN{}2)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index