---

Step * 1 1 1 1 1 1 1 1 1 of Lemma strong-continuity-rel-unique-pair


1. n : ℕ
2. k : ℕn
3. P : (ℕ ⟶ ℕ) ⟶ ℕ ⟶ ℙ
4. F : ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. (P f n))
5. M : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
6. G : ∀f:ℕ ⟶ ℕ. ∃n:ℕ. ∃k:ℕn. ((P f k) ∧ ((M n f) = (inl k) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))
7. f : ℕ ⟶ ℕ
8. P f k
9. (M n f) = (inl k) ∈ (ℕ?)
10. ∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))
11. v3 : P ext2Baire(n;f;0) k
12. v5 : (M n ext2Baire(n;f;0)) = (inl k) ∈ (ℕ?)
13. v6 : ∀m:ℕ. ((↑isl(M m ext2Baire(n;f;0))) ⇒ (m = n ∈ ℕ))
14. (G ext2Baire(n;f;0))
= <n, k, v3, v5, v6>
∈ (∃n@0:ℕ
    ∃k:ℕn@0
     ((P ext2Baire(n;f;0) k)
     ∧ ((M n@0 ext2Baire(n;f;0)) = (inl k) ∈ (ℕ?))
     ∧ (∀m:ℕ. ((↑isl(M m ext2Baire(n;f;0))) ⇒ (m = n@0 ∈ ℕ)))))
15. n = n ∈ ℤ
16. m : ℕ
17. n1 : ℕ
18. k1 : ℕn1
19. v9 : P ext2Baire(m;f;0) k1
20. v11 : (M n1 ext2Baire(m;f;0)) = (inl k1) ∈ (ℕ?)
21. v12 : ∀m@0:ℕ. ((↑isl(M m@0 ext2Baire(m;f;0))) ⇒ (m@0 = n1 ∈ ℕ))
22. (G ext2Baire(m;f;0))
= <n1, k1, v9, v11, v12>
∈ (∃n:ℕ
    ∃k:ℕn
     ((P ext2Baire(m;f;0) k)
     ∧ ((M n ext2Baire(m;f;0)) = (inl k) ∈ (ℕ?))
     ∧ (∀m@0:ℕ. ((↑isl(M m@0 ext2Baire(m;f;0))) ⇒ (m@0 = n ∈ ℕ)))))
⊢ (↑isl(if (n1 =z m) then inl <k1, v9> else inr Ax  fi )) ⇒ (m = n ∈ ℕ)
BY
{ (AutoSplit THEN Eliminate ⌜n1⌝⋅ THEN ThinVar `n1' THEN (D 0 THENA Auto) THEN Thin (-1)) }

1
1. m : ℕ
2. n : ℕ
3. k : ℕn
4. P : (ℕ ⟶ ℕ) ⟶ ℕ ⟶ ℙ
5. F : ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. (P f n))
6. M : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
7. G : ∀f:ℕ ⟶ ℕ. ∃n:ℕ. ∃k:ℕn. ((P f k) ∧ ((M n f) = (inl k) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))
8. f : ℕ ⟶ ℕ
9. P f k
10. (M n f) = (inl k) ∈ (ℕ?)
11. ∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))
12. v3 : P ext2Baire(n;f;0) k
13. v5 : (M n ext2Baire(n;f;0)) = (inl k) ∈ (ℕ?)
14. v6 : ∀m:ℕ. ((↑isl(M m ext2Baire(n;f;0))) ⇒ (m = n ∈ ℕ))
15. (G ext2Baire(n;f;0))
= <n, k, v3, v5, v6>
∈ (∃n@0:ℕ
    ∃k:ℕn@0
     ((P ext2Baire(n;f;0) k)
     ∧ ((M n@0 ext2Baire(n;f;0)) = (inl k) ∈ (ℕ?))
     ∧ (∀m:ℕ. ((↑isl(M m ext2Baire(n;f;0))) ⇒ (m = n@0 ∈ ℕ)))))
16. n = n ∈ ℤ
17. k1 : ℕm
18. v9 : P ext2Baire(m;f;0) k1
19. v11 : (M m ext2Baire(m;f;0)) = (inl k1) ∈ (ℕ?)
20. v12 : ∀m@0:ℕ. ((↑isl(M m@0 ext2Baire(m;f;0))) ⇒ (m@0 = m ∈ ℕ))
21. (G ext2Baire(m;f;0))
= <m, k1, v9, v11, v12>
∈ (∃n:ℕ
    ∃k:ℕn
     ((P ext2Baire(m;f;0) k)
     ∧ ((M n ext2Baire(m;f;0)) = (inl k) ∈ (ℕ?))
     ∧ (∀m@0:ℕ. ((↑isl(M m@0 ext2Baire(m;f;0))) ⇒ (m@0 = n ∈ ℕ)))))
⊢ m = n ∈ ℕ

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}n
3.  P  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
4.  F  :  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}n:\mBbbN{}.  (P  f  n))
5.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  (\mBbbN{}n?)
6.  G  :  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mexists{}n:\mBbbN{}.  \mexists{}k:\mBbbN{}n.  ((P  f  k)  \mwedge{}  ((M  n  f)  =  (inl  k))  \mwedge{}  (\mforall{}m:\mBbbN{}.  ((\muparrow{}isl(M  m  f))  {}\mRightarrow{}  (m  =  n))))
7.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
8.  P  f  k
9.  (M  n  f)  =  (inl  k)
10.  \mforall{}m:\mBbbN{}.  ((\muparrow{}isl(M  m  f))  {}\mRightarrow{}  (m  =  n))
11.  v3  :  P  ext2Baire(n;f;0)  k
12.  v5  :  (M  n  ext2Baire(n;f;0))  =  (inl  k)
13.  v6  :  \mforall{}m:\mBbbN{}.  ((\muparrow{}isl(M  m  ext2Baire(n;f;0)))  {}\mRightarrow{}  (m  =  n))
14.  (G  ext2Baire(n;f;0))  =  <n,  k,  v3,  v5,  v6>
15.  n  =  n
16.  m  :  \mBbbN{}
17.  n1  :  \mBbbN{}
18.  k1  :  \mBbbN{}n1
19.  v9  :  P  ext2Baire(m;f;0)  k1
20.  v11  :  (M  n1  ext2Baire(m;f;0))  =  (inl  k1)
21.  v12  :  \mforall{}m@0:\mBbbN{}.  ((\muparrow{}isl(M  m@0  ext2Baire(m;f;0)))  {}\mRightarrow{}  (m@0  =  n1))
22.  (G  ext2Baire(m;f;0))  =  <n1,  k1,  v9,  v11,  v12>
\mvdash{}  (\muparrow{}isl(if  (n1  =\msubz{}  m)  then  inl  <k1,  v9>  else  inr  Ax    fi  ))  {}\mRightarrow{}  (m  =  n)


By

---

Latex:
(AutoSplit  THEN  Eliminate  \mkleeneopen{}n1\mkleeneclose{}\mcdot{}  THEN  ThinVar  `n1'  THEN  (D  0  THENA  Auto)  THEN  Thin  (-1))

---

Home Index