Theorem cnf2 23192

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086   ∈ wcel 2109  ∀wral 3052  ^◡ccnv 5658   “ cima 5662  ⟶wf 6532  ‘cfv 6536  (class class class)co 7410  TopOnctopon 22853   Cn ccn 23167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708  ax-sep 5271  ax-nul 5281  ax-pow 5340  ax-pr 5407  ax-un 7734

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-id 5553  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6489  df-fun 6538  df-fn 6539  df-f 6540  df-fv 6544  df-ov 7413  df-oprab 7414  df-mpo 7415  df-map 8847  df-top 22837  df-topon 22854  df-cn 23170

This theorem is referenced by:  iscncl  23212  cncls2  23216  cncls  23217  cnntr  23218  cnrest2  23229  cnrest2r  23230  ptcn  23570  txdis1cn  23578  lmcn2  23592  cnmpt11  23606  cnmpt1t  23608  cnmpt12  23610  cnmpt21  23614  cnmpt2t  23616  cnmpt22  23617  cnmpt22f  23618  cnmptcom  23621  cnmptkp  23623  cnmptk1  23624  cnmpt1k  23625  cnmptkk  23626  cnmptk1p  23628  cnmptk2  23629  cnmpt2k  23631  qtopss  23658  qtopeu  23659  qtopomap  23661  qtopcmap  23662  hmeof1o2  23706  xpstopnlem1  23752  xkocnv  23757  xkohmeo  23758  qtophmeo  23760  cnmpt1plusg  24030  cnmpt2plusg  24031  tsmsmhm  24089  cnmpt1vsca  24137  cnmpt2vsca  24138  cnmpt1ds  24787  cnmpt2ds  24788  fsumcn  24817  cnmpopc  24878  htpyco1  24933  htpyco2  24934  phtpyco2  24945  pi1xfrf  25009  pi1xfr  25011  pi1xfrcnvlem  25012  pi1xfrcnv  25013  pi1cof  25015  pi1coghm  25017  cnmpt1ip  25204  cnmpt2ip  25205  txsconnlem  35267  txsconn  35268  cvmlift3lem6  35351  fcnre  45016  refsumcn  45021  refsum2cnlem1  45028  fprodcnlem  45595  icccncfext  45883  itgsubsticclem  45971