Theorem cnf 23308

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1562   ∈ wcel 2144  ∀wral 3078  ∪ cuni 4867  ^◡ccnv 5648   “ cima 5652  ⟶wf 6519  (class class class)co 7398  Topctop 22955   Cn ccn 23286

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3079  df-rex 3089  df-rab 3417  df-v 3458  df-sbc 3747  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5103  df-opab 5165  df-mpt 5184  df-id 5544  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-fv 6531  df-ov 7401  df-oprab 7402  df-mpo 7403  df-map 8812  df-top 22956  df-topon 22973  df-cn 23289

This theorem is referenced by:  cnco  23328  cnclima  23330  cnntri  23333  cnclsi  23334  cnss1  23338  cnss2  23339  cncnpi  23340  cncnp2  23343  cnrest  23347  cnrest2  23348  cnt0  23408  cnt1  23412  cnhaus  23416  dnsconst  23440  cncmp  23454  rncmp  23458  imacmp  23459  cnconn  23484  connima  23487  conncn  23488  2ndcomap  23520  kgencn2  23619  kgencn3  23620  txcnmpt  23686  uptx  23687  txcn  23688  hauseqlcld  23708  xkohaus  23715  xkoptsub  23716  xkopjcn  23718  xkoco1cn  23719  xkoco2cn  23720  xkococnlem  23721  cnmpt11f  23726  cnmpt21f  23734  hmeocnv  23824  hmeores  23833  txhmeo  23865  cnextfres  24131  bndth  25022  evth  25023  evth2  25024  htpyco2  25043  phtpyco2  25054  reparphti  25061  copco  25082  pcopt  25086  pcopt2  25087  pcoass  25088  pcorevlem  25090  pcorev2  25092  hauseqcn  34197  pl1cn  34254  rrhf  34297  esumcocn  34379  cnmbfm  34562  cnpconn  35585  ptpconn  35588  sconnpi1  35594  txsconnlem  35595  cvxsconn  35598  cvmseu  35631  cvmopnlem  35633  cvmfolem  35634  cvmliftmolem1  35636  cvmliftmolem2  35637  cvmliftlem3  35642  cvmliftlem6  35645  cvmliftlem7  35646  cvmliftlem8  35647  cvmliftlem9  35648  cvmliftlem10  35649  cvmliftlem11  35650  cvmliftlem13  35651  cvmliftlem15  35653  cvmlift2lem3  35660  cvmlift2lem5  35662  cvmlift2lem7  35664  cvmlift2lem9  35666  cvmlift2lem10  35667  cvmliftphtlem  35672  cvmlift3lem1  35674  cvmlift3lem2  35675  cvmlift3lem4  35677  cvmlift3lem5  35678  cvmlift3lem6  35679  cvmlift3lem7  35680  cvmlift3lem8  35681  cvmlift3lem9  35682  poimirlem31  38155  poimir  38157  broucube  38158  cnres2  38267  cnresima  38268  hausgraph  43787  refsum2cnlem1  45622  itgsubsticclem  46554  stoweidlem62  46641  cnfsmf  47319  cnneiima  49543  sepfsepc  49554