---

Step * 1 2 of Lemma general-cantor-to-int-uniform-continuity


1. B : ℕ ⟶ ℕ+
2. F : (k:ℕ ⟶ ℕB[k]) ⟶ ℤ
3. ⇃(∃n:ℕ. ∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
4. ⇃(∃n:ℕ
      ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
      ∧ (∀j:ℕ. ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))) ⇒ (n ≤ j)))))
⊢ ∃n:ℕ. ∀f,g:k:ℕ ⟶ ℕB[k].  ((f = g ∈ (k:ℕn ⟶ ℕB[k])) ⇒ ((F f) = (F g) ∈ ℤ))
BY
{ (Assert ∃n:ℕ
           ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
           ∧ (∀j:ℕ. ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))) ⇒ (n ≤ j)))) BY
         (BLemma `prop-truncation-implies`
          THEN Auto
          THEN (D -2 THEN D -1)
          THEN (Assert n = n1 ∈ ℤ BY
                      ((Decide ⌜n < n1⌝⋅ THENA Auto)
                       THENL [(ExRepD THEN InstHyp [⌜n⌝] (-2)⋅ THEN Auto)
                             ; ((Decide ⌜n1 < n⌝⋅ THENA Auto)
                                THENL [(ExRepD THEN InstHyp [⌜n1⌝] (-6)⋅ THEN Auto); Auto]
                             )]
                      ))
          THEN Eliminate ⌜n1⌝⋅
          THEN ThinVar `n1')) }

1
.....aux..... 
1. n : ℕ
2. B : ℕ ⟶ ℕ+
3. F : (k:ℕ ⟶ ℕB[k]) ⟶ ℤ
4. ⇃(∃n:ℕ. ∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
5. ⇃(∃n:ℕ
      ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
      ∧ (∀j:ℕ. ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))) ⇒ (n ≤ j)))))
6. a1 : (∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
∧ (∀j:ℕ. ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))) ⇒ (n ≤ j)))
7. b1 : (∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
∧ (∀j:ℕ. ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))) ⇒ (n ≤ j)))
⊢ <n, a1>
= <n, b1>
∈ (∃n:ℕ
    ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
    ∧ (∀j:ℕ. ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))) ⇒ (n ≤ j)))))

2
1. B : ℕ ⟶ ℕ+
2. F : (k:ℕ ⟶ ℕB[k]) ⟶ ℤ
3. ⇃(∃n:ℕ. ∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
4. ⇃(∃n:ℕ
      ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
      ∧ (∀j:ℕ. ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))) ⇒ (n ≤ j)))))
5. ∃n:ℕ
    ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕn ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ)))
    ∧ (∀j:ℕ. ((∀f,g:i:ℕ ⟶ ℕB[i].  ((f = g ∈ (i:ℕj ⟶ ℕB[i])) ⇒ ((F f) = (F g) ∈ ℤ))) ⇒ (n ≤ j))))
⊢ ∃n:ℕ. ∀f,g:k:ℕ ⟶ ℕB[k].  ((f = g ∈ (k:ℕn ⟶ ℕB[k])) ⇒ ((F f) = (F g) ∈ ℤ))

---

Latex:

---

Latex:

1.  B  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}\msupplus{}
2.  F  :  (k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[k])  {}\mrightarrow{}  \mBbbZ{}
3.  \00D9(\mexists{}n:\mBbbN{}.  \mforall{}f,g:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))
4.  \00D9(\mexists{}n:\mBbbN{}
            ((\mforall{}f,g:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))
            \mwedge{}  (\mforall{}j:\mBbbN{}.  ((\mforall{}f,g:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))  {}\mRightarrow{}  (n  \mleq{}  j)))))
\mvdash{}  \mexists{}n:\mBbbN{}.  \mforall{}f,g:k:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[k].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g)))


By

---

Latex:
(Assert  \mexists{}n:\mBbbN{}
                  ((\mforall{}f,g:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))
                  \mwedge{}  (\mforall{}j:\mBbbN{}.  ((\mforall{}f,g:i:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}B[i].    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))  {}\mRightarrow{}  (n  \mleq{}  j))))  BY
              (BLemma  `prop-truncation-implies`
                THEN  Auto
                THEN  (D  -2  THEN  D  -1)
                THEN  (Assert  n  =  n1  BY
                                        ((Decide  \mkleeneopen{}n  <  n1\mkleeneclose{}\mcdot{}  THENA  Auto)
                                          THENL  [(ExRepD  THEN  InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto)
                                                      ;  ((Decide  \mkleeneopen{}n1  <  n\mkleeneclose{}\mcdot{}  THENA  Auto)
                                                            THENL  [(ExRepD  THEN  InstHyp  [\mkleeneopen{}n1\mkleeneclose{}]  (-6)\mcdot{}  THEN  Auto);  Auto]
                                                      )]
                                        ))
                THEN  Eliminate  \mkleeneopen{}n1\mkleeneclose{}\mcdot{}
                THEN  ThinVar  `n1'))

---

Home Index