---

Step * 1 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 ∈ ℕ))
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)
BY
{ ((Assert ⌜(M n f) = (M n ext2Baire(n;f;0)) ∈ (ℕ?)⌝⋅
    THENA ((MemCD THEN Auto) THEN (Ext THENA Auto) THEN RepUR ``ext2Baire`` 0 THEN AutoSplit)
    )
   THEN (InstHyp [⌜n⌝] (-3)⋅ THENA Auto)
   THEN Eliminate ⌜n@0⌝⋅
   THEN ThinVar `n@0') }

1
1. n : ℕ
2. P : (ℕ ⟶ ℕ) ⟶ ℕ ⟶ ℙ
3. F : ∀f:ℕ ⟶ ℕ. ⇃(∃n:ℕ. (P f n))
4. M : n:ℕ ⟶ (ℕn ⟶ ℕ) ⟶ (ℕn?)
5. G : ∀f:ℕ ⟶ ℕ. ∃n:ℕ. ∃k:ℕn. ((P f k) ∧ ((M n f) = (inl k) ∈ (ℕ?)) ∧ (∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))))
6. f : ℕ ⟶ ℕ
7. k : ℕn
8. P f k
9. (M n f) = (inl k) ∈ (ℕ?)
10. ∀m:ℕ. ((↑isl(M m f)) ⇒ (m = n ∈ ℕ))
11. k1 : ℕn
12. v3 : P ext2Baire(n;f;0) k1
13. v5 : (M n ext2Baire(n;f;0)) = (inl k1) ∈ (ℕ?)
14. v6 : ∀m:ℕ. ((↑isl(M m ext2Baire(n;f;0))) ⇒ (m = n ∈ ℕ))
15. (G ext2Baire(n;f;0))
= <n, 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 ∈ ℕ)))))
16. (M n f) = (M n ext2Baire(n;f;0)) ∈ (ℕ?)
⊢ ∃p:P ext2Baire(n;f;0) k
   ((if (n =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))
11.  n@0  :  \mBbbN{}
12.  k1  :  \mBbbN{}n@0
13.  v3  :  P  ext2Baire(n;f;0)  k1
14.  v5  :  (M  n@0  ext2Baire(n;f;0))  =  (inl  k1)
15.  v6  :  \mforall{}m:\mBbbN{}.  ((\muparrow{}isl(M  m  ext2Baire(n;f;0)))  {}\mRightarrow{}  (m  =  n@0))
16.  (G  ext2Baire(n;f;0))  =  <n@0,  k1,  v3,  v5,  v6>
\mvdash{}  \mexists{}p:P  ext2Baire(n;f;0)  k
      ((if  (n@0  =\msubz{}  n)  then  inl  <k1,  v3>  else  inr  Ax    fi    =  (inl  <k,  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:
((Assert  \mkleeneopen{}(M  n  f)  =  (M  n  ext2Baire(n;f;0))\mkleeneclose{}\mcdot{}
    THENA  ((MemCD  THEN  Auto)  THEN  (Ext  THENA  Auto)  THEN  RepUR  ``ext2Baire``  0  THEN  AutoSplit)
    )
  THEN  (InstHyp  [\mkleeneopen{}n\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)
  THEN  Eliminate  \mkleeneopen{}n@0\mkleeneclose{}\mcdot{}
  THEN  ThinVar  `n@0')

---

Home Index