---

Step * of Lemma second-countable-choice

∀[X:𝕌']. ∀[R:ℕ ⟶ (n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ X) ⟶ ℙ'].
  ((∀n:ℕ. ∃A:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ X. R[n;A]) ⇒ (∃B:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ X. ∀n:ℕ. R[n;B_n]))
BY
{ (Auto THEN (Skolemize (-1) `f' THENA Auto)) }

1
1. [X] : 𝕌'
2. [R] : ℕ ⟶ (n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ X) ⟶ ℙ'
3. ∀n:ℕ. ∃A:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ X. R[n;A]
4. f : n:ℕ ⟶ n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ X
5. ∀n:ℕ. R[n;f n]
⊢ ∃B:n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ X. ∀n:ℕ. R[n;B_n]

---

Latex:

---

Latex:
\mforall{}[X:\mBbbU{}'].  \mforall{}[R:\mBbbN{}  {}\mrightarrow{}  (n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}'].
    ((\mforall{}n:\mBbbN{}.  \mexists{}A:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  X.  R[n;A])  {}\mRightarrow{}  (\mexists{}B:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  X.  \mforall{}n:\mBbbN{}.  R[n;B\_n]))


By

---

Latex:
(Auto  THEN  (Skolemize  (-1)  `f'  THENA  Auto))

---

Home Index