![]() |
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 21233 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) | |
2 | 1 | simprbda 654 | . 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) |
3 | 2 | 3impa 1100 | 1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 ∧ w3a 1072 ∈ wcel 2131 ∀wral 3042 ◡ccnv 5257 “ cima 5261 ⟶wf 6037 ‘cfv 6041 (class class class)co 6805 TopOnctopon 20909 Cn ccn 21222 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 ax-un 7106 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-ral 3047 df-rex 3048 df-rab 3051 df-v 3334 df-sbc 3569 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-pw 4296 df-sn 4314 df-pr 4316 df-op 4320 df-uni 4581 df-br 4797 df-opab 4857 df-mpt 4874 df-id 5166 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-rn 5269 df-res 5270 df-ima 5271 df-iota 6004 df-fun 6043 df-fn 6044 df-f 6045 df-fv 6049 df-ov 6808 df-oprab 6809 df-mpt2 6810 df-map 8017 df-top 20893 df-topon 20910 df-cn 21225 |
This theorem is referenced by: iscncl 21267 cncls2 21271 cncls 21272 cnntr 21273 cnrest2 21284 cnrest2r 21285 ptcn 21624 txdis1cn 21632 lmcn2 21646 cnmpt11 21660 cnmpt1t 21662 cnmpt12 21664 cnmpt21 21668 cnmpt2t 21670 cnmpt22 21671 cnmpt22f 21672 cnmptcom 21675 cnmptkp 21677 cnmptk1 21678 cnmpt1k 21679 cnmptkk 21680 cnmptk1p 21682 cnmptk2 21683 cnmpt2k 21685 qtopss 21712 qtopeu 21713 qtopomap 21715 qtopcmap 21716 hmeof1o2 21760 xpstopnlem1 21806 xkocnv 21811 xkohmeo 21812 qtophmeo 21814 cnmpt1plusg 22084 cnmpt2plusg 22085 tsmsmhm 22142 cnmpt1vsca 22190 cnmpt2vsca 22191 cnmpt1ds 22838 cnmpt2ds 22839 fsumcn 22866 cnmpt2pc 22920 htpyco1 22970 htpyco2 22971 phtpyco2 22982 pi1xfrf 23045 pi1xfr 23047 pi1xfrcnvlem 23048 pi1xfrcnv 23049 pi1cof 23051 pi1coghm 23053 cnmpt1ip 23238 cnmpt2ip 23239 txsconnlem 31521 txsconn 31522 cvmlift3lem6 31605 fcnre 39675 refsumcn 39680 refsum2cnlem1 39687 fprodcnlem 40326 icccncfext 40595 itgsubsticclem 40686 |
Copyright terms: Public domain | W3C validator |