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

Theorem cnf2 18812
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 18798 . . 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 620 . 2  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  F  e.  ( J  Cn  K
) )  ->  F : X --> Y )
323impa 1177 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 369    /\ w3a 960    e. wcel 1761   A.wral 2713   `'ccnv 4835   "cima 4839   -->wf 5411   ` cfv 5415  (class class class)co 6090  TopOnctopon 18458    Cn ccn 18787
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2261  df-mo 2262  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-sbc 3184  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-op 3881  df-uni 4089  df-br 4290  df-opab 4348  df-mpt 4349  df-id 4632  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-map 7212  df-top 18462  df-topon 18465  df-cn 18790
This theorem is referenced by:  iscncl  18832  cncls2  18836  cncls  18837  cnntr  18838  cnrest2  18849  cnrest2r  18850  ptcn  19159  txdis1cn  19167  lmcn2  19181  cnmpt11  19195  cnmpt1t  19197  cnmpt12  19199  cnmpt21  19203  cnmpt2t  19205  cnmpt22  19206  cnmpt22f  19207  cnmptcom  19210  cnmptkp  19212  cnmptk1  19213  cnmpt1k  19214  cnmptkk  19215  cnmptk1p  19217  cnmptk2  19218  cnmpt2k  19220  qtopss  19247  qtopeu  19248  qtopomap  19250  qtopcmap  19251  hmeof1o2  19295  xpstopnlem1  19341  xkocnv  19346  xkohmeo  19347  qtophmeo  19349  cnmpt1plusg  19617  cnmpt2plusg  19618  tsmsmhm  19679  cnmpt1vsca  19727  cnmpt2vsca  19728  cnmpt1ds  20378  cnmpt2ds  20379  fsumcn  20405  cnmpt2pc  20459  htpyco1  20509  htpyco2  20510  phtpyco2  20521  pi1xfrf  20584  pi1xfr  20586  pi1xfrcnvlem  20587  pi1xfrcnv  20588  pi1cof  20590  pi1coghm  20592  cnmpt1ip  20718  cnmpt2ip  20719  txsconlem  27059  txscon  27060  cvmlift3lem6  27143  fcnre  29672  refsumcn  29677  refsum2cnlem1  29684
  Copyright terms: Public domain W3C validator