---

Step * 1 of Lemma general-fan-theorem-troelstra-sq


1. X : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ@i'
2. ∀f:ℕ ⟶ 𝔹. ⇃(∃n:ℕ. X[n;f])@i
⊢ ⇃(∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])
BY
{ (FLemma `axiom-choice-C0` [-1] THENA Auto) }

1
1. X : n:ℕ ⟶ (ℕn ⟶ 𝔹) ⟶ ℙ@i'
2. ∀f:ℕ ⟶ 𝔹. ⇃(∃n:ℕ. X[n;f])@i
3. ⇃(∃F:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f:ℕ ⟶ 𝔹. (X (F f) f))
⊢ ⇃(∃k:ℕ. ∀f:ℕ ⟶ 𝔹. ∃n:ℕk. X[n;f])

---

Latex:

---

Latex:

1.  X  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbP{}@i'
2.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \00D9(\mexists{}n:\mBbbN{}.  X[n;f])@i
\mvdash{}  \00D9(\mexists{}k:\mBbbN{}.  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.  \mexists{}n:\mBbbN{}k.  X[n;f])


By

---

Latex:
(FLemma  `axiom-choice-C0`  [-1]  THENA  Auto)

---

Home Index