---

Step * 1 of Lemma WCP_wf


1. F : (ℕ+ ⟶ ℤ) ⟶ 𝔹
2. f : ℕ+ ⟶ ℤ
3. G : n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} 
4. TERMOF{weak-continuity-principle-nat+-int-bool-ext:o, 1:l} ∈ ∀F:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| 
                                                                                                           f
                                                                                                           = g
                                                                                                           ∈ (ℕ+n
                                                                                                             ⟶ ℤ)} .
                                                                  ∃n:ℕ+. F f = F (G n)
⊢ WCP(F;f;G) ∈ {n:ℕ+| F f = F (G n)} 
BY
{ (Subst' WCP(F;f;G) ~ fst((TERMOF{weak-continuity-principle-nat+-int-bool-ext:o, 1:l} F f G)) 0 THENM Auto) }

1
.....equality..... 
1. F : (ℕ+ ⟶ ℤ) ⟶ 𝔹
2. f : ℕ+ ⟶ ℤ
3. G : n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| f = g ∈ (ℕ+n ⟶ ℤ)} 
4. TERMOF{weak-continuity-principle-nat+-int-bool-ext:o, 1:l} ∈ ∀F:(ℕ+ ⟶ ℤ) ⟶ 𝔹. ∀f:ℕ+ ⟶ ℤ. ∀G:n:ℕ+ ⟶ {g:ℕ+ ⟶ ℤ| 
                                                                                                           f
                                                                                                           = g
                                                                                                           ∈ (ℕ+n
                                                                                                             ⟶ ℤ)} .
                                                                  ∃n:ℕ+. F f = F (G n)
⊢ WCP(F;f;G) ~ fst((TERMOF{weak-continuity-principle-nat+-int-bool-ext:o, 1:l} F f G))

---

Latex:

---

Latex:

1.  F  :  (\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbB{}
2.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
3.  G  :  n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{g:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  f  =  g\} 
4.  TERMOF\{weak-continuity-principle-nat+-int-bool-ext:o,  1:l\}
      \mmember{}  \mforall{}F:(\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{})  {}\mrightarrow{}  \mBbbB{}.  \mforall{}f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}G:n:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \{g:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}|  f  =  g\}  .    \mexists{}n:\mBbbN{}\msupplus{}.  F  f  =  F  (G  n)
\mvdash{}  WCP(F;f;G)  \mmember{}  \{n:\mBbbN{}\msupplus{}|  F  f  =  F  (G  n)\} 


By

---

Latex:
(Subst'  WCP(F;f;G)  \msim{}  fst((TERMOF\{weak-continuity-principle-nat+-int-bool-ext:o,  1:l\}  F  f  G))  0
THENM  Auto
)

---

Home Index