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

Theorem cnf 18850
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 18842 . . 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 1369    e. wcel 1756   A.wral 2715   U.cuni 4091   `'ccnv 4839   "cima 4843   -->wf 5414  (class class class)co 6091   Topctop 18498    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:  cnco  18870  cnclima  18872  cnntri  18875  cnclsi  18876  cnss1  18880  cnss2  18881  cncnpi  18882  cncnp2  18885  cnrest  18889  cnrest2  18890  cnt0  18950  cnt1  18954  cnhaus  18958  dnsconst  18982  cncmp  18995  rncmp  18999  imacmp  19000  cnconn  19026  conima  19029  concn  19030  2ndcomap  19062  kgencn2  19130  kgencn3  19131  txcnmpt  19197  uptx  19198  txcn  19199  hauseqlcld  19219  xkohaus  19226  xkoptsub  19227  xkopjcn  19229  xkoco1cn  19230  xkoco2cn  19231  xkococnlem  19232  cnmpt11f  19237  cnmpt21f  19245  hmeocnv  19335  hmeores  19344  txhmeo  19376  bndth  20530  evth  20531  evth2  20532  htpyco2  20551  phtpyco2  20562  reparphti  20569  copco  20590  pcopt  20594  pcopt2  20595  pcoass  20596  pcorevlem  20598  pcorev2  20600  hauseqcn  26325  pl1cn  26385  rrhf  26427  esumcocn  26529  cnmbfm  26678  cnpcon  27119  ptpcon  27122  sconpi1  27128  txsconlem  27129  cvxscon  27132  cvmseu  27165  cvmopnlem  27167  cvmfolem  27168  cvmliftmolem1  27170  cvmliftmolem2  27171  cvmliftlem3  27176  cvmliftlem6  27179  cvmliftlem7  27180  cvmliftlem8  27181  cvmliftlem9  27182  cvmliftlem10  27183  cvmliftlem11  27184  cvmliftlem13  27185  cvmliftlem15  27187  cvmlift2lem3  27194  cvmlift2lem5  27196  cvmlift2lem7  27198  cvmlift2lem9  27200  cvmlift2lem10  27201  cvmliftphtlem  27206  cvmlift3lem1  27208  cvmlift3lem2  27209  cvmlift3lem4  27211  cvmlift3lem5  27212  cvmlift3lem6  27213  cvmlift3lem7  27214  cvmlift3lem8  27215  cvmlift3lem9  27216  cnres2  28662  cnresima  28663  hausgraph  29580  refsum2cnlem1  29759  stoweidlem62  29857
  Copyright terms: Public domain W3C validator