---

Step * 1 1 1 2 1 of Lemma cantor-to-general-cantor


1. B : ℕ ⟶ ℕ+
2. C : ℕ ⟶ ℕ+
3. ∀n:ℕ. ((B n) ≤ 2^(C n))
4. g : ℕ ⟶ ℕ
5. ((g 0) = 0 ∈ ℤ) ∧ (∀i:ℕ. ((g (i + 1)) = ((g i) + (C i)) ∈ ℤ))
6. ∀n,m:ℕ.  (n < m ⇒ g n < g m)
7. ∀k:ℕ. ∃n:ℕ. (k ∈ {g n..g (n + 1)-})
8. h : k:ℕ ⟶ ℕ
9. ∀k:ℕ. (k ∈ {g (h k)..g ((h k) + 1)-})
10. ∀n:ℕ. ∃f:({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;f)
11. F : n:ℕ ⟶ ({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n
12. ∀n:ℕ. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;F n)
13. k : ℕ
14. p : ℕ ⟶ 𝔹
15. q : ℕ ⟶ 𝔹
16. p = q ∈ (ℕg k ⟶ 𝔹)
17. n : ℕk
⊢ (F n p) = (F n q) ∈ ℕB[n]
BY
{ EqCD }

1
.....subterm..... T:t
1:n
1. B : ℕ ⟶ ℕ+
2. C : ℕ ⟶ ℕ+
3. ∀n:ℕ. ((B n) ≤ 2^(C n))
4. g : ℕ ⟶ ℕ
5. ((g 0) = 0 ∈ ℤ) ∧ (∀i:ℕ. ((g (i + 1)) = ((g i) + (C i)) ∈ ℤ))
6. ∀n,m:ℕ.  (n < m ⇒ g n < g m)
7. ∀k:ℕ. ∃n:ℕ. (k ∈ {g n..g (n + 1)-})
8. h : k:ℕ ⟶ ℕ
9. ∀k:ℕ. (k ∈ {g (h k)..g ((h k) + 1)-})
10. ∀n:ℕ. ∃f:({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;f)
11. F : n:ℕ ⟶ ({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n
12. ∀n:ℕ. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;F n)
13. k : ℕ
14. p : ℕ ⟶ 𝔹
15. q : ℕ ⟶ 𝔹
16. p = q ∈ (ℕg k ⟶ 𝔹)
17. n : ℕk
⊢ (F n) = (F n) ∈ (({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n)

2
.....subterm..... T:t
2:n
1. B : ℕ ⟶ ℕ+
2. C : ℕ ⟶ ℕ+
3. ∀n:ℕ. ((B n) ≤ 2^(C n))
4. g : ℕ ⟶ ℕ
5. ((g 0) = 0 ∈ ℤ) ∧ (∀i:ℕ. ((g (i + 1)) = ((g i) + (C i)) ∈ ℤ))
6. ∀n,m:ℕ.  (n < m ⇒ g n < g m)
7. ∀k:ℕ. ∃n:ℕ. (k ∈ {g n..g (n + 1)-})
8. h : k:ℕ ⟶ ℕ
9. ∀k:ℕ. (k ∈ {g (h k)..g ((h k) + 1)-})
10. ∀n:ℕ. ∃f:({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;f)
11. F : n:ℕ ⟶ ({g n..g (n + 1)-} ⟶ 𝔹) ⟶ ℕB n
12. ∀n:ℕ. Surj({g n..g (n + 1)-} ⟶ 𝔹;ℕB n;F n)
13. k : ℕ
14. p : ℕ ⟶ 𝔹
15. q : ℕ ⟶ 𝔹
16. p = q ∈ (ℕg k ⟶ 𝔹)
17. n : ℕk
⊢ p = q ∈ ({g n..g (n + 1)-} ⟶ 𝔹)

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  C  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
3.  \mforall{}n:\mBbbN{}.  ((B  n)  \mleq{}  2\^{}(C  n))
4.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
5.  ((g  0)  =  0)  \mwedge{}  (\mforall{}i:\mBbbN{}.  ((g  (i  +  1))  =  ((g  i)  +  (C  i))))
6.  \mforall{}n,m:\mBbbN{}.    (n  <  m  {}\mRightarrow{}  g  n  <  g  m)
7.  \mforall{}k:\mBbbN{}.  \mexists{}n:\mBbbN{}.  (k  \mmember{}  \{g  n..g  (n  +  1)\msupminus{}\})
8.  h  :  k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
9.  \mforall{}k:\mBbbN{}.  (k  \mmember{}  \{g  (h  k)..g  ((h  k)  +  1)\msupminus{}\})
10.  \mforall{}n:\mBbbN{}.  \mexists{}f:(\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}B  n.  Surj(\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{};\mBbbN{}B  n;f)
11.  F  :  n:\mBbbN{}  {}\mrightarrow{}  (\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}B  n
12.  \mforall{}n:\mBbbN{}.  Surj(\{g  n..g  (n  +  1)\msupminus{}\}  {}\mrightarrow{}  \mBbbB{};\mBbbN{}B  n;F  n)
13.  k  :  \mBbbN{}
14.  p  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
15.  q  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
16.  p  =  q
17.  n  :  \mBbbN{}k
\mvdash{}  (F  n  p)  =  (F  n  q)


By

---

Latex:
EqCD

---

Home Index