![]() |
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 22734 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) | |
2 | 1 | simprbi 496 | 1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1540 ∈ wcel 2105 ∪ cuni 4908 ‘cfv 6543 Topctop 22715 TopOnctopon 22732 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ral 3061 df-rex 3070 df-rab 3432 df-v 3475 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5574 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-iota 6495 df-fun 6545 df-fv 6551 df-topon 22733 |
This theorem is referenced by: toponunii 22738 toponmax 22748 toponss 22749 toponcom 22750 topgele 22752 topontopn 22762 toponmre 22917 cldmreon 22918 restuni 22986 resttopon2 22992 restlp 23007 restperf 23008 perfopn 23009 ordtcld1 23021 ordtcld2 23022 lmfval 23056 cnfval 23057 cnpfval 23058 cnpf2 23074 cnprcl2 23075 ssidcn 23079 iscnp4 23087 iscncl 23093 cncls2 23097 cncls 23098 cnntr 23099 cncnp 23104 lmcls 23126 lmcld 23127 iscnrm2 23162 ist0-2 23168 ist1-2 23171 ishaus2 23175 isreg2 23201 ordtt1 23203 sscmp 23229 dfconn2 23243 clsconn 23254 conncompcld 23258 1stccnp 23286 locfincf 23355 kgenval 23359 kgenuni 23363 1stckgenlem 23377 kgen2ss 23379 kgencn2 23381 txtopon 23415 txuni 23416 pttopon 23420 ptuniconst 23422 txcls 23428 ptclsg 23439 dfac14lem 23441 xkoccn 23443 ptcnplem 23445 ptcn 23451 cnmpt1t 23489 cnmpt2t 23497 cnmpt1res 23500 cnmpt2res 23501 cnmptkp 23504 cnmptk1p 23509 cnmptk2 23510 xkoinjcn 23511 elqtop3 23527 qtoptopon 23528 qtopcld 23537 qtoprest 23541 qtopcmap 23543 kqval 23550 kqcldsat 23557 isr0 23561 r0cld 23562 regr1lem 23563 kqnrmlem1 23567 kqnrmlem2 23568 pt1hmeo 23630 xpstopnlem1 23633 neifil 23704 trnei 23716 elflim 23795 flimss2 23796 flimss1 23797 flimopn 23799 fbflim2 23801 flimclslem 23808 flffval 23813 flfnei 23815 cnpflf2 23824 cnflf 23826 cnflf2 23827 isfcls2 23837 fclsopn 23838 fclsnei 23843 fclscmp 23854 ufilcmp 23856 fcfval 23857 fcfnei 23859 fcfelbas 23860 cnpfcf 23865 cnfcf 23866 alexsublem 23868 tmdcn2 23913 tmdgsum 23919 tmdgsum2 23920 symgtgp 23930 subgntr 23931 opnsubg 23932 clssubg 23933 clsnsg 23934 cldsubg 23935 tgpconncompeqg 23936 tgpconncomp 23937 ghmcnp 23939 snclseqg 23940 tgphaus 23941 tgpt1 23942 prdstmdd 23948 prdstgpd 23949 tsmsgsum 23963 tsmsid 23964 tsmsmhm 23970 tsmsadd 23971 tgptsmscld 23975 utop3cls 24076 mopnuni 24267 isxms2 24274 prdsxmslem2 24358 metdseq0 24690 cnmpopc 24769 ishtpy 24818 om1val 24877 pi1val 24884 csscld 25097 clsocv 25098 cfilfcls 25122 relcmpcmet 25166 limcres 25735 limccnp 25740 limccnp2 25741 dvbss 25750 perfdvf 25752 dvreslem 25758 dvres2lem 25759 dvcnp2 25769 dvcnp2OLD 25770 dvaddbr 25788 dvmulbr 25789 dvmulbrOLD 25790 dvcmulf 25796 dvmptres2 25814 dvmptcmul 25816 dvmptntr 25823 dvcnvrelem2 25871 ftc1cn 25898 taylthlem1 26224 ulmdvlem3 26253 efrlim 26815 zart0 33323 zarmxt1 33324 pl1cn 33399 cvxpconn 34697 cvxsconn 34698 ivthALT 35684 neibastop2 35710 neibastop3 35711 topmeet 35713 topjoin 35714 refsum2cnlem1 44184 dvresntr 45093 rrxunitopnfi 45467 |
Copyright terms: Public domain | W3C validator |