---

Step * 1 2 1 1 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 : ℕ
6. b1 : ℕB[i]
7. ∃a:ℕ. ((h i a) = b1 ∈ ℕB[i])
⊢ ∃a:ℕ × ℕ. (((λp.let i,n = p in <i, h i n>) a) = <i, b1> ∈ (i:ℕ × ℕB[i]))
BY
{ ((D -1 THEN (D 0 With ⌜<i, a>⌝  THENA (Try (D -1) THEN Reduce 0 THEN Auto))) THEN Reduce 0 THEN EqCD THEN Auto) }

---

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.  i  :  \mBbbN{}
6.  b1  :  \mBbbN{}B[i]
7.  \mexists{}a:\mBbbN{}.  ((h  i  a)  =  b1)
\mvdash{}  \mexists{}a:\mBbbN{}  \mtimes{}  \mBbbN{}.  (((\mlambda{}p.let  i,n  =  p  in  <i,  h  i  n>)  a)  =  <i,  b1>)


By

---

Latex:
((D  -1  THEN  (D  0  With  \mkleeneopen{}<i,  a>\mkleeneclose{}    THENA  (Try  (D  -1)  THEN  Reduce  0  THEN  Auto)))
  THEN  Reduce  0
  THEN  EqCD
  THEN  Auto)

---

Home Index