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

Theorem cnf 21855
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 𝑋 = 𝐽
iscnp2.2 𝑌 = 𝐾
Assertion
Ref Expression
cnf (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋𝑌)

Proof of Theorem cnf
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 iscnp2.1 . . . 4 𝑋 = 𝐽
2 iscnp2.2 . . . 4 𝑌 = 𝐾
31, 2iscn2 21847 . . 3 (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
43simprbi 500 . 2 (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:𝑋𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽))
54simpld 498 1 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋𝑌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399   = wceq 1538  wcel 2112  wral 3109   cuni 4803  ccnv 5522  cima 5526  wf 6324  (class class class)co 7139  Topctop 21502   Cn ccn 21833
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2773  ax-sep 5170  ax-nul 5177  ax-pow 5234  ax-pr 5298  ax-un 7445
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2601  df-eu 2632  df-clab 2780  df-cleq 2794  df-clel 2873  df-nfc 2941  df-ral 3114  df-rex 3115  df-rab 3118  df-v 3446  df-sbc 3724  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4804  df-br 5034  df-opab 5096  df-mpt 5114  df-id 5428  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-res 5535  df-ima 5536  df-iota 6287  df-fun 6330  df-fn 6331  df-f 6332  df-fv 6336  df-ov 7142  df-oprab 7143  df-mpo 7144  df-map 8395  df-top 21503  df-topon 21520  df-cn 21836
This theorem is referenced by:  cnco  21875  cnclima  21877  cnntri  21880  cnclsi  21881  cnss1  21885  cnss2  21886  cncnpi  21887  cncnp2  21890  cnrest  21894  cnrest2  21895  cnt0  21955  cnt1  21959  cnhaus  21963  dnsconst  21987  cncmp  22001  rncmp  22005  imacmp  22006  cnconn  22031  connima  22034  conncn  22035  2ndcomap  22067  kgencn2  22166  kgencn3  22167  txcnmpt  22233  uptx  22234  txcn  22235  hauseqlcld  22255  xkohaus  22262  xkoptsub  22263  xkopjcn  22265  xkoco1cn  22266  xkoco2cn  22267  xkococnlem  22268  cnmpt11f  22273  cnmpt21f  22281  hmeocnv  22371  hmeores  22380  txhmeo  22412  cnextfres  22678  bndth  23567  evth  23568  evth2  23569  htpyco2  23588  phtpyco2  23599  reparphti  23606  copco  23627  pcopt  23631  pcopt2  23632  pcoass  23633  pcorevlem  23635  pcorev2  23637  hauseqcn  31255  pl1cn  31312  rrhf  31353  esumcocn  31453  cnmbfm  31635  cnpconn  32591  ptpconn  32594  sconnpi1  32600  txsconnlem  32601  cvxsconn  32604  cvmseu  32637  cvmopnlem  32639  cvmfolem  32640  cvmliftmolem1  32642  cvmliftmolem2  32643  cvmliftlem3  32648  cvmliftlem6  32651  cvmliftlem7  32652  cvmliftlem8  32653  cvmliftlem9  32654  cvmliftlem10  32655  cvmliftlem11  32656  cvmliftlem13  32657  cvmliftlem15  32659  cvmlift2lem3  32666  cvmlift2lem5  32668  cvmlift2lem7  32670  cvmlift2lem9  32672  cvmlift2lem10  32673  cvmliftphtlem  32678  cvmlift3lem1  32680  cvmlift3lem2  32681  cvmlift3lem4  32683  cvmlift3lem5  32684  cvmlift3lem6  32685  cvmlift3lem7  32686  cvmlift3lem8  32687  cvmlift3lem9  32688  poimirlem31  35087  poimir  35089  broucube  35090  cnres2  35200  cnresima  35201  hausgraph  40153  refsum2cnlem1  41663  itgsubsticclem  42614  stoweidlem62  42701  cnfsmf  43371
  Copyright terms: Public domain W3C validator