---

Step * 1 2 1 of Lemma axiom-choice-C0


1. P : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ@i'
⊢ ⇃(∀f:ℕ ⟶ 𝔹. ∃m:ℕ. (P m f)) ⇒ ⇃(∃F:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f:ℕ ⟶ 𝔹. (P (F f) f))
BY
{ (BLemma `implies-quotient-true` THEN Auto) }

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

---

Latex:

---

Latex:

1.  P  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}@i'
\mvdash{}  \00D9(\mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \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:
(BLemma  `implies-quotient-true`  THEN  Auto)

---

Home Index