Theorem cnf 23184

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 23176	. . 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 2108  ∀wral 3051  ∪ cuni 4883  ^◡ccnv 5653   “ cima 5657  ⟶wf 6527  (class class class)co 7405  Topctop 22831   Cn ccn 23162

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

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 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410  df-map 8842  df-top 22832  df-topon 22849  df-cn 23165

This theorem is referenced by:  cnco  23204  cnclima  23206  cnntri  23209  cnclsi  23210  cnss1  23214  cnss2  23215  cncnpi  23216  cncnp2  23219  cnrest  23223  cnrest2  23224  cnt0  23284  cnt1  23288  cnhaus  23292  dnsconst  23316  cncmp  23330  rncmp  23334  imacmp  23335  cnconn  23360  connima  23363  conncn  23364  2ndcomap  23396  kgencn2  23495  kgencn3  23496  txcnmpt  23562  uptx  23563  txcn  23564  hauseqlcld  23584  xkohaus  23591  xkoptsub  23592  xkopjcn  23594  xkoco1cn  23595  xkoco2cn  23596  xkococnlem  23597  cnmpt11f  23602  cnmpt21f  23610  hmeocnv  23700  hmeores  23709  txhmeo  23741  cnextfres  24007  bndth  24908  evth  24909  evth2  24910  htpyco2  24929  phtpyco2  24940  reparphti  24947  reparphtiOLD  24948  copco  24969  pcopt  24973  pcopt2  24974  pcoass  24975  pcorevlem  24977  pcorev2  24979  hauseqcn  33929  pl1cn  33986  rrhf  34029  esumcocn  34111  cnmbfm  34295  cnpconn  35252  ptpconn  35255  sconnpi1  35261  txsconnlem  35262  cvxsconn  35265  cvmseu  35298  cvmopnlem  35300  cvmfolem  35301  cvmliftmolem1  35303  cvmliftmolem2  35304  cvmliftlem3  35309  cvmliftlem6  35312  cvmliftlem7  35313  cvmliftlem8  35314  cvmliftlem9  35315  cvmliftlem10  35316  cvmliftlem11  35317  cvmliftlem13  35318  cvmliftlem15  35320  cvmlift2lem3  35327  cvmlift2lem5  35329  cvmlift2lem7  35331  cvmlift2lem9  35333  cvmlift2lem10  35334  cvmliftphtlem  35339  cvmlift3lem1  35341  cvmlift3lem2  35342  cvmlift3lem4  35344  cvmlift3lem5  35345  cvmlift3lem6  35346  cvmlift3lem7  35347  cvmlift3lem8  35348  cvmlift3lem9  35349  poimirlem31  37675  poimir  37677  broucube  37678  cnres2  37787  cnresima  37788  hausgraph  43229  refsum2cnlem1  45061  itgsubsticclem  46004  stoweidlem62  46091  cnfsmf  46769  cnneiima  48891  sepfsepc  48902