---

Step * of Lemma axiom-choice-1X-quot

∀X:Type. ∀P:(ℕ ⟶ ℕ) ⟶ X ⟶ ℙ.  ((∀f:ℕ ⟶ ℕ. ⇃(∃m:X. (P f m))) ⇒ ⇃(∃F:(ℕ ⟶ ℕ) ⟶ X. ∀f:ℕ ⟶ ℕ. (P f (F f))))
BY
{ (Auto THEN BLemma `axiom-choice-quot` THEN Auto THEN BLemma `trivial-quotient-true` THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}X:Type.  \mforall{}P:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}.
    ((\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}m:X.  (P  f  m)))  {}\mRightarrow{}  \00D9(\mexists{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  X.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  (P  f  (F  f))))


By

---

Latex:
(Auto  THEN  BLemma  `axiom-choice-quot`  THEN  Auto  THEN  BLemma  `trivial-quotient-true`  THEN  EAuto  1)

---

Home Index