Theorem cnf 20860

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977  ∀wral 2896  ∪ cuni 4372  ^◡ccnv 5037   “ cima 5041  ⟶wf 5800  (class class class)co 6549  Topctop 20517   Cn ccn 20838

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-mpt 4645  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-map 7746  df-top 20521  df-topon 20523  df-cn 20841

This theorem is referenced by:  cnco  20880  cnclima  20882  cnntri  20885  cnclsi  20886  cnss1  20890  cnss2  20891  cncnpi  20892  cncnp2  20895  cnrest  20899  cnrest2  20900  cnt0  20960  cnt1  20964  cnhaus  20968  dnsconst  20992  cncmp  21005  rncmp  21009  imacmp  21010  cnconn  21035  conima  21038  concn  21039  2ndcomap  21071  kgencn2  21170  kgencn3  21171  txcnmpt  21237  uptx  21238  txcn  21239  hauseqlcld  21259  xkohaus  21266  xkoptsub  21267  xkopjcn  21269  xkoco1cn  21270  xkoco2cn  21271  xkococnlem  21272  cnmpt11f  21277  cnmpt21f  21285  hmeocnv  21375  hmeores  21384  txhmeo  21416  cnextfres  21683  bndth  22565  evth  22566  evth2  22567  htpyco2  22586  phtpyco2  22597  reparphti  22605  copco  22626  pcopt  22630  pcopt2  22631  pcoass  22632  pcorevlem  22634  pcorev2  22636  hauseqcn  29269  pl1cn  29329  rrhf  29370  esumcocn  29469  cnmbfm  29652  cnpcon  30466  ptpcon  30469  sconpi1  30475  txsconlem  30476  cvxscon  30479  cvmseu  30512  cvmopnlem  30514  cvmfolem  30515  cvmliftmolem1  30517  cvmliftmolem2  30518  cvmliftlem3  30523  cvmliftlem6  30526  cvmliftlem7  30527  cvmliftlem8  30528  cvmliftlem9  30529  cvmliftlem10  30530  cvmliftlem11  30531  cvmliftlem13  30532  cvmliftlem15  30534  cvmlift2lem3  30541  cvmlift2lem5  30543  cvmlift2lem7  30545  cvmlift2lem9  30547  cvmlift2lem10  30548  cvmliftphtlem  30553  cvmlift3lem1  30555  cvmlift3lem2  30556  cvmlift3lem4  30558  cvmlift3lem5  30559  cvmlift3lem6  30560  cvmlift3lem7  30561  cvmlift3lem8  30562  cvmlift3lem9  30563  poimirlem31  32610  poimir  32612  broucube  32613  cnres2  32732  cnresima  32733  hausgraph  36809  refsum2cnlem1  38219  itgsubsticclem  38867  stoweidlem62  38955  cnfsmf  39627