---

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


1. P : (ℕ ⟶ ℕ) ⟶ ℕ ⟶ ℙ
2. F : ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. (P f n))
3. M : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
4. G : ∀f:ℕ ⟶ ℕ. ∃n:ℕ. ∃k:ℕn. ((P f k) ∧ ((M n f) = (inl k) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))
5. f : ℕ ⟶ ℕ
6. n : ℕ
7. k : ℕn
8. P f k
9. (M n f) = (inl k) ∈ (ℕ?)
10. ∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))
⊢ ∃p:P ext2Baire(n;f;0) k
   ((let z,k,p,q = G ext2Baire(n;f;0) 
     in if (z =z n) then inl <k, p> else inr Ax  fi   
   = (inl <k, p>)
   ∈ (k:ℕn × (P ext2Baire(n;f;0) k)?))
   ∧ (∀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 ∈ ℕ)))\000C)
BY
{ ((GenConclTerm ⌜G ext2Baire(n;f;0)⌝⋅ THENA Auto) THEN ExRepD THEN Reduce 0) }

1
1. P : (ℕ ⟶ ℕ) ⟶ ℕ ⟶ ℙ
2. F : ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. (P f n))
3. M : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
4. G : ∀f:ℕ ⟶ ℕ. ∃n:ℕ. ∃k:ℕn. ((P f k) ∧ ((M n f) = (inl k) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))
5. f : ℕ ⟶ ℕ
6. n : ℕ
7. k : ℕn
8. P f k
9. (M n f) = (inl k) ∈ (ℕ?)
10. ∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))
11. n@0 : ℕ
12. k1 : ℕn@0
13. v3 : P ext2Baire(n;f;0) k1
14. v5 : (M n@0 ext2Baire(n;f;0)) = (inl k1) ∈ (ℕ?)
15. v6 : ∀m:ℕ. ((↑isl(M m ext2Baire(n;f;0))) ⇒ (m = n@0 ∈ ℕ))
16. (G ext2Baire(n;f;0))
= <n@0, k1, 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 ∈ ℕ)))))
⊢ ∃p:P ext2Baire(n;f;0) k
   ((if (n@0 =z n) then inl <k1, v3> else inr Ax  fi  = (inl <k, p>) ∈ (k:ℕn × (P ext2Baire(n;f;0) k)?))
   ∧ (∀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 ∈ ℕ)))\000C)

---

Latex:

---

Latex:

1.  P  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  F  :  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}n:\mBbbN{}.  (P  f  n))
3.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  (\mBbbN{}n?)
4.  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))))
5.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
6.  n  :  \mBbbN{}
7.  k  :  \mBbbN{}n
8.  P  f  k
9.  (M  n  f)  =  (inl  k)
10.  \mforall{}m:\mBbbN{}.  ((\muparrow{}isl(M  m  f))  {}\mRightarrow{}  (m  =  n))
\mvdash{}  \mexists{}p:P  ext2Baire(n;f;0)  k
      ((let  z,k,p,q  =  G  ext2Baire(n;f;0)  in  if  (z  =\msubz{}  n)  then  inl  <k,  p>  else  inr  Ax    fi        =  (inl  <k,  p\000C>))
      \mwedge{}  (\mforall{}m:\mBbbN{}
                ((\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  =  n))))


By

---

Latex:
((GenConclTerm  \mkleeneopen{}G  ext2Baire(n;f;0)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  ExRepD  THEN  Reduce  0)

---

Home Index