Theorem cnf 23192

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

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542   ∈ wcel 2114  ∀wral 3050  ∪ cuni 4862  ^◡ccnv 5622   “ cima 5626  ⟶wf 6487  (class class class)co 7358  Topctop 22839   Cn ccn 23170

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2538  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2810  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-sbc 3740  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-fv 6499  df-ov 7361  df-oprab 7362  df-mpo 7363  df-map 8767  df-top 22840  df-topon 22857  df-cn 23173

This theorem is referenced by:  cnco  23212  cnclima  23214  cnntri  23217  cnclsi  23218  cnss1  23222  cnss2  23223  cncnpi  23224  cncnp2  23227  cnrest  23231  cnrest2  23232  cnt0  23292  cnt1  23296  cnhaus  23300  dnsconst  23324  cncmp  23338  rncmp  23342  imacmp  23343  cnconn  23368  connima  23371  conncn  23372  2ndcomap  23404  kgencn2  23503  kgencn3  23504  txcnmpt  23570  uptx  23571  txcn  23572  hauseqlcld  23592  xkohaus  23599  xkoptsub  23600  xkopjcn  23602  xkoco1cn  23603  xkoco2cn  23604  xkococnlem  23605  cnmpt11f  23610  cnmpt21f  23618  hmeocnv  23708  hmeores  23717  txhmeo  23749  cnextfres  24015  bndth  24915  evth  24916  evth2  24917  htpyco2  24936  phtpyco2  24947  reparphti  24954  reparphtiOLD  24955  copco  24976  pcopt  24980  pcopt2  24981  pcoass  24982  pcorevlem  24984  pcorev2  24986  hauseqcn  34034  pl1cn  34091  rrhf  34134  esumcocn  34216  cnmbfm  34399  cnpconn  35403  ptpconn  35406  sconnpi1  35412  txsconnlem  35413  cvxsconn  35416  cvmseu  35449  cvmopnlem  35451  cvmfolem  35452  cvmliftmolem1  35454  cvmliftmolem2  35455  cvmliftlem3  35460  cvmliftlem6  35463  cvmliftlem7  35464  cvmliftlem8  35465  cvmliftlem9  35466  cvmliftlem10  35467  cvmliftlem11  35468  cvmliftlem13  35469  cvmliftlem15  35471  cvmlift2lem3  35478  cvmlift2lem5  35480  cvmlift2lem7  35482  cvmlift2lem9  35484  cvmlift2lem10  35485  cvmliftphtlem  35490  cvmlift3lem1  35492  cvmlift3lem2  35493  cvmlift3lem4  35495  cvmlift3lem5  35496  cvmlift3lem6  35497  cvmlift3lem7  35498  cvmlift3lem8  35499  cvmlift3lem9  35500  poimirlem31  37821  poimir  37823  broucube  37824  cnres2  37933  cnresima  37934  hausgraph  43484  refsum2cnlem1  45319  itgsubsticclem  46256  stoweidlem62  46343  cnfsmf  47021  cnneiima  49199  sepfsepc  49210