Theorem cnf 22097

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2112  ∀wral 3051  ∪ cuni 4805  ^◡ccnv 5535   “ cima 5539  ⟶wf 6354  (class class class)co 7191  Topctop 21744   Cn ccn 22075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pow 5243  ax-pr 5307  ax-un 7501

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-nfc 2879  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-sbc 3684  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-pw 4501  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-opab 5102  df-mpt 5121  df-id 5440  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6316  df-fun 6360  df-fn 6361  df-f 6362  df-fv 6366  df-ov 7194  df-oprab 7195  df-mpo 7196  df-map 8488  df-top 21745  df-topon 21762  df-cn 22078

This theorem is referenced by:  cnco  22117  cnclima  22119  cnntri  22122  cnclsi  22123  cnss1  22127  cnss2  22128  cncnpi  22129  cncnp2  22132  cnrest  22136  cnrest2  22137  cnt0  22197  cnt1  22201  cnhaus  22205  dnsconst  22229  cncmp  22243  rncmp  22247  imacmp  22248  cnconn  22273  connima  22276  conncn  22277  2ndcomap  22309  kgencn2  22408  kgencn3  22409  txcnmpt  22475  uptx  22476  txcn  22477  hauseqlcld  22497  xkohaus  22504  xkoptsub  22505  xkopjcn  22507  xkoco1cn  22508  xkoco2cn  22509  xkococnlem  22510  cnmpt11f  22515  cnmpt21f  22523  hmeocnv  22613  hmeores  22622  txhmeo  22654  cnextfres  22920  bndth  23809  evth  23810  evth2  23811  htpyco2  23830  phtpyco2  23841  reparphti  23848  copco  23869  pcopt  23873  pcopt2  23874  pcoass  23875  pcorevlem  23877  pcorev2  23879  hauseqcn  31516  pl1cn  31573  rrhf  31614  esumcocn  31714  cnmbfm  31896  cnpconn  32859  ptpconn  32862  sconnpi1  32868  txsconnlem  32869  cvxsconn  32872  cvmseu  32905  cvmopnlem  32907  cvmfolem  32908  cvmliftmolem1  32910  cvmliftmolem2  32911  cvmliftlem3  32916  cvmliftlem6  32919  cvmliftlem7  32920  cvmliftlem8  32921  cvmliftlem9  32922  cvmliftlem10  32923  cvmliftlem11  32924  cvmliftlem13  32925  cvmliftlem15  32927  cvmlift2lem3  32934  cvmlift2lem5  32936  cvmlift2lem7  32938  cvmlift2lem9  32940  cvmlift2lem10  32941  cvmliftphtlem  32946  cvmlift3lem1  32948  cvmlift3lem2  32949  cvmlift3lem4  32951  cvmlift3lem5  32952  cvmlift3lem6  32953  cvmlift3lem7  32954  cvmlift3lem8  32955  cvmlift3lem9  32956  poimirlem31  35494  poimir  35496  broucube  35497  cnres2  35607  cnresima  35608  hausgraph  40681  refsum2cnlem1  42194  itgsubsticclem  43134  stoweidlem62  43221  cnfsmf  43891  cnneiima  45826  sepfsepc  45837