Theorem cnf 22741

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

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106  ∀wral 3061  ∪ cuni 4907  ^◡ccnv 5674   “ cima 5678  ⟶wf 6536  (class class class)co 7405  Topctop 22386   Cn ccn 22719

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7721

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7408  df-oprab 7409  df-mpo 7410  df-map 8818  df-top 22387  df-topon 22404  df-cn 22722

This theorem is referenced by:  cnco  22761  cnclima  22763  cnntri  22766  cnclsi  22767  cnss1  22771  cnss2  22772  cncnpi  22773  cncnp2  22776  cnrest  22780  cnrest2  22781  cnt0  22841  cnt1  22845  cnhaus  22849  dnsconst  22873  cncmp  22887  rncmp  22891  imacmp  22892  cnconn  22917  connima  22920  conncn  22921  2ndcomap  22953  kgencn2  23052  kgencn3  23053  txcnmpt  23119  uptx  23120  txcn  23121  hauseqlcld  23141  xkohaus  23148  xkoptsub  23149  xkopjcn  23151  xkoco1cn  23152  xkoco2cn  23153  xkococnlem  23154  cnmpt11f  23159  cnmpt21f  23167  hmeocnv  23257  hmeores  23266  txhmeo  23298  cnextfres  23564  bndth  24465  evth  24466  evth2  24467  htpyco2  24486  phtpyco2  24497  reparphti  24504  copco  24525  pcopt  24529  pcopt2  24530  pcoass  24531  pcorevlem  24533  pcorev2  24535  hauseqcn  32866  pl1cn  32923  rrhf  32966  esumcocn  33066  cnmbfm  33250  cnpconn  34209  ptpconn  34212  sconnpi1  34218  txsconnlem  34219  cvxsconn  34222  cvmseu  34255  cvmopnlem  34257  cvmfolem  34258  cvmliftmolem1  34260  cvmliftmolem2  34261  cvmliftlem3  34266  cvmliftlem6  34269  cvmliftlem7  34270  cvmliftlem8  34271  cvmliftlem9  34272  cvmliftlem10  34273  cvmliftlem11  34274  cvmliftlem13  34275  cvmliftlem15  34277  cvmlift2lem3  34284  cvmlift2lem5  34286  cvmlift2lem7  34288  cvmlift2lem9  34290  cvmlift2lem10  34291  cvmliftphtlem  34296  cvmlift3lem1  34298  cvmlift3lem2  34299  cvmlift3lem4  34301  cvmlift3lem5  34302  cvmlift3lem6  34303  cvmlift3lem7  34304  cvmlift3lem8  34305  cvmlift3lem9  34306  gg-reparphti  35160  poimirlem31  36507  poimir  36509  broucube  36510  cnres2  36619  cnresima  36620  hausgraph  41939  refsum2cnlem1  43706  itgsubsticclem  44677  stoweidlem62  44764  cnfsmf  45442  cnneiima  47502  sepfsepc  47513