---

Step * 1 2 1 of Lemma countable-nsub-family


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)
BY
{ ((D 0 With ⌜λp.let i,n = p in <i, h i n>⌝  THEN Auto) THEN (D 0 THENA Auto) THEN D -1) }

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)
6. i : ℕ
7. b1 : ℕB[i]
⊢ ∃a:ℕ × ℕ. (((λp.let i,n = p in <i, h i n>) a) = <i, b1> ∈ (i:ℕ × ℕB[i]))

---

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)
4.  h  :  i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i]
5.  \mforall{}i:\mBbbN{}.  Surj(\mBbbN{};\mBbbN{}B[i];h  i)
\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:
((D  0  With  \mkleeneopen{}\mlambda{}p.let  i,n  =  p  in  <i,  h  i  n>\mkleeneclose{}    THEN  Auto)  THEN  (D  0  THENA  Auto)  THEN  D  -1)

---

Home Index