---

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


1. P : (ℕ ⟶ ℕ) ⟶ ℕ ⟶ ℙ
2. F : ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. (P f n))
3. M : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
4. ∀f:ℕ ⟶ ℕ. ∃n:ℕ. ∃k:ℕn. ((P f k) ∧ ((M n f) = (inl k) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))
⊢ ∃M:n:ℕ ⟶ s:(ℕn ⟶ ℕ) ⟶ (k:ℕn × (P ext2Baire(n;s;0) k)?)
   ∀f:ℕ ⟶ ℕ
     ∃n:ℕ
      ∃k:ℕn
       ∃p:P ext2Baire(n;f;0) k
        (((M n f) = (inl <k, p>) ∈ (k:ℕn × (P ext2Baire(n;f;0) k)?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))
BY
{ (RenameVar `G' (-1)
   THEN (InstConcl [⌜λn,s. let z,k,p,q = G ext2Baire(n;s;0) in if (z =z n) then inl <k, p> else inr Ax  fi   ⌝]⋅ THENA A\000Cuto)
   THEN Reduce 0
   THEN (D 0 THENA Auto)) }

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

---

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.  \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))))
\mvdash{}  \mexists{}M:n:\mBbbN{}  {}\mrightarrow{}  s:(\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  (k:\mBbbN{}n  \mtimes{}  (P  ext2Baire(n;s;0)  k)?)
      \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}
          \mexists{}n:\mBbbN{}
            \mexists{}k:\mBbbN{}n.  \mexists{}p:P  ext2Baire(n;f;0)  k.  (((M  n  f)  =  (inl  <k,  p>))  \mwedge{}  (\mforall{}m:\mBbbN{}.  ((\muparrow{}isl(M  m  f))  {}\mRightarrow{}  (m  =  n)))\000C)


By

---

Latex:
(RenameVar  `G'  (-1)
  THEN  (InstConcl  [\mkleeneopen{}\mlambda{}n,s.  let  z,k,p,q  =  G  ext2Baire(n;s;0) 
                                                  in  if  (z  =\msubz{}  n)  then  inl  <k,  p>  else  inr  Ax    fi      \mkleeneclose{}]\mcdot{}
              THENA  Auto
              )
  THEN  Reduce  0
  THEN  (D  0  THENA  Auto))

---

Home Index