Step * 1 of Lemma strong-continuity2-implies-weak-skolem-cantor-nat


1. F : (ℕ âŸś đ”š) âŸś â„•
⊢ â‡ƒ(∃M:(ℕ âŸś đ”š) âŸś â„•. âˆ€f,g:ℕ âŸś đ”š.  ((f = g âˆˆ (ℕM f âŸś đ”š)) â‡’ ((F f) = (F g) âˆˆ â„•)))
BY
{ (InstLemma `strong-continuity2-no-inner-squash-cantor2` [⌜F⌝]⋅ THENA Auto) }

1
1. F : (ℕ âŸś đ”š) âŸś â„•
2. â‡ƒ(∃M:n:ℕ âŸś (ℕn âŸś đ”š) âŸś (ℕ?)
      âˆ€f:ℕ âŸś đ”š. ((∃n:ℕ. ((M n f) = (inl (F f)) âˆˆ (ℕ?))) âˆ§ (∀n:ℕ. (M n f) = (inl (F f)) âˆˆ (ℕ?) supposing â†‘isl(M n f))))
⊢ â‡ƒ(∃M:(ℕ âŸś đ”š) âŸś â„•. âˆ€f,g:ℕ âŸś đ”š.  ((f = g âˆˆ (ℕM f âŸś đ”š)) â‡’ ((F f) = (F g) âˆˆ â„•)))

Latex:

Latex:

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


By

Latex:
(InstLemma  `strong-continuity2-no-inner-squash-cantor2`  [\mkleeneopen{}F\mkleeneclose{}]\mcdot{}  THENA  Auto)



Home Index