Theorem cnf 23221

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 23213	. . 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 5623   “ cima 5627  ⟶wf 6488  (class class class)co 7360  Topctop 22868   Cn ccn 23199

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 5231  ax-nul 5241  ax-pow 5302  ax-pr 5370  ax-un 7682

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 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-ov 7363  df-oprab 7364  df-mpo 7365  df-map 8768  df-top 22869  df-topon 22886  df-cn 23202

This theorem is referenced by:  cnco  23241  cnclima  23243  cnntri  23246  cnclsi  23247  cnss1  23251  cnss2  23252  cncnpi  23253  cncnp2  23256  cnrest  23260  cnrest2  23261  cnt0  23321  cnt1  23325  cnhaus  23329  dnsconst  23353  cncmp  23367  rncmp  23371  imacmp  23372  cnconn  23397  connima  23400  conncn  23401  2ndcomap  23433  kgencn2  23532  kgencn3  23533  txcnmpt  23599  uptx  23600  txcn  23601  hauseqlcld  23621  xkohaus  23628  xkoptsub  23629  xkopjcn  23631  xkoco1cn  23632  xkoco2cn  23633  xkococnlem  23634  cnmpt11f  23639  cnmpt21f  23647  hmeocnv  23737  hmeores  23746  txhmeo  23778  cnextfres  24044  bndth  24935  evth  24936  evth2  24937  htpyco2  24956  phtpyco2  24967  reparphti  24974  copco  24995  pcopt  24999  pcopt2  25000  pcoass  25001  pcorevlem  25003  pcorev2  25005  hauseqcn  34058  pl1cn  34115  rrhf  34158  esumcocn  34240  cnmbfm  34423  cnpconn  35428  ptpconn  35431  sconnpi1  35437  txsconnlem  35438  cvxsconn  35441  cvmseu  35474  cvmopnlem  35476  cvmfolem  35477  cvmliftmolem1  35479  cvmliftmolem2  35480  cvmliftlem3  35485  cvmliftlem6  35488  cvmliftlem7  35489  cvmliftlem8  35490  cvmliftlem9  35491  cvmliftlem10  35492  cvmliftlem11  35493  cvmliftlem13  35494  cvmliftlem15  35496  cvmlift2lem3  35503  cvmlift2lem5  35505  cvmlift2lem7  35507  cvmlift2lem9  35509  cvmlift2lem10  35510  cvmliftphtlem  35515  cvmlift3lem1  35517  cvmlift3lem2  35518  cvmlift3lem4  35520  cvmlift3lem5  35521  cvmlift3lem6  35522  cvmlift3lem7  35523  cvmlift3lem8  35524  cvmlift3lem9  35525  poimirlem31  37986  poimir  37988  broucube  37989  cnres2  38098  cnresima  38099  hausgraph  43651  refsum2cnlem1  45486  itgsubsticclem  46421  stoweidlem62  46508  cnfsmf  47186  cnneiima  49404  sepfsepc  49415