Theorem cnf 21570

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

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507   ∈ wcel 2050  ∀wral 3082  ∪ cuni 4708  ^◡ccnv 5402   “ cima 5406  ⟶wf 6181  (class class class)co 6974  Topctop 21217   Cn ccn 21548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2744  ax-sep 5056  ax-nul 5063  ax-pow 5115  ax-pr 5182  ax-un 7277

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2584  df-clab 2753  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ral 3087  df-rex 3088  df-rab 3091  df-v 3411  df-sbc 3676  df-dif 3826  df-un 3828  df-in 3830  df-ss 3837  df-nul 4173  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-op 4442  df-uni 4709  df-br 4926  df-opab 4988  df-mpt 5005  df-id 5308  df-xp 5409  df-rel 5410  df-cnv 5411  df-co 5412  df-dm 5413  df-rn 5414  df-res 5415  df-ima 5416  df-iota 6149  df-fun 6187  df-fn 6188  df-f 6189  df-fv 6193  df-ov 6977  df-oprab 6978  df-mpo 6979  df-map 8206  df-top 21218  df-topon 21235  df-cn 21551

This theorem is referenced by:  cnco  21590  cnclima  21592  cnntri  21595  cnclsi  21596  cnss1  21600  cnss2  21601  cncnpi  21602  cncnp2  21605  cnrest  21609  cnrest2  21610  cnt0  21670  cnt1  21674  cnhaus  21678  dnsconst  21702  cncmp  21716  rncmp  21720  imacmp  21721  cnconn  21746  connima  21749  conncn  21750  2ndcomap  21782  kgencn2  21881  kgencn3  21882  txcnmpt  21948  uptx  21949  txcn  21950  hauseqlcld  21970  xkohaus  21977  xkoptsub  21978  xkopjcn  21980  xkoco1cn  21981  xkoco2cn  21982  xkococnlem  21983  cnmpt11f  21988  cnmpt21f  21996  hmeocnv  22086  hmeores  22095  txhmeo  22127  cnextfres  22393  bndth  23277  evth  23278  evth2  23279  htpyco2  23298  phtpyco2  23309  reparphti  23316  copco  23337  pcopt  23341  pcopt2  23342  pcoass  23343  pcorevlem  23345  pcorev2  23347  hauseqcn  30811  pl1cn  30871  rrhf  30912  esumcocn  31012  cnmbfm  31195  cnpconn  32091  ptpconn  32094  sconnpi1  32100  txsconnlem  32101  cvxsconn  32104  cvmseu  32137  cvmopnlem  32139  cvmfolem  32140  cvmliftmolem1  32142  cvmliftmolem2  32143  cvmliftlem3  32148  cvmliftlem6  32151  cvmliftlem7  32152  cvmliftlem8  32153  cvmliftlem9  32154  cvmliftlem10  32155  cvmliftlem11  32156  cvmliftlem13  32157  cvmliftlem15  32159  cvmlift2lem3  32166  cvmlift2lem5  32168  cvmlift2lem7  32170  cvmlift2lem9  32172  cvmlift2lem10  32173  cvmliftphtlem  32178  cvmlift3lem1  32180  cvmlift3lem2  32181  cvmlift3lem4  32183  cvmlift3lem5  32184  cvmlift3lem6  32185  cvmlift3lem7  32186  cvmlift3lem8  32187  cvmlift3lem9  32188  poimirlem31  34393  poimir  34395  broucube  34396  cnres2  34512  cnresima  34513  hausgraph  39237  refsum2cnlem1  40742  itgsubsticclem  41715  stoweidlem62  41803  cnfsmf  42473