![]() |
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 21537 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑥 ∈ 𝐾 (◡𝐹 “ 𝑥) ∈ 𝐽))) | |
2 | 1 | simprbda 491 | . 2 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌)) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) |
3 | 2 | 3impa 1090 | 1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐾 ∈ (TopOn‘𝑌) ∧ 𝐹 ∈ (𝐽 Cn 𝐾)) → 𝐹:𝑋⟶𝑌) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∧ w3a 1068 ∈ wcel 2048 ∀wral 3082 ◡ccnv 5399 “ cima 5403 ⟶wf 6178 ‘cfv 6182 (class class class)co 6970 TopOnctopon 21212 Cn ccn 21526 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-13 2299 ax-ext 2745 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-mo 2544 df-eu 2580 df-clab 2754 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ral 3087 df-rex 3088 df-rab 3091 df-v 3411 df-sbc 3678 df-dif 3828 df-un 3830 df-in 3832 df-ss 3839 df-nul 4174 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-op 4442 df-uni 4707 df-br 4924 df-opab 4986 df-mpt 5003 df-id 5305 df-xp 5406 df-rel 5407 df-cnv 5408 df-co 5409 df-dm 5410 df-rn 5411 df-res 5412 df-ima 5413 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-fv 6190 df-ov 6973 df-oprab 6974 df-mpo 6975 df-map 8200 df-top 21196 df-topon 21213 df-cn 21529 |
This theorem is referenced by: iscncl 21571 cncls2 21575 cncls 21576 cnntr 21577 cnrest2 21588 cnrest2r 21589 ptcn 21929 txdis1cn 21937 lmcn2 21951 cnmpt11 21965 cnmpt1t 21967 cnmpt12 21969 cnmpt21 21973 cnmpt2t 21975 cnmpt22 21976 cnmpt22f 21977 cnmptcom 21980 cnmptkp 21982 cnmptk1 21983 cnmpt1k 21984 cnmptkk 21985 cnmptk1p 21987 cnmptk2 21988 cnmpt2k 21990 qtopss 22017 qtopeu 22018 qtopomap 22020 qtopcmap 22021 hmeof1o2 22065 xpstopnlem1 22111 xkocnv 22116 xkohmeo 22117 qtophmeo 22119 cnmpt1plusg 22389 cnmpt2plusg 22390 tsmsmhm 22447 cnmpt1vsca 22495 cnmpt2vsca 22496 cnmpt1ds 23143 cnmpt2ds 23144 fsumcn 23171 cnmpopc 23225 htpyco1 23275 htpyco2 23276 phtpyco2 23287 pi1xfrf 23350 pi1xfr 23352 pi1xfrcnvlem 23353 pi1xfrcnv 23354 pi1cof 23356 pi1coghm 23358 cnmpt1ip 23543 cnmpt2ip 23544 txsconnlem 32032 txsconn 32033 cvmlift3lem6 32116 fcnre 40645 refsumcn 40650 refsum2cnlem1 40657 fprodcnlem 41257 icccncfext 41546 itgsubsticclem 41636 |
Copyright terms: Public domain | W3C validator |