MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  cnf2 Structured version   Unicode version

Theorem cnf2 19836
Description: A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.)
Assertion
Ref Expression
cnf2  |-  ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )  /\  F  e.  ( J  Cn  K ) )  ->  F : X --> Y )

Proof of Theorem cnf2
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 iscn 19822 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  ->  ( F  e.  ( J  Cn  K
)  <->  ( F : X
--> Y  /\  A. x  e.  K  ( `' F " x )  e.  J ) ) )
21simprbda 621 . 2  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  F  e.  ( J  Cn  K
) )  ->  F : X --> Y )
323impa 1189 1  |-  ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )  /\  F  e.  ( J  Cn  K ) )  ->  F : X --> Y )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    /\ w3a 971    e. wcel 1826   A.wral 2732   `'ccnv 4912   "cima 4916   -->wf 5492   ` cfv 5496  (class class class)co 6196  TopOnctopon 19480    Cn ccn 19811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-rab 2741  df-v 3036  df-sbc 3253  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-op 3951  df-uni 4164  df-br 4368  df-opab 4426  df-mpt 4427  df-id 4709  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-fv 5504  df-ov 6199  df-oprab 6200  df-mpt2 6201  df-map 7340  df-top 19484  df-topon 19487  df-cn 19814
This theorem is referenced by:  iscncl  19856  cncls2  19860  cncls  19861  cnntr  19862  cnrest2  19873  cnrest2r  19874  ptcn  20213  txdis1cn  20221  lmcn2  20235  cnmpt11  20249  cnmpt1t  20251  cnmpt12  20253  cnmpt21  20257  cnmpt2t  20259  cnmpt22  20260  cnmpt22f  20261  cnmptcom  20264  cnmptkp  20266  cnmptk1  20267  cnmpt1k  20268  cnmptkk  20269  cnmptk1p  20271  cnmptk2  20272  cnmpt2k  20274  qtopss  20301  qtopeu  20302  qtopomap  20304  qtopcmap  20305  hmeof1o2  20349  xpstopnlem1  20395  xkocnv  20400  xkohmeo  20401  qtophmeo  20403  cnmpt1plusg  20671  cnmpt2plusg  20672  tsmsmhm  20733  cnmpt1vsca  20781  cnmpt2vsca  20782  cnmpt1ds  21432  cnmpt2ds  21433  fsumcn  21459  cnmpt2pc  21513  htpyco1  21563  htpyco2  21564  phtpyco2  21575  pi1xfrf  21638  pi1xfr  21640  pi1xfrcnvlem  21641  pi1xfrcnv  21642  pi1cof  21644  pi1coghm  21646  cnmpt1ip  21772  cnmpt2ip  21773  txsconlem  28874  txscon  28875  cvmlift3lem6  28958  fcnre  31567  refsumcn  31572  refsum2cnlem1  31579  icccncfext  31856  itgsubsticclem  31940
  Copyright terms: Public domain W3C validator