Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > toptopon | Structured version Visualization version Unicode version |
Description: Alternative definition of in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.) |
Ref | Expression |
---|---|
toptopon.1 |
Ref | Expression |
---|---|
toptopon | TopOn |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | toptopon.1 | . . 3 | |
2 | istopon 20717 | . . 3 TopOn | |
3 | 1, 2 | mpbiran2 954 | . 2 TopOn |
4 | 3 | bicomi 214 | 1 TopOn |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wceq 1483 wcel 1990 cuni 4436 cfv 5888 ctop 20698 TopOnctopon 20715 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-rab 2921 df-v 3202 df-sbc 3436 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-iota 5851 df-fun 5890 df-fv 5896 df-topon 20716 |
This theorem is referenced by: toptopon2 20723 eltpsi 20748 neiptopreu 20937 restuni 20966 stoig 20967 restlp 20987 restperf 20988 perfopn 20989 iscn2 21042 iscnp2 21043 lmcvg 21066 cnss1 21080 cnss2 21081 cncnpi 21082 cncnp2 21085 cnnei 21086 cnrest 21089 cnrest2 21090 cnrest2r 21091 cnpresti 21092 cnprest 21093 cnprest2 21094 paste 21098 lmss 21102 lmcnp 21108 lmcn 21109 t1t0 21152 haust1 21156 restcnrm 21166 resthauslem 21167 t1sep2 21173 sshauslem 21176 lmmo 21184 rncmp 21199 connima 21228 conncn 21229 1stcelcls 21264 kgeni 21340 kgenuni 21342 kgenftop 21343 kgenss 21346 kgenhaus 21347 kgencmp2 21349 kgenidm 21350 iskgen3 21352 1stckgen 21357 kgencn3 21361 kgen2cn 21362 txuni 21395 ptuniconst 21401 dfac14 21421 ptcnplem 21424 ptcnp 21425 txcnmpt 21427 txcn 21429 ptcn 21430 txindis 21437 txdis1cn 21438 ptrescn 21442 txcmpb 21447 lmcn2 21452 txkgen 21455 xkohaus 21456 xkoptsub 21457 xkopt 21458 cnmpt11 21466 cnmpt11f 21467 cnmpt1t 21468 cnmpt12 21470 cnmpt21 21474 cnmpt21f 21475 cnmpt2t 21476 cnmpt22 21477 cnmpt22f 21478 cnmptcom 21481 cnmptkp 21483 xkofvcn 21487 cnmpt2k 21491 txconn 21492 imasnopn 21493 imasncld 21494 imasncls 21495 qtopcmplem 21510 qtopkgen 21513 qtopss 21518 qtopeu 21519 qtopomap 21521 qtopcmap 21522 kqtop 21548 kqt0 21549 nrmr0reg 21552 regr1 21553 kqreg 21554 kqnrm 21555 hmeof1o 21567 hmeores 21574 hmeoqtop 21578 hmphref 21584 hmphindis 21600 cmphaushmeo 21603 txhmeo 21606 ptunhmeo 21611 xpstopnlem1 21612 ptcmpfi 21616 xkocnv 21617 xkohmeo 21618 kqhmph 21622 hausflim 21785 flimsncls 21790 flfneii 21796 hausflf 21801 cnpflfi 21803 flfcnp 21808 flfcnp2 21811 flimfnfcls 21832 cnpfcfi 21844 flfcntr 21847 cnextfun 21868 cnextfvval 21869 cnextf 21870 cnextcn 21871 cnextfres1 21872 cnextucn 22107 retopon 22567 cnmpt2pc 22727 evth 22758 evth2 22759 htpyco1 22777 htpyco2 22778 phtpyco2 22789 pcopt 22822 pcopt2 22823 pcorevlem 22826 pi1cof 22859 pi1coghm 22861 qtophaus 29903 rrhre 30065 pconnconn 31213 connpconn 31217 pconnpi1 31219 sconnpi1 31221 txsconnlem 31222 txsconn 31223 cvxsconn 31225 cvmsf1o 31254 cvmliftmolem1 31263 cvmliftlem8 31274 cvmlift2lem9a 31285 cvmlift2lem9 31293 cvmlift2lem11 31295 cvmlift2lem12 31296 cvmliftphtlem 31299 cvmlift3lem6 31306 cvmlift3lem8 31308 cvmlift3lem9 31309 cnres2 33562 cnresima 33563 hausgraph 37790 ntrf2 38422 fcnre 39184 |
Copyright terms: Public domain | W3C validator |