Theorem cnf2 23230

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 23216	. . 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 5627   “ cima 5631  ⟶wf 6492  ‘cfv 6496  (class class class)co 7364  TopOnctopon 22891   Cn ccn 23205

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 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686

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 3391  df-v 3432  df-sbc 3730  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5523  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-fv 6504  df-ov 7367  df-oprab 7368  df-mpo 7369  df-map 8772  df-top 22875  df-topon 22892  df-cn 23208

This theorem is referenced by:  iscncl  23250  cncls2  23254  cncls  23255  cnntr  23256  cnrest2  23267  cnrest2r  23268  ptcn  23608  txdis1cn  23616  lmcn2  23630  cnmpt11  23644  cnmpt1t  23646  cnmpt12  23648  cnmpt21  23652  cnmpt2t  23654  cnmpt22  23655  cnmpt22f  23656  cnmptcom  23659  cnmptkp  23661  cnmptk1  23662  cnmpt1k  23663  cnmptkk  23664  cnmptk1p  23666  cnmptk2  23667  cnmpt2k  23669  qtopss  23696  qtopeu  23697  qtopomap  23699  qtopcmap  23700  hmeof1o2  23744  xpstopnlem1  23790  xkocnv  23795  xkohmeo  23796  qtophmeo  23798  cnmpt1plusg  24068  cnmpt2plusg  24069  tsmsmhm  24127  cnmpt1vsca  24175  cnmpt2vsca  24176  cnmpt1ds  24824  cnmpt2ds  24825  fsumcn  24853  cnmpopc  24911  htpyco1  24961  htpyco2  24962  phtpyco2  24973  pi1xfrf  25036  pi1xfr  25038  pi1xfrcnvlem  25039  pi1xfrcnv  25040  pi1cof  25042  pi1coghm  25044  cnmpt1ip  25230  cnmpt2ip  25231  txsconnlem  35444  txsconn  35445  cvmlift3lem6  35528  fcnre  45482  refsumcn  45487  refsum2cnlem1  45494  fprodcnlem  46055  icccncfext  46341  itgsubsticclem  46429