---

Step * 1 2 of Lemma countable-nsub-family


1. B : ℕ ⟶ ℕ+
2. ∃f:ℕ ⟶ (ℕ × ℕ). Surj(ℕ;ℕ × ℕ;f)
3. ∀i:ℕ. ∃g:ℕ ⟶ ℕB[i]. Surj(ℕ;ℕB[i];g)
⊢ ∃g:(ℕ × ℕ) ⟶ (i:ℕ × ℕB[i]). Surj(ℕ × ℕ;i:ℕ × ℕB[i];g)
BY
{ (Skolemize (-1) `h' THENA Auto) }

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

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}  \mtimes{}  \mBbbN{}).  Surj(\mBbbN{};\mBbbN{}  \mtimes{}  \mBbbN{};f)
3.  \mforall{}i:\mBbbN{}.  \mexists{}g:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].  Surj(\mBbbN{};\mBbbN{}B[i];g)
\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:
(Skolemize  (-1)  `h'  THENA  Auto)

---

Home Index