Theorem cnf2 23195

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 23181	. . 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 3050  ^◡ccnv 5622   “ cima 5626  ⟶wf 6487  ‘cfv 6491  (class class class)co 7358  TopOnctopon 22856   Cn ccn 23170

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 2183  ax-ext 2707  ax-sep 5240  ax-nul 5250  ax-pow 5309  ax-pr 5376  ax-un 7680

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 2932  df-ral 3051  df-rex 3060  df-rab 3399  df-v 3441  df-sbc 3740  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4285  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-mpt 5179  df-id 5518  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-iota 6447  df-fun 6493  df-fn 6494  df-f 6495  df-fv 6499  df-ov 7361  df-oprab 7362  df-mpo 7363  df-map 8767  df-top 22840  df-topon 22857  df-cn 23173

This theorem is referenced by:  iscncl  23215  cncls2  23219  cncls  23220  cnntr  23221  cnrest2  23232  cnrest2r  23233  ptcn  23573  txdis1cn  23581  lmcn2  23595  cnmpt11  23609  cnmpt1t  23611  cnmpt12  23613  cnmpt21  23617  cnmpt2t  23619  cnmpt22  23620  cnmpt22f  23621  cnmptcom  23624  cnmptkp  23626  cnmptk1  23627  cnmpt1k  23628  cnmptkk  23629  cnmptk1p  23631  cnmptk2  23632  cnmpt2k  23634  qtopss  23661  qtopeu  23662  qtopomap  23664  qtopcmap  23665  hmeof1o2  23709  xpstopnlem1  23755  xkocnv  23760  xkohmeo  23761  qtophmeo  23763  cnmpt1plusg  24033  cnmpt2plusg  24034  tsmsmhm  24092  cnmpt1vsca  24140  cnmpt2vsca  24141  cnmpt1ds  24789  cnmpt2ds  24790  fsumcn  24819  cnmpopc  24880  htpyco1  24935  htpyco2  24936  phtpyco2  24947  pi1xfrf  25011  pi1xfr  25013  pi1xfrcnvlem  25014  pi1xfrcnv  25015  pi1cof  25017  pi1coghm  25019  cnmpt1ip  25205  cnmpt2ip  25206  txsconnlem  35413  txsconn  35414  cvmlift3lem6  35497  fcnre  45307  refsumcn  45312  refsum2cnlem1  45319  fprodcnlem  45882  icccncfext  46168  itgsubsticclem  46256