---

Step * of Lemma axiom-choice-00-quot

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

---

Latex:

---

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


By

---

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

---

Home Index