![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > toponunii | 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 |
---|---|
topontopi.1 | ⊢ 𝐽 ∈ (TopOn‘𝐵) |
Ref | Expression |
---|---|
toponunii | ⊢ 𝐵 = ∪ 𝐽 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | topontopi.1 | . 2 ⊢ 𝐽 ∈ (TopOn‘𝐵) | |
2 | toponuni 22259 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐵 = ∪ 𝐽 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1541 ∈ wcel 2106 ∪ cuni 4864 ‘cfv 6494 TopOnctopon 22255 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5255 ax-nul 5262 ax-pow 5319 ax-pr 5383 ax-un 7669 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2888 df-ral 3064 df-rex 3073 df-rab 3407 df-v 3446 df-dif 3912 df-un 3914 df-in 3916 df-ss 3926 df-nul 4282 df-if 4486 df-pw 4561 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4865 df-br 5105 df-opab 5167 df-mpt 5188 df-id 5530 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-iota 6446 df-fun 6496 df-fv 6502 df-topon 22256 |
This theorem is referenced by: toponrestid 22266 indisuni 22349 indistpsx 22356 letopuni 22554 dfac14 22965 unicntop 24145 sszcld 24176 reperflem 24177 cnperf 24179 iiuni 24240 abscncfALT 24283 cncfcnvcn 24284 cnheiborlem 24313 cnheibor 24314 cnllycmp 24315 bndth 24317 mbfimaopnlem 25015 limcnlp 25238 limcflflem 25240 limcflf 25241 limcmo 25242 limcres 25246 limccnp 25251 limccnp2 25252 perfdvf 25263 recnperf 25265 dvcnp2 25280 dvaddbr 25298 dvmulbr 25299 dvcobr 25306 dvcnvlem 25336 lhop1lem 25373 taylthlem2 25729 abelth 25796 cxpcn3 26097 lgamucov 26383 ftalem3 26420 blocni 29645 ipasslem8 29677 ubthlem1 29710 tpr2uni 32377 tpr2rico 32384 mndpluscn 32398 rmulccn 32400 raddcn 32401 cvxsconn 33728 cvmlift2lem11 33798 ivthALT 34796 poimir 36100 broucube 36101 dvtanlem 36116 ftc1cnnc 36139 dvasin 36151 dvacos 36152 dvreasin 36153 dvreacos 36154 areacirclem2 36156 reheibor 36287 islptre 43830 dirkercncf 44318 fourierdlem62 44379 |
Copyright terms: Public domain | W3C validator |