Theorem cnf2 22753

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088   ∈ wcel 2107  ∀wral 3062  ^◡ccnv 5676   “ cima 5680  ⟶wf 6540  ‘cfv 6544  (class class class)co 7409  TopOnctopon 22412   Cn ccn 22728

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-sbc 3779  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-fv 6552  df-ov 7412  df-oprab 7413  df-mpo 7414  df-map 8822  df-top 22396  df-topon 22413  df-cn 22731

This theorem is referenced by:  iscncl  22773  cncls2  22777  cncls  22778  cnntr  22779  cnrest2  22790  cnrest2r  22791  ptcn  23131  txdis1cn  23139  lmcn2  23153  cnmpt11  23167  cnmpt1t  23169  cnmpt12  23171  cnmpt21  23175  cnmpt2t  23177  cnmpt22  23178  cnmpt22f  23179  cnmptcom  23182  cnmptkp  23184  cnmptk1  23185  cnmpt1k  23186  cnmptkk  23187  cnmptk1p  23189  cnmptk2  23190  cnmpt2k  23192  qtopss  23219  qtopeu  23220  qtopomap  23222  qtopcmap  23223  hmeof1o2  23267  xpstopnlem1  23313  xkocnv  23318  xkohmeo  23319  qtophmeo  23321  cnmpt1plusg  23591  cnmpt2plusg  23592  tsmsmhm  23650  cnmpt1vsca  23698  cnmpt2vsca  23699  cnmpt1ds  24358  cnmpt2ds  24359  fsumcn  24386  cnmpopc  24444  htpyco1  24494  htpyco2  24495  phtpyco2  24506  pi1xfrf  24569  pi1xfr  24571  pi1xfrcnvlem  24572  pi1xfrcnv  24573  pi1cof  24575  pi1coghm  24577  cnmpt1ip  24764  cnmpt2ip  24765  txsconnlem  34231  txsconn  34232  cvmlift3lem6  34315  fcnre  43709  refsumcn  43714  refsum2cnlem1  43721  fprodcnlem  44315  icccncfext  44603  itgsubsticclem  44691