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

`∀F:(ℕ ⟶ ℕ) ⟶ ℕ. ⇃(∃M:(ℕ ⟶ ℕ) ⟶ ℕ. ∀f,g:ℕ ⟶ ℕ.  ((f = g ∈ (ℕM f ⟶ ℕ)) `` ((F f) = (F g) ∈ ℕ)))`
BY
`{ ((UnivCD THENA Auto)`
`   THEN (Assert ⇃(strong-continuity2(ℕ;F)) BY`
`               ((InstLemma `strong-continuity2-no-inner-squash` [⌜F⌝]⋅ THENA Auto)`
`                THEN Unfold `strong-continuity2` 0`
`                THEN Auto))`
`   THEN Fold `weak-continuity-skolem` 0`
`   THEN MoveToConcl (-1)`
`   THEN BLemma  `implies-quotient-true``
`   THEN Auto) }`

1
`1. F : (ℕ ⟶ ℕ) ⟶ ℕ`
`2. strong-continuity2(ℕ;F)`
`⊢ weak-continuity-skolem(ℕ;F)`

Latex:

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

By

Latex:
((UnivCD  THENA  Auto)
THEN  (Assert  \00D9(strong-continuity2(\mBbbN{};F))  BY
((InstLemma  `strong-continuity2-no-inner-squash`  [\mkleeneopen{}F\mkleeneclose{}]\mcdot{}  THENA  Auto)
THEN  Unfold  `strong-continuity2`  0
THEN  Auto))
THEN  Fold  `weak-continuity-skolem`  0
THEN  MoveToConcl  (-1)
THEN  BLemma    `implies-quotient-true`
THEN  Auto)

Home Index