Add cncfmpt2fcntop to iset.mm

This is cncfmpt2f from set.mm with different notation for the topology
on the complex numbers.  The proof is otherwise very similar.

Author: jkingdon

iset.mm

@@ -139749,6 +139749,23 @@ S C_ ( P ( ball ` D ) T ) ) $=
       LLDSTUEUMCDUFUGAELLUJDGFUHUI $.
   $}
 
+  ${
+    $d x F $.  $d x J $.  $d x ph $.  $d x X $.
+    cncfmpt2fcntop.1 $e |- J = ( MetOpen ` ( abs o. - ) ) $.
+    cncfmpt2f.2 $e |- ( ph -> F e. ( ( J tX J ) Cn J ) ) $.
+    cncfmpt2f.3 $e |- ( ph -> ( x e. X |-> A ) e. ( X -cn-> CC ) ) $.
+    cncfmpt2f.4 $e |- ( ph -> ( x e. X |-> B ) e. ( X -cn-> CC ) ) $.
+    $( Composition of continuous functions. ` -cn-> ` analogue of ~ cnmpt12f .
+       (Contributed by Mario Carneiro, 3-Sep-2014.) $)
+    cncfmpt2fcntop $p |- ( ph
+        -> ( x e. X |-> ( A F B ) ) e. ( X -cn-> CC ) ) $=
+      ( co cmpt crest cc ctopon cfv wcel wss eleqtrd ccn cntoptopon cncfrss syl
+      resttopon sylancr wceq ssid eqid toponrestid cncfcncntop sylancl cnmpt12f
+      ccncf eleqtrrd ) ABGCDELMFGNLZFUALZGOUNLZABCDEUPFFFGAFOPQRGOSZUPGPQRFHUBZ
+      ABGCMZURRUSJGOVAUCUDZGFOUEUFAVAURUQJAUSOOSURUQUGVBOUHGOFUPFHUPUIFOUTUJUKU
+      LZTABGDMURUQKVCTIUMVCUO $.
+  $}
+
   ${
     $d A x w y z $.  $d F w y z $.
     addccncf.1 $e |- F = ( x e. CC |-> ( x + A ) ) $.

mmil.raw.html

@@ -10763,6 +10763,11 @@
   <td>~ cncfcn1cntop</td>
 </tr>
 
+<tr>
+  <td>cncfmpt2f</td>
+  <td>~ cncfmpt2fcntop</td>
+</tr>
+
 <tr>
   <td>cdivcncf</td>
   <td>~ cdivcncfap</td>
@@ -10987,7 +10992,7 @@
 <tr>
   <td>dvcnp2</td>
   <td><i>none</i></td>
-  <td>The set.mm proof relies on subcn , mulcn , cncfmpt2f , limccnp2 ,
+  <td>The set.mm proof relies on limccnp2
   and the converse of ~ cnplimcim</td>
 </tr>