Theorem cnf2 23210

Description: A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.)

Assertion

Ref	Expression
cnf2	⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌)

Proof of Theorem cnf2

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iscn 23196	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)))
2	1	simprbda 498	. 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌)
3	2	3impa 1110	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087   ∈ wcel 2114  ∀wral 3052  ^◡ccnv 5633   “ cima 5637  ⟶wf 6498  ‘cfv 6502  (class class class)co 7370  TopOnctopon 22871   Cn ccn 23185

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 2185  ax-ext 2709  ax-sep 5245  ax-nul 5255  ax-pow 5314  ax-pr 5381  ax-un 7692

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 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-sbc 3743  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5529  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-fv 6510  df-ov 7373  df-oprab 7374  df-mpo 7375  df-map 8779  df-top 22855  df-topon 22872  df-cn 23188

This theorem is referenced by:  iscncl  23230  cncls2  23234  cncls  23235  cnntr  23236  cnrest2  23247  cnrest2r  23248  ptcn  23588  txdis1cn  23596  lmcn2  23610  cnmpt11  23624  cnmpt1t  23626  cnmpt12  23628  cnmpt21  23632  cnmpt2t  23634  cnmpt22  23635  cnmpt22f  23636  cnmptcom  23639  cnmptkp  23641  cnmptk1  23642  cnmpt1k  23643  cnmptkk  23644  cnmptk1p  23646  cnmptk2  23647  cnmpt2k  23649  qtopss  23676  qtopeu  23677  qtopomap  23679  qtopcmap  23680  hmeof1o2  23724  xpstopnlem1  23770  xkocnv  23775  xkohmeo  23776  qtophmeo  23778  cnmpt1plusg  24048  cnmpt2plusg  24049  tsmsmhm  24107  cnmpt1vsca  24155  cnmpt2vsca  24156  cnmpt1ds  24804  cnmpt2ds  24805  fsumcn  24834  cnmpopc  24895  htpyco1  24950  htpyco2  24951  phtpyco2  24962  pi1xfrf  25026  pi1xfr  25028  pi1xfrcnvlem  25029  pi1xfrcnv  25030  pi1cof  25032  pi1coghm  25034  cnmpt1ip  25220  cnmpt2ip  25221  txsconnlem  35462  txsconn  35463  cvmlift3lem6  35546  fcnre  45414  refsumcn  45419  refsum2cnlem1  45426  fprodcnlem  45988  icccncfext  46274  itgsubsticclem  46362