---

Step * 1 of Lemma second-countable-choice


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]
BY
{ With ⌜λn,s. if (n =z 0) then f 0 0 (λx.⊥) else f (s 0) (n - 1) (λi.(s (i + 1))) fi ⌝ (D 0)⋅ }

1
.....wf..... 
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]
⊢ λn,s. if (n =z 0) then f 0 0 (λx.⊥) else f (s 0) (n - 1) (λi.(s (i + 1))) fi  ∈ n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ X

2
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]
⊢ ∀n:ℕ. R[n;λn,s. if (n =z 0) then f 0 0 (λx.⊥) else f (s 0) (n - 1) (λi.(s (i + 1))) fi _n]

3
.....wf..... 
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]
6. B : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ X
⊢ ∀n:ℕ. R[n;B_n] ∈ ℙ'

---

Latex:

---

Latex:

1.  [X]  :  \mBbbU{}'
2.  [R]  :  \mBbbN{}  {}\mrightarrow{}  (n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  X)  {}\mrightarrow{}  \mBbbP{}'
3.  \mforall{}n:\mBbbN{}.  \mexists{}A:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  X.  R[n;A]
4.  f  :  n:\mBbbN{}  {}\mrightarrow{}  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  X
5.  \mforall{}n:\mBbbN{}.  R[n;f  n]
\mvdash{}  \mexists{}B:n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  X.  \mforall{}n:\mBbbN{}.  R[n;B\_n]


By

---

Latex:
With  \mkleeneopen{}\mlambda{}n,s.  if  (n  =\msubz{}  0)  then  f  0  0  (\mlambda{}x.\mbot{})  else  f  (s  0)  (n  -  1)  (\mlambda{}i.(s  (i  +  1)))  fi  \mkleeneclose{}  (D  0)\mcdot{}

---

Home Index