---

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

∀B:{B:Type| B ⊆r Base} . ∀X:Type. ∀P:B ⟶ X ⟶ ℙ.  ((∀n:B. ⇃(∃m:X. (P n m))) ⇒ ⇃(∃f:B ⟶ X. ∀n:B. (P n (f n))))
BY
{ (Auto THEN BLemma `axiom-choice-quot` THEN Auto THEN BLemma `trivial-quotient-true` THEN EAuto 1) }

---

Latex:

---

Latex:
\mforall{}B:\{B:Type|  B  \msubseteq{}r  Base\}  .  \mforall{}X:Type.  \mforall{}P:B  {}\mrightarrow{}  X  {}\mrightarrow{}  \mBbbP{}.
    ((\mforall{}n:B.  \00D9(\mexists{}m:X.  (P  n  m)))  {}\mRightarrow{}  \00D9(\mexists{}f:B  {}\mrightarrow{}  X.  \mforall{}n:B.  (P  n  (f  n))))


By

---

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

---

Home Index