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

Theorem cnf 18694
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 18686 . . 3  |-  ( F  e.  ( J  Cn  K )  <->  ( ( J  e.  Top  /\  K  e.  Top )  /\  ( F : X --> Y  /\  A. x  e.  K  ( `' F " x )  e.  J ) ) )
43simprbi 461 . 2  |-  ( F  e.  ( J  Cn  K )  ->  ( F : X --> Y  /\  A. x  e.  K  ( `' F " x )  e.  J ) )
54simpld 456 1  |-  ( F  e.  ( J  Cn  K )  ->  F : X --> Y )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1364    e. wcel 1757   A.wral 2707   U.cuni 4081   `'ccnv 4828   "cima 4832   -->wf 5404  (class class class)co 6082   Topctop 18342    Cn ccn 18672
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 1671  ax-6 1709  ax-7 1729  ax-8 1759  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pow 4460  ax-pr 4521  ax-un 6363
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 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2966  df-sbc 3178  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-nul 3628  df-if 3782  df-pw 3852  df-sn 3868  df-pr 3870  df-op 3874  df-uni 4082  df-br 4283  df-opab 4341  df-mpt 4342  df-id 4625  df-xp 4835  df-rel 4836  df-cnv 4837  df-co 4838  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842  df-iota 5371  df-fun 5410  df-fn 5411  df-f 5412  df-fv 5416  df-ov 6085  df-oprab 6086  df-mpt2 6087  df-map 7206  df-top 18347  df-topon 18350  df-cn 18675
This theorem is referenced by:  cnco  18714  cnclima  18716  cnntri  18719  cnclsi  18720  cnss1  18724  cnss2  18725  cncnpi  18726  cncnp2  18729  cnrest  18733  cnrest2  18734  cnt0  18794  cnt1  18798  cnhaus  18802  dnsconst  18826  cncmp  18839  rncmp  18843  imacmp  18844  cnconn  18870  conima  18873  concn  18874  2ndcomap  18906  kgencn2  18974  kgencn3  18975  txcnmpt  19041  uptx  19042  txcn  19043  hauseqlcld  19063  xkohaus  19070  xkoptsub  19071  xkopjcn  19073  xkoco1cn  19074  xkoco2cn  19075  xkococnlem  19076  cnmpt11f  19081  cnmpt21f  19089  hmeocnv  19179  hmeores  19188  txhmeo  19220  bndth  20374  evth  20375  evth2  20376  htpyco2  20395  phtpyco2  20406  reparphti  20413  copco  20434  pcopt  20438  pcopt2  20439  pcoass  20440  pcorevlem  20442  pcorev2  20444  hauseqcn  26181  pl1cn  26241  rrhf  26283  esumcocn  26385  cnmbfm  26534  cnpcon  26969  ptpcon  26972  sconpi1  26978  txsconlem  26979  cvxscon  26982  cvmseu  27015  cvmopnlem  27017  cvmfolem  27018  cvmliftmolem1  27020  cvmliftmolem2  27021  cvmliftlem3  27026  cvmliftlem6  27029  cvmliftlem7  27030  cvmliftlem8  27031  cvmliftlem9  27032  cvmliftlem10  27033  cvmliftlem11  27034  cvmliftlem13  27035  cvmliftlem15  27037  cvmlift2lem3  27044  cvmlift2lem5  27046  cvmlift2lem7  27048  cvmlift2lem9  27050  cvmlift2lem10  27051  cvmliftphtlem  27056  cvmlift3lem1  27058  cvmlift3lem2  27059  cvmlift3lem4  27061  cvmlift3lem5  27062  cvmlift3lem6  27063  cvmlift3lem7  27064  cvmlift3lem8  27065  cvmlift3lem9  27066  cnres2  28508  cnresima  28509  hausgraph  29427  refsum2cnlem1  29606  stoweidlem62  29705
  Copyright terms: Public domain W3C validator