![]() |
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 21240 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) | |
2 | 1 | simprbi 489 | 1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1508 ∈ wcel 2051 ∪ cuni 4709 ‘cfv 6186 Topctop 21221 TopOnctopon 21238 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2745 ax-sep 5057 ax-nul 5064 ax-pow 5116 ax-pr 5183 ax-un 7278 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2548 df-eu 2585 df-clab 2754 df-cleq 2766 df-clel 2841 df-nfc 2913 df-ral 3088 df-rex 3089 df-rab 3092 df-v 3412 df-sbc 3677 df-dif 3827 df-un 3829 df-in 3831 df-ss 3838 df-nul 4174 df-if 4346 df-pw 4419 df-sn 4437 df-pr 4439 df-op 4443 df-uni 4710 df-br 4927 df-opab 4989 df-mpt 5006 df-id 5309 df-xp 5410 df-rel 5411 df-cnv 5412 df-co 5413 df-dm 5414 df-iota 6150 df-fun 6188 df-fv 6194 df-topon 21239 |
This theorem is referenced by: toponunii 21244 toponmax 21254 toponss 21255 toponcom 21256 topgele 21258 topontopn 21268 toponmre 21421 cldmreon 21422 restuni 21490 resttopon2 21496 restlp 21511 restperf 21512 perfopn 21513 ordtcld1 21525 ordtcld2 21526 lmfval 21560 cnfval 21561 cnpfval 21562 cnpf2 21578 cnprcl2 21579 ssidcn 21583 iscnp4 21591 iscncl 21597 cncls2 21601 cncls 21602 cnntr 21603 cncnp 21608 lmcls 21630 lmcld 21631 iscnrm2 21666 ist0-2 21672 ist1-2 21675 ishaus2 21679 isreg2 21705 ordtt1 21707 sscmp 21733 dfconn2 21747 clsconn 21758 conncompcld 21762 1stccnp 21790 locfincf 21859 kgenval 21863 kgenuni 21867 1stckgenlem 21881 kgen2ss 21883 kgencn2 21885 txtopon 21919 txuni 21920 pttopon 21924 ptuniconst 21926 txcls 21932 ptclsg 21943 dfac14lem 21945 xkoccn 21947 ptcnplem 21949 ptcn 21955 cnmpt1t 21993 cnmpt2t 22001 cnmpt1res 22004 cnmpt2res 22005 cnmptkp 22008 cnmptk1p 22013 cnmptk2 22014 xkoinjcn 22015 elqtop3 22031 qtoptopon 22032 qtopcld 22041 qtoprest 22045 qtopcmap 22047 kqval 22054 kqcldsat 22061 isr0 22065 r0cld 22066 regr1lem 22067 kqnrmlem1 22071 kqnrmlem2 22072 pt1hmeo 22134 xpstopnlem1 22137 neifil 22208 trnei 22220 elflim 22299 flimss2 22300 flimss1 22301 flimopn 22303 fbflim2 22305 flimclslem 22312 flffval 22317 flfnei 22319 cnpflf2 22328 cnflf 22330 cnflf2 22331 isfcls2 22341 fclsopn 22342 fclsnei 22347 fclscmp 22358 ufilcmp 22360 fcfval 22361 fcfnei 22363 fcfelbas 22364 cnpfcf 22369 cnfcf 22370 alexsublem 22372 tmdcn2 22417 tmdgsum 22423 tmdgsum2 22424 symgtgp 22429 subgntr 22434 opnsubg 22435 clssubg 22436 clsnsg 22437 cldsubg 22438 tgpconncompeqg 22439 tgpconncomp 22440 ghmcnp 22442 snclseqg 22443 tgphaus 22444 tgpt1 22445 prdstmdd 22451 prdstgpd 22452 tsmsgsum 22466 tsmsid 22467 tsmsmhm 22473 tsmsadd 22474 tgptsmscld 22478 utop3cls 22579 mopnuni 22770 isxms2 22777 prdsxmslem2 22858 metdseq0 23181 cnmpopc 23251 ishtpy 23295 om1val 23353 pi1val 23360 csscld 23571 clsocv 23572 cfilfcls 23596 relcmpcmet 23640 limcres 24203 limccnp 24208 limccnp2 24209 dvbss 24218 perfdvf 24220 dvreslem 24226 dvres2lem 24227 dvcnp2 24236 dvaddbr 24254 dvmulbr 24255 dvcmulf 24261 dvmptres2 24278 dvmptcmul 24280 dvmptntr 24287 dvcnvrelem2 24334 ftc1cn 24359 taylthlem1 24680 ulmdvlem3 24709 efrlim 25265 pl1cn 30875 cvxpconn 32107 cvxsconn 32108 ivthALT 33237 neibastop2 33263 neibastop3 33264 topmeet 33266 topjoin 33267 refsum2cnlem1 40747 dvresntr 41662 rrxunitopnfi 42038 |
Copyright terms: Public domain | W3C validator |