---

Step * 1 1 1 2 2 of Lemma cantor-to-interval-onto-proper

.....set predicate..... 
1. a : ℝ
2. b : ℝ
3. a < b
4. x : ℝ
5. a ≤ x
6. x ≤ b
7. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} .
     ∃g:{g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]} . (g = f ∈ (ℕn ⟶ 𝔹)\000C)
8. g : n:ℕ
⟶ f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} 
⟶ {g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]} 
9. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} .  ((g n f) = f ∈ (ℕn ⟶ 𝔹))
10. ∀n:ℕ. (primrec(n;λx.ff;g) ∈ {f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} )
11. λn.(primrec(n + 1;λx.ff;g) n) ∈ ℕ ⟶ 𝔹
⊢ ∀n:ℕ
    (x ∈ [fst(cantor-interval(a;b;λn.(primrec(n + 1;λx.ff;g) n);n)), snd(cantor-interval(a;b;λn.(primrec(n + 1;λx.ff;g) 
                                                                                                 n);n))])
BY
{ ((D 0 THENA Auto) THEN (InstHyp [⌜n⌝] (-3)⋅ THENA Auto) THEN (MemTypeHD (-1) THENA Auto) THEN (Unhide THENA Auto)) }

1
1. a : ℝ
2. b : ℝ
3. a < b
4. x : ℝ
5. a ≤ x
6. x ≤ b
7. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} .
     ∃g:{g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]} . (g = f ∈ (ℕn ⟶ 𝔹)\000C)
8. g : n:ℕ
⟶ f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} 
⟶ {g:ℕn + 1 ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;g;n + 1)), snd(cantor-interval(a;b;g;n + 1))]} 
9. ∀n:ℕ. ∀f:{f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} .  ((g n f) = f ∈ (ℕn ⟶ 𝔹))
10. ∀n:ℕ. (primrec(n;λx.ff;g) ∈ {f:ℕn ⟶ 𝔹| x ∈ [fst(cantor-interval(a;b;f;n)), snd(cantor-interval(a;b;f;n))]} )
11. λn.(primrec(n + 1;λx.ff;g) n) ∈ ℕ ⟶ 𝔹
12. n : ℕ
13. primrec(n;λx.ff;g) = primrec(n;λx.ff;g) ∈ (ℕn ⟶ 𝔹)
14. x ∈ [fst(cantor-interval(a;b;primrec(n;λx.ff;g);n)), snd(cantor-interval(a;b;primrec(n;λx.ff;g);n))]
⊢ x ∈ [fst(cantor-interval(a;b;λn.(primrec(n + 1;λx.ff;g) n);n)), snd(cantor-interval(a;b;λn.(primrec(n + 1;λx.ff;g) 
                                                                                              n);n))]

---

Latex:

---

Latex:
.....set  predicate..... 
1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  a  <  b
4.  x  :  \mBbbR{}
5.  a  \mleq{}  x
6.  x  \mleq{}  b
7.  \mforall{}n:\mBbbN{}.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]\}  .
          \mexists{}g:\{g:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;g;n  +  1)),  snd(cantor-interval(a;b;g;n  +  1))]\} 
            (g  =  f)
8.  g  :  n:\mBbbN{}
{}\mrightarrow{}  f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]\} 
{}\mrightarrow{}  \{g:\mBbbN{}n  +  1  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;g;n  +  1)),  snd(cantor-interval(a;b;g;n  +  1))]\} 
9.  \mforall{}n:\mBbbN{}.  \mforall{}f:\{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}|  x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]\}  .
          ((g  n  f)  =  f)
10.  \mforall{}n:\mBbbN{}
            (primrec(n;\mlambda{}x.ff;g)  \mmember{}  \{f:\mBbbN{}n  {}\mrightarrow{}  \mBbbB{}| 
                                                          x  \mmember{}  [fst(cantor-interval(a;b;f;n)),  snd(cantor-interval(a;b;f;n))]\}  )
11.  \mlambda{}n.(primrec(n  +  1;\mlambda{}x.ff;g)  n)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  \mforall{}n:\mBbbN{}
        (x  \mmember{}  [fst(cantor-interval(a;b;\mlambda{}n.(primrec(n  +  1;\mlambda{}x.ff;g) 
                                                                            n);n)),  snd(cantor-interval(a;b;\mlambda{}n.(primrec(n  +  1;\mlambda{}x.ff;g) 
                                                                                                                                                    n);n))])


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  (Unhide  THENA  Auto))

---

Home Index