Theorem cnf 23225

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3052  ∪ cuni 4851  ^◡ccnv 5625   “ cima 5629  ⟶wf 6490  (class class class)co 7362  Topctop 22872   Cn ccn 23203

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5232  ax-nul 5242  ax-pow 5304  ax-pr 5372  ax-un 7684

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5521  df-xp 5632  df-rel 5633  df-cnv 5634  df-co 5635  df-dm 5636  df-rn 5637  df-res 5638  df-ima 5639  df-iota 6450  df-fun 6496  df-fn 6497  df-f 6498  df-fv 6502  df-ov 7365  df-oprab 7366  df-mpo 7367  df-map 8770  df-top 22873  df-topon 22890  df-cn 23206

This theorem is referenced by:  cnco  23245  cnclima  23247  cnntri  23250  cnclsi  23251  cnss1  23255  cnss2  23256  cncnpi  23257  cncnp2  23260  cnrest  23264  cnrest2  23265  cnt0  23325  cnt1  23329  cnhaus  23333  dnsconst  23357  cncmp  23371  rncmp  23375  imacmp  23376  cnconn  23401  connima  23404  conncn  23405  2ndcomap  23437  kgencn2  23536  kgencn3  23537  txcnmpt  23603  uptx  23604  txcn  23605  hauseqlcld  23625  xkohaus  23632  xkoptsub  23633  xkopjcn  23635  xkoco1cn  23636  xkoco2cn  23637  xkococnlem  23638  cnmpt11f  23643  cnmpt21f  23651  hmeocnv  23741  hmeores  23750  txhmeo  23782  cnextfres  24048  bndth  24939  evth  24940  evth2  24941  htpyco2  24960  phtpyco2  24971  reparphti  24978  copco  24999  pcopt  25003  pcopt2  25004  pcoass  25005  pcorevlem  25007  pcorev2  25009  hauseqcn  34062  pl1cn  34119  rrhf  34162  esumcocn  34244  cnmbfm  34427  cnpconn  35432  ptpconn  35435  sconnpi1  35441  txsconnlem  35442  cvxsconn  35445  cvmseu  35478  cvmopnlem  35480  cvmfolem  35481  cvmliftmolem1  35483  cvmliftmolem2  35484  cvmliftlem3  35489  cvmliftlem6  35492  cvmliftlem7  35493  cvmliftlem8  35494  cvmliftlem9  35495  cvmliftlem10  35496  cvmliftlem11  35497  cvmliftlem13  35498  cvmliftlem15  35500  cvmlift2lem3  35507  cvmlift2lem5  35509  cvmlift2lem7  35511  cvmlift2lem9  35513  cvmlift2lem10  35514  cvmliftphtlem  35519  cvmlift3lem1  35521  cvmlift3lem2  35522  cvmlift3lem4  35524  cvmlift3lem5  35525  cvmlift3lem6  35526  cvmlift3lem7  35527  cvmlift3lem8  35528  cvmlift3lem9  35529  poimirlem31  37992  poimir  37994  broucube  37995  cnres2  38104  cnresima  38105  hausgraph  43657  refsum2cnlem1  45492  itgsubsticclem  46427  stoweidlem62  46514  cnfsmf  47192  cnneiima  49410  sepfsepc  49421