Theorem cnf 21250

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

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1630   ∈ wcel 2137  ∀wral 3048  ∪ cuni 4586  ^◡ccnv 5263   “ cima 5267  ⟶wf 6043  (class class class)co 6811  Topctop 20898   Cn ccn 21228

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-8 2139  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pow 4990  ax-pr 5053  ax-un 7112

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-eu 2609  df-mo 2610  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-ne 2931  df-ral 3053  df-rex 3054  df-rab 3057  df-v 3340  df-sbc 3575  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-pw 4302  df-sn 4320  df-pr 4322  df-op 4326  df-uni 4587  df-br 4803  df-opab 4863  df-mpt 4880  df-id 5172  df-xp 5270  df-rel 5271  df-cnv 5272  df-co 5273  df-dm 5274  df-rn 5275  df-res 5276  df-ima 5277  df-iota 6010  df-fun 6049  df-fn 6050  df-f 6051  df-fv 6055  df-ov 6814  df-oprab 6815  df-mpt2 6816  df-map 8023  df-top 20899  df-topon 20916  df-cn 21231

This theorem is referenced by:  cnco  21270  cnclima  21272  cnntri  21275  cnclsi  21276  cnss1  21280  cnss2  21281  cncnpi  21282  cncnp2  21285  cnrest  21289  cnrest2  21290  cnt0  21350  cnt1  21354  cnhaus  21358  dnsconst  21382  cncmp  21395  rncmp  21399  imacmp  21400  cnconn  21425  connima  21428  conncn  21429  2ndcomap  21461  kgencn2  21560  kgencn3  21561  txcnmpt  21627  uptx  21628  txcn  21629  hauseqlcld  21649  xkohaus  21656  xkoptsub  21657  xkopjcn  21659  xkoco1cn  21660  xkoco2cn  21661  xkococnlem  21662  cnmpt11f  21667  cnmpt21f  21675  hmeocnv  21765  hmeores  21774  txhmeo  21806  cnextfres  22072  bndth  22956  evth  22957  evth2  22958  htpyco2  22977  phtpyco2  22988  reparphti  22995  copco  23016  pcopt  23020  pcopt2  23021  pcoass  23022  pcorevlem  23024  pcorev2  23026  hauseqcn  30248  pl1cn  30308  rrhf  30349  esumcocn  30449  cnmbfm  30632  cnpconn  31517  ptpconn  31520  sconnpi1  31526  txsconnlem  31527  cvxsconn  31530  cvmseu  31563  cvmopnlem  31565  cvmfolem  31566  cvmliftmolem1  31568  cvmliftmolem2  31569  cvmliftlem3  31574  cvmliftlem6  31577  cvmliftlem7  31578  cvmliftlem8  31579  cvmliftlem9  31580  cvmliftlem10  31581  cvmliftlem11  31582  cvmliftlem13  31583  cvmliftlem15  31585  cvmlift2lem3  31592  cvmlift2lem5  31594  cvmlift2lem7  31596  cvmlift2lem9  31598  cvmlift2lem10  31599  cvmliftphtlem  31604  cvmlift3lem1  31606  cvmlift3lem2  31607  cvmlift3lem4  31609  cvmlift3lem5  31610  cvmlift3lem6  31611  cvmlift3lem7  31612  cvmlift3lem8  31613  cvmlift3lem9  31614  poimirlem31  33751  poimir  33753  broucube  33754  cnres2  33873  cnresima  33874  hausgraph  38290  refsum2cnlem1  39693  itgsubsticclem  40692  stoweidlem62  40780  cnfsmf  41453