![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > cntop2 | Structured version Visualization version Unicode version |
Description: Reverse closure for a continuous function. (Contributed by Mario Carneiro, 21-Aug-2015.) |
Ref | Expression |
---|---|
cntop2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2461 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | eqid 2461 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | iscn2 20302 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | simplbi 466 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 4 | simprd 469 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-8 1899 ax-9 1906 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 ax-nul 4547 ax-pow 4594 ax-pr 4652 ax-un 6609 |
This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-eu 2313 df-mo 2314 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ne 2634 df-ral 2753 df-rex 2754 df-rab 2757 df-v 3058 df-sbc 3279 df-dif 3418 df-un 3420 df-in 3422 df-ss 3429 df-nul 3743 df-if 3893 df-pw 3964 df-sn 3980 df-pr 3982 df-op 3986 df-uni 4212 df-br 4416 df-opab 4475 df-mpt 4476 df-id 4767 df-xp 4858 df-rel 4859 df-cnv 4860 df-co 4861 df-dm 4862 df-rn 4863 df-res 4864 df-ima 4865 df-iota 5564 df-fun 5602 df-fn 5603 df-f 5604 df-fv 5608 df-ov 6317 df-oprab 6318 df-mpt2 6319 df-map 7499 df-top 19969 df-topon 19971 df-cn 20291 |
This theorem is referenced by: cnco 20330 cncls2i 20334 cnntri 20335 cnss1 20340 cncnpi 20342 cncnp2 20345 cnrest 20349 cnrest2r 20351 paste 20358 cncmp 20455 rncmp 20459 cnconn 20485 conima 20488 concn 20489 2ndcomap 20521 kgen2cn 20622 txcnmpt 20687 uptx 20688 lmcn2 20712 xkoco1cn 20720 xkoco2cn 20721 xkococnlem 20722 cnmpt11 20726 cnmpt11f 20727 cnmpt1t 20728 cnmpt12 20730 cnmpt21 20734 cnmpt2t 20736 cnmpt22 20737 cnmpt22f 20738 cnmptcom 20741 cnmpt2k 20751 qtopeu 20779 hmeofval 20821 hmeof1o 20827 hmeontr 20832 hmeores 20834 hmeoqtop 20838 hmphen 20848 reghmph 20856 nrmhmph 20857 txhmeo 20866 xpstopnlem1 20872 flfcntr 21106 cnmpt2pc 22004 ishtpy 22051 htpyco1 22057 htpyco2 22058 isphtpy 22060 phtpyco2 22069 isphtpc 22073 pcofval 22089 pcopt 22101 pcopt2 22102 pcorevlem 22105 pi1cof 22138 pi1coghm 22140 cnmbfm 29133 cnpcon 30001 |
Copyright terms: Public domain | W3C validator |