Theorem cnf 23140

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 23132	. . 3 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)))
4	3	simprbi 496	. 2 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))
5	4	simpld 494	1 ⊢ (𝐹 ∈ (𝐽 Cn 𝐾) → 𝐹:𝑋⟶𝑌)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3045  ∪ cuni 4874  ^◡ccnv 5640   “ cima 5644  ⟶wf 6510  (class class class)co 7390  Topctop 22787   Cn ccn 23118

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pow 5323  ax-pr 5390  ax-un 7714

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-rab 3409  df-v 3452  df-sbc 3757  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-br 5111  df-opab 5173  df-mpt 5192  df-id 5536  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-fv 6522  df-ov 7393  df-oprab 7394  df-mpo 7395  df-map 8804  df-top 22788  df-topon 22805  df-cn 23121

This theorem is referenced by:  cnco  23160  cnclima  23162  cnntri  23165  cnclsi  23166  cnss1  23170  cnss2  23171  cncnpi  23172  cncnp2  23175  cnrest  23179  cnrest2  23180  cnt0  23240  cnt1  23244  cnhaus  23248  dnsconst  23272  cncmp  23286  rncmp  23290  imacmp  23291  cnconn  23316  connima  23319  conncn  23320  2ndcomap  23352  kgencn2  23451  kgencn3  23452  txcnmpt  23518  uptx  23519  txcn  23520  hauseqlcld  23540  xkohaus  23547  xkoptsub  23548  xkopjcn  23550  xkoco1cn  23551  xkoco2cn  23552  xkococnlem  23553  cnmpt11f  23558  cnmpt21f  23566  hmeocnv  23656  hmeores  23665  txhmeo  23697  cnextfres  23963  bndth  24864  evth  24865  evth2  24866  htpyco2  24885  phtpyco2  24896  reparphti  24903  reparphtiOLD  24904  copco  24925  pcopt  24929  pcopt2  24930  pcoass  24931  pcorevlem  24933  pcorev2  24935  hauseqcn  33895  pl1cn  33952  rrhf  33995  esumcocn  34077  cnmbfm  34261  cnpconn  35224  ptpconn  35227  sconnpi1  35233  txsconnlem  35234  cvxsconn  35237  cvmseu  35270  cvmopnlem  35272  cvmfolem  35273  cvmliftmolem1  35275  cvmliftmolem2  35276  cvmliftlem3  35281  cvmliftlem6  35284  cvmliftlem7  35285  cvmliftlem8  35286  cvmliftlem9  35287  cvmliftlem10  35288  cvmliftlem11  35289  cvmliftlem13  35290  cvmliftlem15  35292  cvmlift2lem3  35299  cvmlift2lem5  35301  cvmlift2lem7  35303  cvmlift2lem9  35305  cvmlift2lem10  35306  cvmliftphtlem  35311  cvmlift3lem1  35313  cvmlift3lem2  35314  cvmlift3lem4  35316  cvmlift3lem5  35317  cvmlift3lem6  35318  cvmlift3lem7  35319  cvmlift3lem8  35320  cvmlift3lem9  35321  poimirlem31  37652  poimir  37654  broucube  37655  cnres2  37764  cnresima  37765  hausgraph  43201  refsum2cnlem1  45038  itgsubsticclem  45980  stoweidlem62  46067  cnfsmf  46745  cnneiima  48909  sepfsepc  48920