Theorem cnf2 23389

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 23375	. . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽)))
2	1	simprbda 503	. 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌)
3	2	3impa 1125	1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   ∈ wcel 2150  ∀wral 3086  ^◡ccnv 5664   “ cima 5668  ⟶wf 6536  ‘cfv 6540  (class class class)co 7414  TopOnctopon 23050   Cn ccn 23364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-10 2183  ax-11 2199  ax-12 2220  ax-ext 2742  ax-sep 5262  ax-nul 5274  ax-pow 5340  ax-pr 5408  ax-un 7736

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2099  df-mo 2574  df-eu 2604  df-clab 2749  df-cleq 2762  df-clel 2845  df-nfc 2919  df-ne 2966  df-ral 3087  df-rex 3097  df-rab 3424  df-v 3464  df-sbc 3753  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-mpt 5198  df-id 5560  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6496  df-fun 6542  df-fn 6543  df-f 6544  df-fv 6548  df-ov 7417  df-oprab 7418  df-mpo 7419  df-map 8829  df-top 23034  df-topon 23051  df-cn 23367

This theorem is referenced by:  iscncl  23409  cncls2  23413  cncls  23414  cnntr  23415  cnrest2  23426  cnrest2r  23427  ptcn  23767  txdis1cn  23775  lmcn2  23789  cnmpt11  23803  cnmpt1t  23805  cnmpt12  23807  cnmpt21  23811  cnmpt2t  23813  cnmpt22  23814  cnmpt22f  23815  cnmptcom  23818  cnmptkp  23820  cnmptk1  23821  cnmpt1k  23822  cnmptkk  23823  cnmptk1p  23825  cnmptk2  23826  cnmpt2k  23828  qtopss  23855  qtopeu  23856  qtopomap  23858  qtopcmap  23859  hmeof1o2  23903  xpstopnlem1  23949  xkocnv  23954  xkohmeo  23955  qtophmeo  23957  cnmpt1plusg  24227  cnmpt2plusg  24228  tsmsmhm  24286  cnmpt1vsca  24334  cnmpt2vsca  24335  cnmpt1ds  24983  cnmpt2ds  24984  fsumcn  25012  cnmpopc  25070  htpyco1  25120  htpyco2  25121  phtpyco2  25132  pi1xfrf  25195  pi1xfr  25197  pi1xfrcnvlem  25198  pi1xfrcnv  25199  pi1cof  25201  pi1coghm  25203  cnmpt1ip  25389  cnmpt2ip  25390  txsconnlem  35690  txsconn  35691  cvmlift3lem6  35774  fcnre  45697  refsumcn  45702  refsum2cnlem1  45709  fprodcnlem  46267  icccncfext  46553  itgsubsticclem  46641