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

Theorem cnf 21784
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 21776 . . 3 (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝑋𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽)))
43simprbi 497 . 2 (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:𝑋𝑌 ∧ ∀𝑥𝐾 (𝐹𝑥) ∈ 𝐽))
54simpld 495 1 (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋𝑌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1528  wcel 2105  wral 3138   cuni 4832  ccnv 5548  cima 5552  wf 6345  (class class class)co 7145  Topctop 21431   Cn ccn 21762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pow 5258  ax-pr 5321  ax-un 7450
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-mo 2618  df-eu 2650  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ral 3143  df-rex 3144  df-rab 3147  df-v 3497  df-sbc 3772  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-op 4566  df-uni 4833  df-br 5059  df-opab 5121  df-mpt 5139  df-id 5454  df-xp 5555  df-rel 5556  df-cnv 5557  df-co 5558  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562  df-iota 6308  df-fun 6351  df-fn 6352  df-f 6353  df-fv 6357  df-ov 7148  df-oprab 7149  df-mpo 7150  df-map 8398  df-top 21432  df-topon 21449  df-cn 21765
This theorem is referenced by:  cnco  21804  cnclima  21806  cnntri  21809  cnclsi  21810  cnss1  21814  cnss2  21815  cncnpi  21816  cncnp2  21819  cnrest  21823  cnrest2  21824  cnt0  21884  cnt1  21888  cnhaus  21892  dnsconst  21916  cncmp  21930  rncmp  21934  imacmp  21935  cnconn  21960  connima  21963  conncn  21964  2ndcomap  21996  kgencn2  22095  kgencn3  22096  txcnmpt  22162  uptx  22163  txcn  22164  hauseqlcld  22184  xkohaus  22191  xkoptsub  22192  xkopjcn  22194  xkoco1cn  22195  xkoco2cn  22196  xkococnlem  22197  cnmpt11f  22202  cnmpt21f  22210  hmeocnv  22300  hmeores  22309  txhmeo  22341  cnextfres  22607  bndth  23491  evth  23492  evth2  23493  htpyco2  23512  phtpyco2  23523  reparphti  23530  copco  23551  pcopt  23555  pcopt2  23556  pcoass  23557  pcorevlem  23559  pcorev2  23561  hauseqcn  31038  pl1cn  31098  rrhf  31139  esumcocn  31239  cnmbfm  31421  cnpconn  32375  ptpconn  32378  sconnpi1  32384  txsconnlem  32385  cvxsconn  32388  cvmseu  32421  cvmopnlem  32423  cvmfolem  32424  cvmliftmolem1  32426  cvmliftmolem2  32427  cvmliftlem3  32432  cvmliftlem6  32435  cvmliftlem7  32436  cvmliftlem8  32437  cvmliftlem9  32438  cvmliftlem10  32439  cvmliftlem11  32440  cvmliftlem13  32441  cvmliftlem15  32443  cvmlift2lem3  32450  cvmlift2lem5  32452  cvmlift2lem7  32454  cvmlift2lem9  32456  cvmlift2lem10  32457  cvmliftphtlem  32462  cvmlift3lem1  32464  cvmlift3lem2  32465  cvmlift3lem4  32467  cvmlift3lem5  32468  cvmlift3lem6  32469  cvmlift3lem7  32470  cvmlift3lem8  32471  cvmlift3lem9  32472  poimirlem31  34805  poimir  34807  broucube  34808  cnres2  34924  cnresima  34925  hausgraph  39692  refsum2cnlem1  41174  itgsubsticclem  42140  stoweidlem62  42228  cnfsmf  42898
  Copyright terms: Public domain W3C validator