![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > toponuni | Structured version Visualization version GIF version |
Description: The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
Ref | Expression |
---|---|
toponuni | ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | istopon 20919 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) | |
2 | 1 | simprbi 483 | 1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1632 ∈ wcel 2139 ∪ cuni 4588 ‘cfv 6049 Topctop 20900 TopOnctopon 20917 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-8 2141 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 ax-sep 4933 ax-nul 4941 ax-pow 4992 ax-pr 5055 ax-un 7114 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-eu 2611 df-mo 2612 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-ne 2933 df-ral 3055 df-rex 3056 df-rab 3059 df-v 3342 df-sbc 3577 df-dif 3718 df-un 3720 df-in 3722 df-ss 3729 df-nul 4059 df-if 4231 df-pw 4304 df-sn 4322 df-pr 4324 df-op 4328 df-uni 4589 df-br 4805 df-opab 4865 df-mpt 4882 df-id 5174 df-xp 5272 df-rel 5273 df-cnv 5274 df-co 5275 df-dm 5276 df-iota 6012 df-fun 6051 df-fv 6057 df-topon 20918 |
This theorem is referenced by: toponunii 20923 toponmax 20932 toponss 20933 toponcom 20934 topgele 20936 topontopn 20946 toponmre 21099 cldmreon 21100 restuni 21168 resttopon2 21174 restlp 21189 restperf 21190 perfopn 21191 ordtcld1 21203 ordtcld2 21204 lmfval 21238 cnfval 21239 cnpfval 21240 cnpf2 21256 cnprcl2 21257 ssidcn 21261 iscnp4 21269 iscncl 21275 cncls2 21279 cncls 21280 cnntr 21281 cncnp 21286 lmcls 21308 lmcld 21309 iscnrm2 21344 ist0-2 21350 ist1-2 21353 ishaus2 21357 isreg2 21383 ordtt1 21385 sscmp 21410 dfconn2 21424 clsconn 21435 conncompcld 21439 1stccnp 21467 locfincf 21536 kgenval 21540 kgenuni 21544 1stckgenlem 21558 kgen2ss 21560 kgencn2 21562 txtopon 21596 txuni 21597 pttopon 21601 ptuniconst 21603 txcls 21609 ptclsg 21620 dfac14lem 21622 xkoccn 21624 ptcnplem 21626 ptcn 21632 cnmpt1t 21670 cnmpt2t 21678 cnmpt1res 21681 cnmpt2res 21682 cnmptkp 21685 cnmptk1p 21690 cnmptk2 21691 xkoinjcn 21692 elqtop3 21708 qtoptopon 21709 qtopcld 21718 qtoprest 21722 qtopcmap 21724 kqval 21731 kqcldsat 21738 isr0 21742 r0cld 21743 regr1lem 21744 kqnrmlem1 21748 kqnrmlem2 21749 pt1hmeo 21811 xpstopnlem1 21814 neifil 21885 trnei 21897 elflim 21976 flimss2 21977 flimss1 21978 flimopn 21980 fbflim2 21982 flimclslem 21989 flffval 21994 flfnei 21996 cnpflf2 22005 cnflf 22007 cnflf2 22008 isfcls2 22018 fclsopn 22019 fclsnei 22024 fclscmp 22035 ufilcmp 22037 fcfval 22038 fcfnei 22040 fcfelbas 22041 cnpfcf 22046 cnfcf 22047 alexsublem 22049 tmdcn2 22094 tmdgsum 22100 tmdgsum2 22101 symgtgp 22106 subgntr 22111 opnsubg 22112 clssubg 22113 clsnsg 22114 cldsubg 22115 tgpconncompeqg 22116 tgpconncomp 22117 ghmcnp 22119 snclseqg 22120 tgphaus 22121 tgpt1 22122 prdstmdd 22128 prdstgpd 22129 tsmsgsum 22143 tsmsid 22144 tsmsmhm 22150 tsmsadd 22151 tgptsmscld 22155 utop3cls 22256 mopnuni 22447 isxms2 22454 prdsxmslem2 22535 metdseq0 22858 cnmpt2pc 22928 ishtpy 22972 om1val 23030 pi1val 23037 csscld 23248 clsocv 23249 cfilfcls 23272 relcmpcmet 23315 limcres 23849 limccnp 23854 limccnp2 23855 dvbss 23864 perfdvf 23866 dvreslem 23872 dvres2lem 23873 dvcnp2 23882 dvaddbr 23900 dvmulbr 23901 dvcmulf 23907 dvmptres2 23924 dvmptcmul 23926 dvmptntr 23933 dvcnvrelem2 23980 ftc1cn 24005 taylthlem1 24326 ulmdvlem3 24355 efrlim 24895 pl1cn 30310 cvxpconn 31531 cvxsconn 31532 ivthALT 32636 neibastop2 32662 neibastop3 32663 topmeet 32665 topjoin 32666 refsum2cnlem1 39695 dvresntr 40635 rrxunitopnfi 41015 |
Copyright terms: Public domain | W3C validator |