| 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 22918 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) | |
| 2 | 1 | simprbi 496 | 1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2108 ∪ cuni 4907 ‘cfv 6561 Topctop 22899 TopOnctopon 22916 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-iota 6514 df-fun 6563 df-fv 6569 df-topon 22917 |
| This theorem is referenced by: toponunii 22922 toponmax 22932 toponss 22933 toponcom 22934 topgele 22936 topontopn 22946 toponmre 23101 cldmreon 23102 restuni 23170 resttopon2 23176 restlp 23191 restperf 23192 perfopn 23193 ordtcld1 23205 ordtcld2 23206 lmfval 23240 cnfval 23241 cnpfval 23242 cnpf2 23258 cnprcl2 23259 ssidcn 23263 iscnp4 23271 iscncl 23277 cncls2 23281 cncls 23282 cnntr 23283 cncnp 23288 lmcls 23310 lmcld 23311 iscnrm2 23346 ist0-2 23352 ist1-2 23355 ishaus2 23359 isreg2 23385 ordtt1 23387 sscmp 23413 dfconn2 23427 clsconn 23438 conncompcld 23442 1stccnp 23470 locfincf 23539 kgenval 23543 kgenuni 23547 1stckgenlem 23561 kgen2ss 23563 kgencn2 23565 txtopon 23599 txuni 23600 pttopon 23604 ptuniconst 23606 txcls 23612 ptclsg 23623 dfac14lem 23625 xkoccn 23627 ptcnplem 23629 ptcn 23635 cnmpt1t 23673 cnmpt2t 23681 cnmpt1res 23684 cnmpt2res 23685 cnmptkp 23688 cnmptk1p 23693 cnmptk2 23694 xkoinjcn 23695 elqtop3 23711 qtoptopon 23712 qtopcld 23721 qtoprest 23725 qtopcmap 23727 kqval 23734 kqcldsat 23741 isr0 23745 r0cld 23746 regr1lem 23747 kqnrmlem1 23751 kqnrmlem2 23752 pt1hmeo 23814 xpstopnlem1 23817 neifil 23888 trnei 23900 elflim 23979 flimss2 23980 flimss1 23981 flimopn 23983 fbflim2 23985 flimclslem 23992 flffval 23997 flfnei 23999 cnpflf2 24008 cnflf 24010 cnflf2 24011 isfcls2 24021 fclsopn 24022 fclsnei 24027 fclscmp 24038 ufilcmp 24040 fcfval 24041 fcfnei 24043 fcfelbas 24044 cnpfcf 24049 cnfcf 24050 alexsublem 24052 tmdcn2 24097 tmdgsum 24103 tmdgsum2 24104 symgtgp 24114 subgntr 24115 opnsubg 24116 clssubg 24117 clsnsg 24118 cldsubg 24119 tgpconncompeqg 24120 tgpconncomp 24121 ghmcnp 24123 snclseqg 24124 tgphaus 24125 tgpt1 24126 prdstmdd 24132 prdstgpd 24133 tsmsgsum 24147 tsmsid 24148 tsmsmhm 24154 tsmsadd 24155 tgptsmscld 24159 utop3cls 24260 mopnuni 24451 isxms2 24458 prdsxmslem2 24542 metdseq0 24876 cnmpopc 24955 ishtpy 25004 om1val 25063 pi1val 25070 csscld 25283 clsocv 25284 cfilfcls 25308 relcmpcmet 25352 limcres 25921 limccnp 25926 limccnp2 25927 dvbss 25936 perfdvf 25938 dvreslem 25944 dvres2lem 25945 dvcnp2 25955 dvcnp2OLD 25956 dvaddbr 25974 dvmulbr 25975 dvmulbrOLD 25976 dvcmulf 25982 dvmptres2 26000 dvmptcmul 26002 dvmptntr 26009 dvcnvrelem2 26057 ftc1cn 26084 taylthlem1 26415 ulmdvlem3 26445 efrlim 27012 efrlimOLD 27013 zart0 33878 zarmxt1 33879 pl1cn 33954 cvxpconn 35247 cvxsconn 35248 ivthALT 36336 neibastop2 36362 neibastop3 36363 topmeet 36365 topjoin 36366 refsum2cnlem1 45042 dvresntr 45933 rrxunitopnfi 46307 |
| Copyright terms: Public domain | W3C validator |