![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > toptopon | Structured version Visualization version GIF version |
Description: Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.) |
Ref | Expression |
---|---|
toptopon.1 | ⊢ 𝑋 = ∪ 𝐽 |
Ref | Expression |
---|---|
toptopon | ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | toptopon.1 | . . 3 ⊢ 𝑋 = ∪ 𝐽 | |
2 | istopon 21128 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ (𝐽 ∈ Top ∧ 𝑋 = ∪ 𝐽)) | |
3 | 1, 2 | mpbiran2 700 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝑋) ↔ 𝐽 ∈ Top) |
4 | 3 | bicomi 216 | 1 ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 = wceq 1601 ∈ wcel 2107 ∪ cuni 4673 ‘cfv 6137 Topctop 21109 TopOnctopon 21126 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5019 ax-nul 5027 ax-pow 5079 ax-pr 5140 ax-un 7228 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4674 df-br 4889 df-opab 4951 df-mpt 4968 df-id 5263 df-xp 5363 df-rel 5364 df-cnv 5365 df-co 5366 df-dm 5367 df-iota 6101 df-fun 6139 df-fv 6145 df-topon 21127 |
This theorem is referenced by: toptopon2 21134 eltpsi 21160 neiptopreu 21349 restuni 21378 stoig 21379 restlp 21399 restperf 21400 perfopn 21401 iscn2 21454 iscnp2 21455 lmcvg 21478 cnss1 21492 cnss2 21493 cncnpi 21494 cncnp2 21497 cnnei 21498 cnrest 21501 cnrest2 21502 cnrest2r 21503 cnpresti 21504 cnprest 21505 cnprest2 21506 paste 21510 lmss 21514 lmcnp 21520 lmcn 21521 t1t0 21564 haust1 21568 restcnrm 21578 resthauslem 21579 t1sep2 21585 sshauslem 21588 lmmo 21596 rncmp 21612 connima 21641 conncn 21642 1stcelcls 21677 kgeni 21753 kgenuni 21755 kgenftop 21756 kgenss 21759 kgenhaus 21760 kgencmp2 21762 kgenidm 21763 iskgen3 21765 1stckgen 21770 kgencn3 21774 kgen2cn 21775 txuni 21808 ptuniconst 21814 dfac14 21834 ptcnplem 21837 ptcnp 21838 txcnmpt 21840 txcn 21842 ptcn 21843 txindis 21850 txdis1cn 21851 ptrescn 21855 txcmpb 21860 lmcn2 21865 txkgen 21868 xkohaus 21869 xkoptsub 21870 xkopt 21871 cnmpt11 21879 cnmpt11f 21880 cnmpt1t 21881 cnmpt12 21883 cnmpt21 21887 cnmpt21f 21888 cnmpt2t 21889 cnmpt22 21890 cnmpt22f 21891 cnmptcom 21894 cnmptkp 21896 xkofvcn 21900 cnmpt2k 21904 txconn 21905 imasnopn 21906 imasncld 21907 imasncls 21908 qtopcmplem 21923 qtopkgen 21926 qtopss 21931 qtopeu 21932 qtopomap 21934 qtopcmap 21935 kqtop 21961 kqt0 21962 nrmr0reg 21965 regr1 21966 kqreg 21967 kqnrm 21968 hmeof1o 21980 hmeores 21987 hmeoqtop 21991 hmphref 21997 hmphindis 22013 cmphaushmeo 22016 txhmeo 22019 ptunhmeo 22024 xpstopnlem1 22025 ptcmpfi 22029 xkocnv 22030 xkohmeo 22031 kqhmph 22035 hausflim 22197 flimsncls 22202 flfneii 22208 hausflf 22213 cnpflfi 22215 flfcnp 22220 flfcnp2 22223 flimfnfcls 22244 cnpfcfi 22256 flfcntr 22259 cnextfun 22280 cnextfvval 22281 cnextf 22282 cnextcn 22283 cnextfres1 22284 cnextucn 22519 retopon 22979 cnmpt2pc 23139 evth 23170 evth2 23171 htpyco1 23189 htpyco2 23190 phtpyco2 23201 pcopt 23233 pcopt2 23234 pcorevlem 23237 pi1cof 23270 pi1coghm 23272 qtophaus 30505 rrhre 30667 pconnconn 31816 connpconn 31820 pconnpi1 31822 sconnpi1 31824 txsconnlem 31825 txsconn 31826 cvxsconn 31828 cvmsf1o 31857 cvmliftmolem1 31866 cvmliftlem8 31877 cvmlift2lem9a 31888 cvmlift2lem9 31896 cvmlift2lem11 31898 cvmlift2lem12 31899 cvmliftphtlem 31902 cvmlift3lem6 31909 cvmlift3lem8 31911 cvmlift3lem9 31912 cnres2 34191 cnresima 34192 hausgraph 38759 ntrf2 39388 fcnre 40127 |
Copyright terms: Public domain | W3C validator |