---

Step * of Lemma axiom-choice-C0

∀P:n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ. ((∀f:ℕ ⟶ 𝔹. ⇃(∃m:ℕ. (P m f))) ⇒ ⇃(∃F:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f:ℕ ⟶ 𝔹. (P (F f) f)))
BY
{ Auto }

1
1. P : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ@i'
2. ∀f:ℕ ⟶ 𝔹. ⇃(∃m:ℕ. (P m f))@i
⊢ ⇃(∃F:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f:ℕ ⟶ 𝔹. (P (F f) f))

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index