---

Step * 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 : ℕ
⊢ (↑isl(let z,k,p,q = G ext2Baire(m;f;0) in if (z =z m) then inl <k, p> else inr Ax  fi   )) ⇒ (m = n ∈ ℕ)
BY
{ ((GenConclTerm ⌜G ext2Baire(m;f;0)⌝⋅ THENA Auto)
   THEN DVar `v'
   THEN DVar `v7'
   THEN DVar `v8'
   THEN DVar `v10'
   THEN Reduce 0) }

1
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 ∈ ℕ)

---

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{}
\mvdash{}  (\muparrow{}isl(let  z,k,p,q  =  G  ext2Baire(m;f;0)  in  if  (z  =\msubz{}  m)  then  inl  <k,  p>  else  inr  Ax    fi      ))  {}\mRightarrow{}  (m  =\000C  n)


By

---

Latex:
((GenConclTerm  \mkleeneopen{}G  ext2Baire(m;f;0)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  DVar  `v'
  THEN  DVar  `v7'
  THEN  DVar  `v8'
  THEN  DVar  `v10'
  THEN  Reduce  0)

---

Home Index