Theorem cnf 23169

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.

Step	Hyp	Ref	Expression
1		iscnp2.1	. . . 4 ⊢ 𝑋 = ∪ 𝐽
2		iscnp2.2	. . . 4 ⊢ 𝑌 = ∪ 𝐾
3	1, 2	iscn2 23161	. . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)))
4	3	simprbi 496	. 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))
5	4	simpld 494	1 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶𝑌)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∀wral 3050  ∪ cuni 4880  ^◡ccnv 5650   “ cima 5654  ⟶wf 6523  (class class class)co 7399  Topctop 22816   Cn ccn 23147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-sep 5263  ax-nul 5273  ax-pow 5332  ax-pr 5399  ax-un 7723

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3414  df-v 3459  df-sbc 3764  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-br 5117  df-opab 5179  df-mpt 5199  df-id 5545  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-fv 6535  df-ov 7402  df-oprab 7403  df-mpo 7404  df-map 8836  df-top 22817  df-topon 22834  df-cn 23150

This theorem is referenced by:  cnco  23189  cnclima  23191  cnntri  23194  cnclsi  23195  cnss1  23199  cnss2  23200  cncnpi  23201  cncnp2  23204  cnrest  23208  cnrest2  23209  cnt0  23269  cnt1  23273  cnhaus  23277  dnsconst  23301  cncmp  23315  rncmp  23319  imacmp  23320  cnconn  23345  connima  23348  conncn  23349  2ndcomap  23381  kgencn2  23480  kgencn3  23481  txcnmpt  23547  uptx  23548  txcn  23549  hauseqlcld  23569  xkohaus  23576  xkoptsub  23577  xkopjcn  23579  xkoco1cn  23580  xkoco2cn  23581  xkococnlem  23582  cnmpt11f  23587  cnmpt21f  23595  hmeocnv  23685  hmeores  23694  txhmeo  23726  cnextfres  23992  bndth  24893  evth  24894  evth2  24895  htpyco2  24914  phtpyco2  24925  reparphti  24932  reparphtiOLD  24933  copco  24954  pcopt  24958  pcopt2  24959  pcoass  24960  pcorevlem  24962  pcorev2  24964  hauseqcn  33837  pl1cn  33894  rrhf  33937  esumcocn  34019  cnmbfm  34203  cnpconn  35173  ptpconn  35176  sconnpi1  35182  txsconnlem  35183  cvxsconn  35186  cvmseu  35219  cvmopnlem  35221  cvmfolem  35222  cvmliftmolem1  35224  cvmliftmolem2  35225  cvmliftlem3  35230  cvmliftlem6  35233  cvmliftlem7  35234  cvmliftlem8  35235  cvmliftlem9  35236  cvmliftlem10  35237  cvmliftlem11  35238  cvmliftlem13  35239  cvmliftlem15  35241  cvmlift2lem3  35248  cvmlift2lem5  35250  cvmlift2lem7  35252  cvmlift2lem9  35254  cvmlift2lem10  35255  cvmliftphtlem  35260  cvmlift3lem1  35262  cvmlift3lem2  35263  cvmlift3lem4  35265  cvmlift3lem5  35266  cvmlift3lem6  35267  cvmlift3lem7  35268  cvmlift3lem8  35269  cvmlift3lem9  35270  poimirlem31  37596  poimir  37598  broucube  37599  cnres2  37708  cnresima  37709  hausgraph  43154  refsum2cnlem1  44988  itgsubsticclem  45934  stoweidlem62  46021  cnfsmf  46699  cnneiima  48770  sepfsepc  48781