---

Step * 1 of Lemma countable-nsub-family

.....assertion..... 
1. B : ℕ ⟶ ℕ+
2. ∃f:ℕ ⟶ (ℕ × ℕ). Surj(ℕ;ℕ × ℕ;f)
⊢ ∃g:(ℕ × ℕ) ⟶ (i:ℕ × ℕB[i]). Surj(ℕ × ℕ;i:ℕ × ℕB[i];g)
BY
{ Assert ⌜∀i:ℕ. ∃g:ℕ ⟶ ℕB[i]. Surj(ℕ;ℕB[i];g)⌝⋅ }

1
.....assertion..... 
1. B : ℕ ⟶ ℕ+
2. ∃f:ℕ ⟶ (ℕ × ℕ). Surj(ℕ;ℕ × ℕ;f)
⊢ ∀i:ℕ. ∃g:ℕ ⟶ ℕB[i]. Surj(ℕ;ℕB[i];g)

2
1. B : ℕ ⟶ ℕ+
2. ∃f:ℕ ⟶ (ℕ × ℕ). Surj(ℕ;ℕ × ℕ;f)
3. ∀i:ℕ. ∃g:ℕ ⟶ ℕB[i]. Surj(ℕ;ℕB[i];g)
⊢ ∃g:(ℕ × ℕ) ⟶ (i:ℕ × ℕB[i]). Surj(ℕ × ℕ;i:ℕ × ℕB[i];g)

---

Latex:

---

Latex:
.....assertion..... 
1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}  \mtimes{}  \mBbbN{}).  Surj(\mBbbN{};\mBbbN{}  \mtimes{}  \mBbbN{};f)
\mvdash{}  \mexists{}g:(\mBbbN{}  \mtimes{}  \mBbbN{})  {}\mrightarrow{}  (i:\mBbbN{}  \mtimes{}  \mBbbN{}B[i]).  Surj(\mBbbN{}  \mtimes{}  \mBbbN{};i:\mBbbN{}  \mtimes{}  \mBbbN{}B[i];g)


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}i:\mBbbN{}.  \mexists{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].  Surj(\mBbbN{};\mBbbN{}B[i];g)\mkleeneclose{}\mcdot{}

---

Home Index