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

Theorem cnf 19874
Description: A continuous function is a mapping. (Contributed by FL, 8-Dec-2006.) (Revised by Mario Carneiro, 21-Aug-2015.)
Hypotheses
Ref Expression
iscnp2.1  |-  X  = 
U. J
iscnp2.2  |-  Y  = 
U. K
Assertion
Ref Expression
cnf  |-  ( F  e.  ( J  Cn  K )  ->  F : X --> Y )

Proof of Theorem cnf
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 iscnp2.1 . . . 4  |-  X  = 
U. J
2 iscnp2.2 . . . 4  |-  Y  = 
U. K
31, 2iscn2 19866 . . 3  |-  ( F  e.  ( J  Cn  K )  <->  ( ( J  e.  Top  /\  K  e.  Top )  /\  ( F : X --> Y  /\  A. x  e.  K  ( `' F " x )  e.  J ) ) )
43simprbi 464 . 2  |-  ( F  e.  ( J  Cn  K )  ->  ( F : X --> Y  /\  A. x  e.  K  ( `' F " x )  e.  J ) )
54simpld 459 1  |-  ( F  e.  ( J  Cn  K )  ->  F : X --> Y )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1395    e. wcel 1819   A.wral 2807   U.cuni 4251   `'ccnv 5007   "cima 5011   -->wf 5590  (class class class)co 6296   Topctop 19521    Cn ccn 19852
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-8 1821  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pow 4634  ax-pr 4695  ax-un 6591
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-eu 2287  df-mo 2288  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-sbc 3328  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4252  df-br 4457  df-opab 4516  df-mpt 4517  df-id 4804  df-xp 5014  df-rel 5015  df-cnv 5016  df-co 5017  df-dm 5018  df-rn 5019  df-res 5020  df-ima 5021  df-iota 5557  df-fun 5596  df-fn 5597  df-f 5598  df-fv 5602  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-map 7440  df-top 19526  df-topon 19529  df-cn 19855
This theorem is referenced by:  cnco  19894  cnclima  19896  cnntri  19899  cnclsi  19900  cnss1  19904  cnss2  19905  cncnpi  19906  cncnp2  19909  cnrest  19913  cnrest2  19914  cnt0  19974  cnt1  19978  cnhaus  19982  dnsconst  20006  cncmp  20019  rncmp  20023  imacmp  20024  cnconn  20049  conima  20052  concn  20053  2ndcomap  20085  kgencn2  20184  kgencn3  20185  txcnmpt  20251  uptx  20252  txcn  20253  hauseqlcld  20273  xkohaus  20280  xkoptsub  20281  xkopjcn  20283  xkoco1cn  20284  xkoco2cn  20285  xkococnlem  20286  cnmpt11f  20291  cnmpt21f  20299  hmeocnv  20389  hmeores  20398  txhmeo  20430  bndth  21584  evth  21585  evth2  21586  htpyco2  21605  phtpyco2  21616  reparphti  21623  copco  21644  pcopt  21648  pcopt2  21649  pcoass  21650  pcorevlem  21652  pcorev2  21654  hauseqcn  28038  pl1cn  28098  rrhf  28140  esumcocn  28252  cnmbfm  28407  cnpcon  28872  ptpcon  28875  sconpi1  28881  txsconlem  28882  cvxscon  28885  cvmseu  28918  cvmopnlem  28920  cvmfolem  28921  cvmliftmolem1  28923  cvmliftmolem2  28924  cvmliftlem3  28929  cvmliftlem6  28932  cvmliftlem7  28933  cvmliftlem8  28934  cvmliftlem9  28935  cvmliftlem10  28936  cvmliftlem11  28937  cvmliftlem13  28938  cvmliftlem15  28940  cvmlift2lem3  28947  cvmlift2lem5  28949  cvmlift2lem7  28951  cvmlift2lem9  28953  cvmlift2lem10  28954  cvmliftphtlem  28959  cvmlift3lem1  28961  cvmlift3lem2  28962  cvmlift3lem4  28964  cvmlift3lem5  28965  cvmlift3lem6  28966  cvmlift3lem7  28967  cvmlift3lem8  28968  cvmlift3lem9  28969  cnres2  30443  cnresima  30444  hausgraph  31355  refsum2cnlem1  31594  itgsubsticclem  31956  stoweidlem62  32026
  Copyright terms: Public domain W3C validator