---

Step * 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 : ℕ ⟶ ℕ
⊢ ∃n:ℕ
   ∃k:ℕ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
{ ((InstHyp [⌜f⌝] (-2)⋅ THENA Auto)
   THEN ExRepD
   THEN (InstConcl [⌜n⌝;⌜k⌝]⋅
         THENA (Auto THEN (GenConclTerm ⌜G ext2Baire(m;f;0)⌝⋅ THENA Auto) THEN ExRepD THEN Reduce 0 THEN AutoSplit)
         )) }

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 ∈ ℕ))
⊢ ∃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)

---

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{}
\mvdash{}  \mexists{}n:\mBbbN{}
      \mexists{}k:\mBbbN{}n
        \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,\000C  p>))
          \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:
((InstHyp  [\mkleeneopen{}f\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  ExRepD
  THEN  (InstConcl  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  (GenConclTerm  \mkleeneopen{}G  ext2Baire(m;f;0)\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  ExRepD
                            THEN  Reduce  0
                            THEN  AutoSplit)
              ))

---

Home Index