---

Step * 1 2 1 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)
6. i : ℕ
7. b1 : ℕB[i]
⊢ ∃a:ℕ × ℕ. (((λp.let i,n = p in <i, h i n>) a) = <i, b1> ∈ (i:ℕ × ℕB[i]))
BY
{ (D -3 With ⌜i⌝  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 : ℕ
6. b1 : ℕB[i]
7. Surj(ℕ;ℕB[i];h 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)
6.  i  :  \mBbbN{}
7.  b1  :  \mBbbN{}B[i]
\mvdash{}  \mexists{}a:\mBbbN{}  \mtimes{}  \mBbbN{}.  (((\mlambda{}p.let  i,n  =  p  in  <i,  h  i  n>)  a)  =  <i,  b1>)


By

---

Latex:
(D  -3  With  \mkleeneopen{}i\mkleeneclose{}    THENA  Auto)

---

Home Index