Theorem cnf 20960

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

Syntax hints:   → wi 4   ∧ wa 384   = wceq 1480   ∈ wcel 1987  ∀wral 2907  ∪ cuni 4402  ^◡ccnv 5073   “ cima 5077  ⟶wf 5843  (class class class)co 6604  Topctop 20617   Cn ccn 20938

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-sbc 3418  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-op 4155  df-uni 4403  df-br 4614  df-opab 4674  df-mpt 4675  df-id 4989  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-fv 5855  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-map 7804  df-top 20621  df-topon 20623  df-cn 20941

This theorem is referenced by:  cnco  20980  cnclima  20982  cnntri  20985  cnclsi  20986  cnss1  20990  cnss2  20991  cncnpi  20992  cncnp2  20995  cnrest  20999  cnrest2  21000  cnt0  21060  cnt1  21064  cnhaus  21068  dnsconst  21092  cncmp  21105  rncmp  21109  imacmp  21110  cnconn  21135  connima  21138  conncn  21139  2ndcomap  21171  kgencn2  21270  kgencn3  21271  txcnmpt  21337  uptx  21338  txcn  21339  hauseqlcld  21359  xkohaus  21366  xkoptsub  21367  xkopjcn  21369  xkoco1cn  21370  xkoco2cn  21371  xkococnlem  21372  cnmpt11f  21377  cnmpt21f  21385  hmeocnv  21475  hmeores  21484  txhmeo  21516  cnextfres  21783  bndth  22665  evth  22666  evth2  22667  htpyco2  22686  phtpyco2  22697  reparphti  22705  copco  22726  pcopt  22730  pcopt2  22731  pcoass  22732  pcorevlem  22734  pcorev2  22736  hauseqcn  29720  pl1cn  29780  rrhf  29821  esumcocn  29920  cnmbfm  30103  cnpconn  30917  ptpconn  30920  sconnpi1  30926  txsconnlem  30927  cvxsconn  30930  cvmseu  30963  cvmopnlem  30965  cvmfolem  30966  cvmliftmolem1  30968  cvmliftmolem2  30969  cvmliftlem3  30974  cvmliftlem6  30977  cvmliftlem7  30978  cvmliftlem8  30979  cvmliftlem9  30980  cvmliftlem10  30981  cvmliftlem11  30982  cvmliftlem13  30983  cvmliftlem15  30985  cvmlift2lem3  30992  cvmlift2lem5  30994  cvmlift2lem7  30996  cvmlift2lem9  30998  cvmlift2lem10  30999  cvmliftphtlem  31004  cvmlift3lem1  31006  cvmlift3lem2  31007  cvmlift3lem4  31009  cvmlift3lem5  31010  cvmlift3lem6  31011  cvmlift3lem7  31012  cvmlift3lem8  31013  cvmlift3lem9  31014  poimirlem31  33069  poimir  33071  broucube  33072  cnres2  33191  cnresima  33192  hausgraph  37268  refsum2cnlem1  38676  itgsubsticclem  39495  stoweidlem62  39583  cnfsmf  40253