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

Theorem cnf 20204
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 20196 . . 3  |-  ( F  e.  ( J  Cn  K )  <->  ( ( J  e.  Top  /\  K  e.  Top )  /\  ( F : X --> Y  /\  A. x  e.  K  ( `' F " x )  e.  J ) ) )
43simprbi 465 . 2  |-  ( F  e.  ( J  Cn  K )  ->  ( F : X --> Y  /\  A. x  e.  K  ( `' F " x )  e.  J ) )
54simpld 460 1  |-  ( F  e.  ( J  Cn  K )  ->  F : X --> Y )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    = wceq 1437    e. wcel 1872   A.wral 2714   U.cuni 4162   `'ccnv 4795   "cima 4799   -->wf 5540  (class class class)co 6249   Topctop 19859    Cn ccn 20182
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-br 4367  df-opab 4426  df-mpt 4427  df-id 4711  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-fv 5552  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-map 7429  df-top 19863  df-topon 19865  df-cn 20185
This theorem is referenced by:  cnco  20224  cnclima  20226  cnntri  20229  cnclsi  20230  cnss1  20234  cnss2  20235  cncnpi  20236  cncnp2  20239  cnrest  20243  cnrest2  20244  cnt0  20304  cnt1  20308  cnhaus  20312  dnsconst  20336  cncmp  20349  rncmp  20353  imacmp  20354  cnconn  20379  conima  20382  concn  20383  2ndcomap  20415  kgencn2  20514  kgencn3  20515  txcnmpt  20581  uptx  20582  txcn  20583  hauseqlcld  20603  xkohaus  20610  xkoptsub  20611  xkopjcn  20613  xkoco1cn  20614  xkoco2cn  20615  xkococnlem  20616  cnmpt11f  20621  cnmpt21f  20629  hmeocnv  20719  hmeores  20728  txhmeo  20760  cnextfres  21026  bndth  21928  evth  21929  evth2  21930  htpyco2  21952  phtpyco2  21963  reparphti  21970  copco  21991  pcopt  21995  pcopt2  21996  pcoass  21997  pcorevlem  21999  pcorev2  22001  hauseqcn  28653  pl1cn  28713  rrhf  28754  esumcocn  28853  cnmbfm  29037  cnpcon  29905  ptpcon  29908  sconpi1  29914  txsconlem  29915  cvxscon  29918  cvmseu  29951  cvmopnlem  29953  cvmfolem  29954  cvmliftmolem1  29956  cvmliftmolem2  29957  cvmliftlem3  29962  cvmliftlem6  29965  cvmliftlem7  29966  cvmliftlem8  29967  cvmliftlem9  29968  cvmliftlem10  29969  cvmliftlem11  29970  cvmliftlem13  29971  cvmliftlem15  29973  cvmlift2lem3  29980  cvmlift2lem5  29982  cvmlift2lem7  29984  cvmlift2lem9  29986  cvmlift2lem10  29987  cvmliftphtlem  29992  cvmlift3lem1  29994  cvmlift3lem2  29995  cvmlift3lem4  29997  cvmlift3lem5  29998  cvmlift3lem6  29999  cvmlift3lem7  30000  cvmlift3lem8  30001  cvmlift3lem9  30002  poimirlem31  31878  poimir  31880  broucube  31881  cnres2  32002  cnresima  32003  hausgraph  36002  refsum2cnlem1  37274  itgsubsticclem  37735  stoweidlem62  37806  stoweidlem62OLD  37807
  Copyright terms: Public domain W3C validator