![]() |
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 20765 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) | |
2 | 1 | simprbi 479 | 1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1523 ∈ wcel 2030 ∪ cuni 4468 ‘cfv 5926 Topctop 20746 TopOnctopon 20763 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-8 2032 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 ax-sep 4814 ax-nul 4822 ax-pow 4873 ax-pr 4936 ax-un 6991 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1056 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-eu 2502 df-mo 2503 df-clab 2638 df-cleq 2644 df-clel 2647 df-nfc 2782 df-ne 2824 df-ral 2946 df-rex 2947 df-rab 2950 df-v 3233 df-sbc 3469 df-dif 3610 df-un 3612 df-in 3614 df-ss 3621 df-nul 3949 df-if 4120 df-pw 4193 df-sn 4211 df-pr 4213 df-op 4217 df-uni 4469 df-br 4686 df-opab 4746 df-mpt 4763 df-id 5053 df-xp 5149 df-rel 5150 df-cnv 5151 df-co 5152 df-dm 5153 df-iota 5889 df-fun 5928 df-fv 5934 df-topon 20764 |
This theorem is referenced by: toponunii 20769 toponmax 20778 toponss 20779 toponcom 20780 topgele 20782 topontopn 20792 toponmre 20945 cldmreon 20946 restuni 21014 resttopon2 21020 restlp 21035 restperf 21036 perfopn 21037 ordtcld1 21049 ordtcld2 21050 lmfval 21084 cnfval 21085 cnpfval 21086 cnpf2 21102 cnprcl2 21103 ssidcn 21107 iscnp4 21115 iscncl 21121 cncls2 21125 cncls 21126 cnntr 21127 cncnp 21132 lmcls 21154 lmcld 21155 iscnrm2 21190 ist0-2 21196 ist1-2 21199 ishaus2 21203 isreg2 21229 ordtt1 21231 sscmp 21256 dfconn2 21270 clsconn 21281 conncompcld 21285 1stccnp 21313 locfincf 21382 kgenval 21386 kgenuni 21390 1stckgenlem 21404 kgen2ss 21406 kgencn2 21408 txtopon 21442 txuni 21443 pttopon 21447 ptuniconst 21449 txcls 21455 ptclsg 21466 dfac14lem 21468 xkoccn 21470 ptcnplem 21472 ptcn 21478 cnmpt1t 21516 cnmpt2t 21524 cnmpt1res 21527 cnmpt2res 21528 cnmptkp 21531 cnmptk1p 21536 cnmptk2 21537 xkoinjcn 21538 elqtop3 21554 qtoptopon 21555 qtopcld 21564 qtoprest 21568 qtopcmap 21570 kqval 21577 kqcldsat 21584 isr0 21588 r0cld 21589 regr1lem 21590 kqnrmlem1 21594 kqnrmlem2 21595 pt1hmeo 21657 xpstopnlem1 21660 neifil 21731 trnei 21743 elflim 21822 flimss2 21823 flimss1 21824 flimopn 21826 fbflim2 21828 flimclslem 21835 flffval 21840 flfnei 21842 cnpflf2 21851 cnflf 21853 cnflf2 21854 isfcls2 21864 fclsopn 21865 fclsnei 21870 fclscmp 21881 ufilcmp 21883 fcfval 21884 fcfnei 21886 fcfelbas 21887 cnpfcf 21892 cnfcf 21893 alexsublem 21895 tmdcn2 21940 tmdgsum 21946 tmdgsum2 21947 symgtgp 21952 subgntr 21957 opnsubg 21958 clssubg 21959 clsnsg 21960 cldsubg 21961 tgpconncompeqg 21962 tgpconncomp 21963 ghmcnp 21965 snclseqg 21966 tgphaus 21967 tgpt1 21968 prdstmdd 21974 prdstgpd 21975 tsmsgsum 21989 tsmsid 21990 tsmsmhm 21996 tsmsadd 21997 tgptsmscld 22001 utop3cls 22102 mopnuni 22293 isxms2 22300 prdsxmslem2 22381 metdseq0 22704 cnmpt2pc 22774 ishtpy 22818 om1val 22876 pi1val 22883 csscld 23094 clsocv 23095 cfilfcls 23118 relcmpcmet 23161 limcres 23695 limccnp 23700 limccnp2 23701 dvbss 23710 perfdvf 23712 dvreslem 23718 dvres2lem 23719 dvcnp2 23728 dvaddbr 23746 dvmulbr 23747 dvcmulf 23753 dvmptres2 23770 dvmptcmul 23772 dvmptntr 23779 dvcnvrelem2 23826 ftc1cn 23851 taylthlem1 24172 ulmdvlem3 24201 efrlim 24741 pl1cn 30129 cvxpconn 31350 cvxsconn 31351 ivthALT 32455 neibastop2 32481 neibastop3 32482 topmeet 32484 topjoin 32485 refsum2cnlem1 39510 dvresntr 40450 rrxunitopnfi 40830 |
Copyright terms: Public domain | W3C validator |