Theorem cnf2 23202

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 23188	. . 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 3049  ^◡ccnv 5619   “ cima 5623  ⟶wf 6483  ‘cfv 6487  (class class class)co 7356  TopOnctopon 22863   Cn ccn 23177

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 2184  ax-ext 2707  ax-sep 5220  ax-nul 5230  ax-pow 5296  ax-pr 5364  ax-un 7678

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 2931  df-ral 3050  df-rex 3060  df-rab 3388  df-v 3429  df-sbc 3726  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-pw 4533  df-sn 4558  df-pr 4560  df-op 4564  df-uni 4841  df-br 5075  df-opab 5137  df-mpt 5156  df-id 5515  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-fv 6495  df-ov 7359  df-oprab 7360  df-mpo 7361  df-map 8764  df-top 22847  df-topon 22864  df-cn 23180

This theorem is referenced by:  iscncl  23222  cncls2  23226  cncls  23227  cnntr  23228  cnrest2  23239  cnrest2r  23240  ptcn  23580  txdis1cn  23588  lmcn2  23602  cnmpt11  23616  cnmpt1t  23618  cnmpt12  23620  cnmpt21  23624  cnmpt2t  23626  cnmpt22  23627  cnmpt22f  23628  cnmptcom  23631  cnmptkp  23633  cnmptk1  23634  cnmpt1k  23635  cnmptkk  23636  cnmptk1p  23638  cnmptk2  23639  cnmpt2k  23641  qtopss  23668  qtopeu  23669  qtopomap  23671  qtopcmap  23672  hmeof1o2  23716  xpstopnlem1  23762  xkocnv  23767  xkohmeo  23768  qtophmeo  23770  cnmpt1plusg  24040  cnmpt2plusg  24041  tsmsmhm  24099  cnmpt1vsca  24147  cnmpt2vsca  24148  cnmpt1ds  24796  cnmpt2ds  24797  fsumcn  24825  cnmpopc  24883  htpyco1  24933  htpyco2  24934  phtpyco2  24945  pi1xfrf  25008  pi1xfr  25010  pi1xfrcnvlem  25011  pi1xfrcnv  25012  pi1cof  25014  pi1coghm  25016  cnmpt1ip  25202  cnmpt2ip  25203  txsconnlem  35410  txsconn  35411  cvmlift3lem6  35494  fcnre  45444  refsumcn  45449  refsum2cnlem1  45456  fprodcnlem  46017  icccncfext  46303  itgsubsticclem  46391