Step * of Lemma strong-continuity2-implies-weak-skolem2

`∀F:(ℕ ⟶ 𝔹) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ 𝔹) ⟶ ℕ. ∀f,g:ℕ ⟶ 𝔹.  ((f = g ∈ (ℕM f ⟶ 𝔹)) `` ((F f) = (F g) ∈ ℕ)))`
BY
`{ ((UnivCD THENA Auto)`
`   THEN Fold `weak-continuity-skolem` 0`
`   THEN (Assert ℕ2 ~ 𝔹 BY`
`               EAuto 2)`
`   THEN RenameVar `e' (-1)`
`   THEN Assert ⌜⇃(weak-continuity-skolem(ℕ2;λf.(F ((fst(e)) o f))))⌝⋅) }`

1
`.....assertion..... `
`1. F : (ℕ ⟶ 𝔹) ⟶ ℕ`
`2. e : ℕ2 ~ 𝔹`
`⊢ ⇃(weak-continuity-skolem(ℕ2;λf.(F ((fst(e)) o f))))`

2
`1. F : (ℕ ⟶ 𝔹) ⟶ ℕ`
`2. e : ℕ2 ~ 𝔹`
`3. ⇃(weak-continuity-skolem(ℕ2;λf.(F ((fst(e)) o f))))`
`⊢ ⇃(weak-continuity-skolem(𝔹;F))`

Latex:

Latex:
\mforall{}F:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}.  \00D9(\mexists{}M:(\mBbbN{}  {}\mrightarrow{}  \mBbbB{})  {}\mrightarrow{}  \mBbbN{}.  \mforall{}f,g:\mBbbN{}  {}\mrightarrow{}  \mBbbB{}.    ((f  =  g)  {}\mRightarrow{}  ((F  f)  =  (F  g))))

By

Latex:
((UnivCD  THENA  Auto)
THEN  Fold  `weak-continuity-skolem`  0
THEN  (Assert  \mBbbN{}2  \msim{}  \mBbbB{}  BY
EAuto  2)
THEN  RenameVar  `e'  (-1)
THEN  Assert  \mkleeneopen{}\00D9(weak-continuity-skolem(\mBbbN{}2;\mlambda{}f.(F  ((fst(e))  o  f))))\mkleeneclose{}\mcdot{})

Home Index