---

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


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)
BY
{ (HypSubst' (-8) (-1)
   THEN HypSubst' (-4) (-1)
   THEN (Assert ⌜k = k1 ∈ ℕ⌝⋅ THENA Auto)
   THEN Eliminate ⌜k1⌝⋅
   THEN ThinVar `k1'
   THEN Thin (-1)) }

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 ∈ ℕ)))))
⊢ ∃p:P ext2Baire(n;f;0) k
   ((if (n =z n) then inl <k, 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.  n  :  \mBbbN{}
2.  P  :  (\mBbbN{}  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
3.  F  :  \mforall{}f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}n:\mBbbN{}.  (P  f  n))
4.  M  :  n:\mBbbN{}  {}\mrightarrow{}  (\mBbbN{}n  {}\mrightarrow{}  \mBbbN{})  {}\mrightarrow{}  (\mBbbN{}n?)
5.  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))))
6.  f  :  \mBbbN{}  {}\mrightarrow{}  \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.  k1  :  \mBbbN{}n
12.  v3  :  P  ext2Baire(n;f;0)  k1
13.  v5  :  (M  n  ext2Baire(n;f;0))  =  (inl  k1)
14.  v6  :  \mforall{}m:\mBbbN{}.  ((\muparrow{}isl(M  m  ext2Baire(n;f;0)))  {}\mRightarrow{}  (m  =  n))
15.  (G  ext2Baire(n;f;0))  =  <n,  k1,  v3,  v5,  v6>
16.  (M  n  f)  =  (M  n  ext2Baire(n;f;0))
\mvdash{}  \mexists{}p:P  ext2Baire(n;f;0)  k
      ((if  (n  =\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:
(HypSubst'  (-8)  (-1)
  THEN  HypSubst'  (-4)  (-1)
  THEN  (Assert  \mkleeneopen{}k  =  k1\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Eliminate  \mkleeneopen{}k1\mkleeneclose{}\mcdot{}
  THEN  ThinVar  `k1'
  THEN  Thin  (-1))

---

Home Index