Intuitionize the next part of the limCC section (#3261)

* Add limcres to mmil.html

* Add metcnpd to iset.mm

This is a deduction form of metcnp .

* Add cnplimcim to iset.mm

This is one direction of cnplimc from set.mm.  We probably need the
converse at some point, but start with the easy direction.

* Add toponrestid to iset.mm

Copied without change from set.mm.

* Add cncfcncntop to iset.mm

This is cncfcn from set.mm with the only change being the notation for
the toplogy of the complex numbers.  The proof is also the set.mm proof with
those changes.

* Add cncfcn1cntop to iset.mm

This is cncfcn1 from set.mm with the notation for the topology of the
complex numbers changed.  The proof is the set.mm proof, changed
accordingly.

* Add cnlimcim to iset.mm

This is one direction of cnlimc from set.mm.  The proof is similar to
the set.mm proof but adjusted for being an implication rather than a
biconditional.

* Add cnlimci to iset.mm

Stated as in set.mm.  The proof is slightly modified because it is in
terms of cnlimcim rather than cnlimc as found in set.mm, but is
basically the set.mm proof.

* Add cnmptlimc to iset.mm

Copied without change from set.mm.

* Add cofmpt to iset.mm

Copied without change from set.mm.

* Add limccnpcntop to iset.mm

Stated the same as limccnp in set.mm except for the notation for the
topology of the complex numbers.

The proof is a new proof using ellimc3ap and metcnpd .

Author: jkingdon

iset.mm

@@ -49576,6 +49576,18 @@ We use their notation ("onto" under the arrow).  (Contributed by NM,
       EFCMNZGOZCFGOHIJKAICEGPMEUEPLCMEGUEMGQCUDGRCUDGSTUACUDFGUBUC $.
   $}
 
+  ${
+    $d x A $.  $d y B $.  $d x y C $.  $d x y F $.  $d x ph $.
+    cofmpt.1 $e |- ( ph -> F : C --> D ) $.
+    cofmpt.2 $e |- ( ( ph /\ x e. A ) -> B e. C ) $.
+    $( Express composition of a maps-to function with another function in a
+       maps-to notation.  (Contributed by Thierry Arnoux, 29-Jun-2017.) $)
+    cofmpt $p |- ( ph ->
+                     ( F o. ( x e. A |-> B ) ) = ( x e. A |-> ( F ` B ) ) ) $=
+      ( vy cv cfv cmpt eqidd feqmptd fveq2 fmptco ) ABJCEDJKZGLDGLBCDMZGIASNAJE
+      FGHORDGPQ $.
+  $}
+
   ${
     $d x y A $.  $d x y B $.  $d x C $.  $d x y D $.  $d x E $.
     $( Express composition of two functions as a maps-to applying both in
@@ -129719,6 +129731,15 @@ _Introduction to General Topology_ (1983), p. 114) and it is convenient
     ( ctopon cfv wcel ctop cuni topontop toptopon2 sylib ) ABCDEAFEAAGCDEBAHAIJ
     $.
 
+  ${
+    toponrestid.t $e |- A e. ( TopOn ` B ) $.
+    $( Given a topology on a set, restricting it to that same set has no
+       effect.  (Contributed by Jim Kingdon, 6-Jul-2022.) $)
+    toponrestid $p |- A = ( A |`t B ) $=
+      ( crest co ctopon cfv wcel wceq toponunii restid ax-mp eqcomi ) ABDEZAABF
+      GZHNAICAOBBACJKLM $.
+  $}
+
   ${
     $d A x y $.
     $( The set of topologies on a set is included in the double power set of
@@ -135120,6 +135141,26 @@ S C_ ( P ( ball ` D ) T ) ) $=
       XFXLXGABXJQJXEXJWPUHWEWFVSWG $.
   $}
 
+  ${
+    $d C w y z $.  $d D w y z $.  $d F w y z $.  $d P w y z $.  $d X w y z $.
+    $d Y w y z $.
+    metcnpd.j $e |- ( ph -> J = ( MetOpen ` C ) ) $.
+    metcnpd.k $e |- ( ph -> K = ( MetOpen ` D ) ) $.
+    metcnpd.c $e |- ( ph -> C e. ( *Met ` X ) ) $.
+    metcnpd.d $e |- ( ph -> D e. ( *Met ` Y ) ) $.
+    metcnpd.p $e |- ( ph -> P e. X ) $.
+    $( Two ways to say a mapping from metric ` C ` to metric ` D ` is
+       continuous at point ` P ` .  (Contributed by Jim Kingdon,
+       14-Jun-2023.) $)
+    metcnpd $p |- ( ph -> ( F e. ( ( J CnP K ) ` P ) <->
+        ( F : X --> Y /\ A. y e. RR+ E. z e. RR+
+        A. w e. X ( ( P C w ) < z -> ( ( F ` P ) D ( F ` w ) ) < y ) ) ) ) $=
+      ( co cfv wcel ccnp cmopn wf cv clt wbr wi wral crp wrex wa oveq12d fveq1d
+      eleq2d cxmet wb eqid metcnp syl3anc bitrd ) AHGIJUARZSZTHGEUBSZFUBSZUARZS
+      ZTZKLHUCGDUDZERCUDUEUFGHSVHHSFRBUDUEUFUGDKUHCUIUJBUIUHUKZAVBVFHAGVAVEAIVC
+      JVDUAMNULUMUNAEKUOSTFLUOSTGKTVGVIUPOPQBCDEFGHVCVDKLVCUQVDUQURUSUT $.
+  $}
+
 
 $(
 =-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=
@@ -135815,6 +135856,31 @@ S C_ ( P ( ball ` D ) T ) ) $=
       $.
   $}
 
+  ${
+    cncfcn.2 $e |- J = ( MetOpen ` ( abs o. - ) ) $.
+    cncfcn.3 $e |- K = ( J |`t A ) $.
+    cncfcn.4 $e |- L = ( J |`t B ) $.
+    $( Relate complex function continuity to topological continuity.
+       (Contributed by Mario Carneiro, 17-Feb-2015.) $)
+    cncfcncntop $p |- ( ( A C_ CC /\ B C_ CC )
+        -> ( A -cn-> B ) = ( K Cn L ) ) $=
+      ( cc wss co cxp cres cmopn cfv ccn eqid crest wceq cnxmet ccncf cabs cmin
+      ccom cncfmet cxmet wcel simpl metrest sylancr syl5eq simpr oveq12d eqtr4d
+      wa ) AIJZBIJZUOZABUAKUBUCUDZAALMZNOZUSBBLMZNOZPKDEPKABUTVBVAVCUTQZVBQZVAQ
+      ZVCQZUEURDVAEVCPURDCARKZVAGURUSIUFOUGZUPVHVASTUPUQUHUSUTCVAIAVDFVFUIUJUKU
+      RECBRKZVCHURVIUQVJVCSTUPUQULUSVBCVCIBVEFVGUIUJUKUMUN $.
+  $}
+
+  ${
+    cncfcn1.1 $e |- J = ( MetOpen ` ( abs o. - ) ) $.
+    $( Relate complex function continuity to topological continuity.
+       (Contributed by Paul Chapman, 28-Nov-2007.)  (Revised by Mario Carneiro,
+       7-Sep-2015.)  (Revised by Jim Kingdon, 16-Jun-2023.) $)
+    cncfcn1cntop $p |- ( CC -cn-> CC ) = ( J Cn J ) $=
+      ( cc wss ccncf co ccn wceq ssid cntoptopon toponrestid cncfcncntop mp2an
+      ) CCDZNCCEFAAGFHCIZOCCAAABACABJKZPLM $.
+  $}
+
   ${
     $d x w y z A $.  $d x w y z S $.  $d x w y z T $.
     $( A constant function is a continuous function on ` CC ` .  (Contributed
@@ -136220,6 +136286,129 @@ S C_ ( P ( ball ` D ) T ) ) $=
       $.
   $}
 
+  ${
+    $d A d e z $.  $d B d e z $.  $d F d e z $.  $d J d e z $.  $d K d e z $.
+    cnplimcim.k $e |- K = ( MetOpen ` ( abs o. - ) ) $.
+    cnplimc.j $e |- J = ( K |`t A ) $.
+    $( If a function is continuous at ` B ` , its limit at ` B ` equals the
+       value of the function there.  (Contributed by Mario Carneiro,
+       28-Dec-2016.)  (Revised by Jim Kingdon, 14-Jun-2023.) $)
+    cnplimcim $p |- ( ( A C_ CC /\ B e. A )
+        -> ( F e. ( ( J CnP K ) ` B ) ->
+        ( F : A --> CC /\ ( F ` B ) e. ( F limCC B ) ) ) ) $=
+      ( vz vd ve cc wcel wa co cfv wbr cmin cabs clt crp wss wf climc ctopon wi
+      ccnp crest cntoptopon simpl resttopon sylancr syl5eqel 3expia sylancl imp
+      cnpf2 cv cap wral wrex simplr ffvelrnd ccom cxp cres simpr wb wceq simpll
+      cmopn cxmet cnxmet eqid metrest mpan syl5eq syl a1i xmetres2 syldan mpbid
+      metcnpd simprd ad3antrrr ovresd cnmetdval syl2anc abssubd biimprd adantld
+      sseldd 3eqtrd breq1d eqtrd biimpd imim12d ralimdva reximdva mpd ellimc3ap
+      mpbir2and jca ex ) AKUAZBALZMZCBDEUFNOLZAKCUBZBCOZCBUCNLZMXFXGMZXHXJXFXGX
+      HXFDAUDOZLZEKUDOLZXGXHUEXFDEAUGNZXLGXFXNXDXOXLLEFUHZXDXEUIAEKUJUKULXPXMXN
+      XGXHBCDEAKUPUMUNUOZXKXJXIKLZHUQZBURPZXSBQNROZIUQZSPZMZXSCOZXIQNROZJUQZSPZ
+      UEZHAUSZITUTZJTUSZXKAKBCXQXDXEXGVAZVBZXKBXSRQVCZAAVDVEZNZYBSPZXIYEYONZYGS
+      PZUEZHAUSZITUTZJTUSZYLXKXHUUDXKXGXHUUDMZXFXGVFXFXGXHXGUUEVGXQXFXHMZJIHYPY
+      OBCDEAKUUFXDDYPVJOZVHXDXEXHVIZXDDXOUUGGYOKVKOLZXDXOUUGVHVLYOYPEUUGKAYPVMF
+      UUGVMVNVOVPVQEYOVJOVHUUFFVRUUFUUIXDYPAVKOLVLUUHYOAKVSUKUUIUUFVLVRXDXEXHVA
+      ZWBVTWAWCXKUUCYKJTXKYGTLZMZUUBYJITUULYBTLZMZUUAYIHAUUNXSALZMZYDYRYTYHUUPY
+      CYRXTUUPYRYCUUPYQYAYBSUUPYQBXSYONZBXSQNROZYAUUPBXSYOAXKXEUUKUUMUUOYMWDUUN
+      UUOVFZWEUUPBKLZXSKLUUQUURVHXKUUTUUKUUMUUOXFXGXHUUTXQUUFAKBUUHUUJWKVTZWDZU
+      UPAKXSXKXDUUKUUMUUOXDXEXGVIZWDUUSWKZBXSYOYOVMZWFWGUUPBXSUVBUVDWHWLWMWIWJU
+      UPYTYHUUPYSYFYGSUUPYSXIYEQNROZYFUUPXRYEKLYSUVFVHXKXRUUKUUMUUOYNWDZUUPAKXS
+      CXKXHUUKUUMUUOXQWDUUSVBZXIYEYOUVEWFWGUUPXIYEUVGUVHWHWNWMWOWPWQWRWQWSXKJIH
+      ABXICXQUVCUVAWTXAXBXC $.
+  $}
+
+  ${
+    $d x A $.  $d x F $.
+    $( If ` F ` is a continuous function, the limit of the function at each
+       point equals the value of the function.  (Contributed by Mario Carneiro,
+       28-Dec-2016.)  (Revised by Jim Kingdon, 16-Jun-2023.) $)
+    cnlimcim $p |- ( A C_ CC -> ( F e. ( A -cn-> CC ) ->
+        ( F : A --> CC /\ A. x e. A ( F ` x ) e. ( F limCC x ) ) ) ) $=
+      ( cc wss ccncf co wcel wf cabs cmin ccom cmopn cfv crest wral eqid ctopon
+      cv wa ccnp climc ccn wceq cntoptopon toponrestid cncfcncntop mpan2 eleq2d
+      ssid wb resttopon mpan cncnp sylancl bitrd cnplimcim syl6 ralimdva anim2d
+      simpr sylbid ) BDEZCBDFGZHZBDCIZCASZJKLMNZBOGZVHUAGNHZABPZTZVFVGCNCVGUBGH
+      ZABPZTVCVECVIVHUCGZHZVLVCVDVOCVCDDEVDVOUDDUJBDVHVIVHVHQZVIQZVHDVHVQUEZUFU
+      GUHUIVCVIBRNHZVHDRNHZVPVLUKWAVCVTVSBVHDULUMVSACVIVHBDUNUOUPVCVKVNVFVCVJVM
+      ABVCVGBHTVJVFVMTVMBVGCVIVHVQVRUQVFVMVAURUSUTVB $.
+  $}
+
+  ${
+    $d x A $.  $d x B $.  $d x F $.
+    cnlimci.f $e |- ( ph -> F e. ( A -cn-> D ) ) $.
+    cnlimci.c $e |- ( ph -> B e. A ) $.
+    $( If ` F ` is a continuous function, then the limit of the function at any
+       point equals its value.  (Contributed by Mario Carneiro,
+       28-Dec-2016.) $)
+    cnlimci $p |- ( ph -> ( F ` B ) e. ( F limCC B ) ) $=
+      ( vx cv cfv climc co wcel wceq fveq2 cc wss ccncf syl wa eleq12d cncfrss2
+      oveq2 wral cncfrss ssid cncfss sylancl sseldd cnlimcim imp simprd syl2anc
+      wf rspcdva ) AHIZEJZEUPKLZMZCEJZECKLZMHBCUPCNUQUTURVAUPCEOUPCEKUCUAABPQZE
+      BPRLZMZUSHBUDZAEBDRLZMZVBFBDEUESAVFVCEADPQZPPQVFVCQAVGVHFBDEUBSPUFBDPUGUH
+      FUIVBVDTBPEUNZVEVBVDVIVETHBEUJUKULUMGUO $.
+  $}
+
+  ${
+    $d x A $.  $d x B $.  $d x D $.  $d x Y $.
+    cnmptlimc.f $e |- ( ph -> ( x e. A |-> X ) e. ( A -cn-> D ) ) $.
+    cnmptlimc.b $e |- ( ph -> B e. A ) $.
+    cnmptlimc.1 $e |- ( x = B -> X = Y ) $.
+    $( If ` F ` is a continuous function, then the limit of the function at any
+       point equals its value.  (Contributed by Mario Carneiro,
+       28-Dec-2016.) $)
+    cnmptlimc $p |- ( ph -> Y e. ( ( x e. A |-> X ) limCC B ) ) $=
+      ( cmpt cfv climc co eqid wcel cv wceq eleq1d wf wral ccncf cncff syl fmpt
+      sylibr rspcdva fvmptd3 cnlimci eqeltrrd ) ADBCFKZLGUKDMNABDFGCUKEUKOZJIAF
+      EPZGEPBCDBQDRFGEJSACEUKTZUMBCUAAUKCEUBNPUNHCEUKUCUDBCEFUKULUEUFIUGUHACDEU
+      KHIUIUJ $.
+  $}
+
+  ${
+    $d A p z $.  $d B d e p z $.  $d C d e p w z $.  $d D d e p w z $.
+    $d F d e p w z $.  $d G d e p w z $.  $d d e p ph z $.
+    limccnp.f $e |- ( ph -> F : A --> D ) $.
+    limccnp.d $e |- ( ph -> D C_ CC ) $.
+    limccnpcntop.k $e |- K = ( MetOpen ` ( abs o. - ) ) $.
+    limccnp.j $e |- J = ( K |`t D ) $.
+    limccnp.c $e |- ( ph -> C e. ( F limCC B ) ) $.
+    limccnp.b $e |- ( ph -> G e. ( ( J CnP K ) ` C ) ) $.
+    $( If the limit of ` F ` at ` B ` is ` C ` and ` G ` is continuous at
+       ` C ` , then the limit of ` G o. F ` at ` B ` is ` G ( C ) ` .
+       (Contributed by Mario Carneiro, 28-Dec-2016.)  (Revised by Jim Kingdon,
+       18-Jun-2023.) $)
+    limccnpcntop $p |- ( ph -> ( G ` C ) e. ( ( G o. F ) limCC B ) ) $=
+      ( cfv co wcel cc crp vz vd ve vw vp ccom climc cv cap wbr cmin cabs wa wi
+      clt wral wrex ctopon ccnp crest wss cntoptopon resttopon sylancr syl5eqel
+      wf a1i cnpf2 syl3anc ctop cntoptop cnprcl2k ffvelrnd cxp cres cmopn cxmet
+      wceq cnxmet eqid metrest syl5eq xmetres2 metcnpd mpbid simprd simplr fssd
+      simplll cdm fdmd w3a limcrcl syl simp2d eqsstr3d simp3d ellimc3ap syl2anc
+      r19.21bi oveq2 breq1d fveq2 oveq2d imbi12d simpllr ad5antr rspcdva ovresd
+      simpr simpld sseldd cnmetdval abssubd 3eqtrd fvco3 fveq2d eqeltrd 3eqtr2d
+      3imtr3d imim2d ralimdva reximdva mpd rexlimdva2 fco mpbir2and ) ADGPZGFUF
+      ZCUGQRYHSRZUAUHZCUIUJYKCUKQULPUBUHZUOUJUMZYKYIPZYHUKQULPZUCUHZUOUJZUNZUAB
+      UPZUBTUQZUCTUPZAESDGAHEURPZRZISURPRZGDHIUSQPRZESGVFZAHIEUTQZUUBMAUUDESVAZ
+      UUGUUBRILVBZKEISVCVDVEZUUDAUUIVGODGHIESVHVIZAUUCIVJRZUUEDERZUUJUULAILVKVG
+      ODGHIEVLVIZVMZADUDUHZULUKUFZEEVNVOZQZUEUHZUOUJZYHUUPGPZUUQQZYPUOUJZUNZUDE
+      UPZUETUQZUCTUPZUUAAUUFUVHAUUEUUFUVHUMOAUCUEUDUURUUQDGHIESAHUUGUURVPPZMAUU
+      QSVQPRZUUHUUGUVIVRVSKUUQUURIUVISEUURVTLUVIVTWAVDWBIUUQVPPVRALVGAUVJUUHUUR
+      EVQPRVSKUUQESWCVDUVJAVSVGUUNWDWEWFAUVGYTUCTAYPTRZUMZUVFYTUETUVLUUTTRZUMZU
+      VFUMZYMYKFPZDUKQULPZUUTUOUJZUNZUABUPZUBTUQZYTUVOAUVMUWAAUVKUVMUVFWIUVLUVM
+      UVFWGAUWAUETADSRZUWAUETUPZADFCUGQRZUWBUWCUMNAUEUBUABCDFABESFJKWHABFWJZSAB
+      EFJWKAUWESFVFZUWESVAZCSRZAUWDUWFUWGUWHWLNCDFWMWNZWOWPZAUWFUWGUWHUWIWQZWRW
+      EZWFWTWSUVOUVTYSUBTUVOYLTRZUMZUVSYRUABUWNYKBRZUMZUVRYQYMUWPDUVPUURQZUUTUO
+      UJZYHUVPGPZUUQQZYPUOUJZUVRYQUWPUVEUWRUXAUNUDEUVPUUPUVPVRZUVAUWRUVDUXAUXBU
+      USUWQUUTUOUUPUVPDUURXAXBUXBUVCUWTYPUOUXBUVBUWSYHUUQUUPUVPGXCXDXBXEUVNUVFU
+      WMUWOXFUWPBEYKFABEFVFZUVKUVMUVFUWMUWOJXGZUWNUWOXJZVMZXHUWPUWQUVQUUTUOUWPU
+      WQDUVPUUQQZDUVPUKQULPZUVQUWPDUVPUUQEAUUMUVKUVMUVFUWMUWOUUNXGUXFXIUWPUWBUV
+      PSRUXGUXHVRAUWBUVKUVMUVFUWMUWOAUWBUWCUWLXKXGZUWPESUVPAUUHUVKUVMUVFUWMUWOK
+      XGUXFXLZDUVPUUQUUQVTZXMWSUWPDUVPUXIUXJXNXOXBUWPUWTYOYPUOUWPUWTYHUWSUKQZUL
+      PZYHYNUKQZULPYOUWPYJUWSSRUWTUXMVRAYJUVKUVMUVFUWMUWOUUOXGZUWPESUVPGAUUFUVK
+      UVMUVFUWMUWOUUKXGUXFVMZYHUWSUUQUXKXMWSUWPUXNUXLULUWPYNUWSYHUKUWPUXCUWOYNU
+      WSVRUXDUXEBEYKGFXPWSZXDXQUWPYHYNUXOUWPYNUWSSUXQUXPXRXNXSXBXTYAYBYCYDYEYBY
+      DAUCUBUABCYHYIAUUFUXCBSYIVFUUKJBESGFYFWSUWJUWKWRYG $.
+  $}
+
 
 $(
 ###############################################################################

mmil.raw.html

@@ -10106,6 +10106,16 @@
   <TD>~ divccncfap</TD>
 </TR>
 
+<tr>
+  <td>cncfcn</td>
+  <td>~ cncfcncntop</td>
+</tr>
+
+<tr>
+  <td>cncfcn1</td>
+  <td>~ cncfcn1cntop</td>
+</tr>
+
 <tr>
   <td>cdivcncf</td>
   <td>~ cdivcncfap</td>
@@ -10149,6 +10159,42 @@
   <td><i>none</i></td>
 </tr>
 
+<tr>
+  <td>limcres</td>
+  <td><i>none</i></td>
+  <td>Although this would appear to be provable,
+  it might benefit from some additional theorems which
+  help us manipulate ` |``t ` and metric spaces.
+  If iset.mm doesn't have CCfld yet, use
+  ` ( MetOpen `` ( abs o. - ) ) ` for the topology of the
+  complex numbers (see cnfldtopn in set.mm).
+  Proof sketch: because interiors are open, we can form
+  a ball around ` B ` which is contained in
+  ` ( ( int `` J ) `` ( C u. { B } ) ) ` which gives
+  us the delta we need to apply ~ ellimc3ap for
+  ` ( F limCC B ) ` (given that we can apply
+  ~ ellimc3ap for ` ( ( F |`` C ) limCC B ) ` when
+  working within ` C ` ).</td>
+</tr>
+
+<tr>
+  <td>cnplimc</td>
+  <td>~ cnplimcim</td>
+  <td>The converse is conjectured to also be provable, but
+  would require a more involved proof.</td>
+</tr>
+
+<tr>
+  <td>cnlimc</td>
+  <td>~ cnlimcim</td>
+  <td>See cnplimc concerning biconditionalizing this</td>
+</tr>
+
+<tr>
+  <td>limccnp</td>
+  <td>~ limccnpcntop</td>
+</tr>
+
 </TABLE>
 
 <HR NOSHADE SIZE=1><A NAME="bib"></A><B><FONT