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

Theorem cnf2 18853
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 18839 . . 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 623 . 2  |-  ( ( ( J  e.  (TopOn `  X )  /\  K  e.  (TopOn `  Y )
)  /\  F  e.  ( J  Cn  K
) )  ->  F : X --> Y )
323impa 1182 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 965    e. wcel 1756   A.wral 2715   `'ccnv 4839   "cima 4843   -->wf 5414   ` cfv 5418  (class class class)co 6091  TopOnctopon 18499    Cn ccn 18828
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-rab 2724  df-v 2974  df-sbc 3187  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-op 3884  df-uni 4092  df-br 4293  df-opab 4351  df-mpt 4352  df-id 4636  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-fv 5426  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-map 7216  df-top 18503  df-topon 18506  df-cn 18831
This theorem is referenced by:  iscncl  18873  cncls2  18877  cncls  18878  cnntr  18879  cnrest2  18890  cnrest2r  18891  ptcn  19200  txdis1cn  19208  lmcn2  19222  cnmpt11  19236  cnmpt1t  19238  cnmpt12  19240  cnmpt21  19244  cnmpt2t  19246  cnmpt22  19247  cnmpt22f  19248  cnmptcom  19251  cnmptkp  19253  cnmptk1  19254  cnmpt1k  19255  cnmptkk  19256  cnmptk1p  19258  cnmptk2  19259  cnmpt2k  19261  qtopss  19288  qtopeu  19289  qtopomap  19291  qtopcmap  19292  hmeof1o2  19336  xpstopnlem1  19382  xkocnv  19387  xkohmeo  19388  qtophmeo  19390  cnmpt1plusg  19658  cnmpt2plusg  19659  tsmsmhm  19720  cnmpt1vsca  19768  cnmpt2vsca  19769  cnmpt1ds  20419  cnmpt2ds  20420  fsumcn  20446  cnmpt2pc  20500  htpyco1  20550  htpyco2  20551  phtpyco2  20562  pi1xfrf  20625  pi1xfr  20627  pi1xfrcnvlem  20628  pi1xfrcnv  20629  pi1cof  20631  pi1coghm  20633  cnmpt1ip  20759  cnmpt2ip  20760  txsconlem  27129  txscon  27130  cvmlift3lem6  27213  fcnre  29747  refsumcn  29752  refsum2cnlem1  29759
  Copyright terms: Public domain W3C validator