Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > cnf2 | Structured version Visualization version GIF version |
Description: A continuous function is a mapping. (Contributed by Mario Carneiro, 21-Aug-2015.) |
Ref | Expression |
---|---|
cnf2 | ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iscn 22386 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) | |
2 | 1 | simprbda 499 | . 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) |
3 | 2 | 3impa 1109 | 1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1086 ∈ wcel 2106 ∀wral 3064 ◡ccnv 5588 “ cima 5592 ⟶wf 6429 ‘cfv 6433 (class class class)co 7275 TopOnctopon 22059 Cn ccn 22375 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2709 ax-sep 5223 ax-nul 5230 ax-pow 5288 ax-pr 5352 ax-un 7588 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1783 df-nf 1787 df-sb 2068 df-mo 2540 df-eu 2569 df-clab 2716 df-cleq 2730 df-clel 2816 df-nfc 2889 df-ral 3069 df-rex 3070 df-rab 3073 df-v 3434 df-sbc 3717 df-dif 3890 df-un 3892 df-in 3894 df-ss 3904 df-nul 4257 df-if 4460 df-pw 4535 df-sn 4562 df-pr 4564 df-op 4568 df-uni 4840 df-br 5075 df-opab 5137 df-mpt 5158 df-id 5489 df-xp 5595 df-rel 5596 df-cnv 5597 df-co 5598 df-dm 5599 df-rn 5600 df-res 5601 df-ima 5602 df-iota 6391 df-fun 6435 df-fn 6436 df-f 6437 df-fv 6441 df-ov 7278 df-oprab 7279 df-mpo 7280 df-map 8617 df-top 22043 df-topon 22060 df-cn 22378 |
This theorem is referenced by: iscncl 22420 cncls2 22424 cncls 22425 cnntr 22426 cnrest2 22437 cnrest2r 22438 ptcn 22778 txdis1cn 22786 lmcn2 22800 cnmpt11 22814 cnmpt1t 22816 cnmpt12 22818 cnmpt21 22822 cnmpt2t 22824 cnmpt22 22825 cnmpt22f 22826 cnmptcom 22829 cnmptkp 22831 cnmptk1 22832 cnmpt1k 22833 cnmptkk 22834 cnmptk1p 22836 cnmptk2 22837 cnmpt2k 22839 qtopss 22866 qtopeu 22867 qtopomap 22869 qtopcmap 22870 hmeof1o2 22914 xpstopnlem1 22960 xkocnv 22965 xkohmeo 22966 qtophmeo 22968 cnmpt1plusg 23238 cnmpt2plusg 23239 tsmsmhm 23297 cnmpt1vsca 23345 cnmpt2vsca 23346 cnmpt1ds 24005 cnmpt2ds 24006 fsumcn 24033 cnmpopc 24091 htpyco1 24141 htpyco2 24142 phtpyco2 24153 pi1xfrf 24216 pi1xfr 24218 pi1xfrcnvlem 24219 pi1xfrcnv 24220 pi1cof 24222 pi1coghm 24224 cnmpt1ip 24411 cnmpt2ip 24412 txsconnlem 33202 txsconn 33203 cvmlift3lem6 33286 fcnre 42568 refsumcn 42573 refsum2cnlem1 42580 fprodcnlem 43140 icccncfext 43428 itgsubsticclem 43516 |
Copyright terms: Public domain | W3C validator |