---

Step * of Lemma countable-nsub-family

∀B:ℕ ⟶ ℕ+. ∃g:ℕ ⟶ (i:ℕ × ℕB[i]). Surj(ℕ;i:ℕ × ℕB[i];g)
BY
{ ((D 0 THENA Auto)
   THEN (Assert ∃f:ℕ ⟶ (ℕ × ℕ). Surj(ℕ;ℕ × ℕ;f) BY
               (InstLemma `code-pair-bijection` [] THEN D -1 THEN Auto))
   THEN (Assert ⌜∃g:(ℕ × ℕ) ⟶ (i:ℕ × ℕB[i]). Surj(ℕ × ℕ;i:ℕ × ℕB[i];g)⌝⋅
   THENM (ExRepD THEN FLemma `compose-surjections` [-1;-3] THEN Auto)
   )) }

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

---

Latex:

---

Latex:
\mforall{}B:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}.  \mexists{}g:\mBbbN{}  {}\mrightarrow{}  (i:\mBbbN{}  \mtimes{}  \mBbbN{}B[i]).  Surj(\mBbbN{};i:\mBbbN{}  \mtimes{}  \mBbbN{}B[i];g)


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (Assert  \mexists{}f:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}  \mtimes{}  \mBbbN{}).  Surj(\mBbbN{};\mBbbN{}  \mtimes{}  \mBbbN{};f)  BY
                          (InstLemma  `code-pair-bijection`  []  THEN  D  -1  THEN  Auto))
  THEN  (Assert  \mkleeneopen{}\mexists{}g:(\mBbbN{}  \mtimes{}  \mBbbN{})  {}\mrightarrow{}  (i:\mBbbN{}  \mtimes{}  \mBbbN{}B[i]).  Surj(\mBbbN{}  \mtimes{}  \mBbbN{};i:\mBbbN{}  \mtimes{}  \mBbbN{}B[i];g)\mkleeneclose{}\mcdot{}
  THENM  (ExRepD  THEN  FLemma  `compose-surjections`  [-1;-3]  THEN  Auto)
  ))

---

Home Index