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 21517 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐵 = ∪ 𝐽 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1536 ∈ wcel 2113 ∪ cuni 4831 ‘cfv 6348 TopOnctopon 21513 |
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 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2792 ax-sep 5196 ax-nul 5203 ax-pow 5259 ax-pr 5323 ax-un 7454 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1084 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-mo 2621 df-eu 2653 df-clab 2799 df-cleq 2813 df-clel 2892 df-nfc 2962 df-ral 3142 df-rex 3143 df-rab 3146 df-v 3493 df-sbc 3769 df-dif 3932 df-un 3934 df-in 3936 df-ss 3945 df-nul 4285 df-if 4461 df-pw 4534 df-sn 4561 df-pr 4563 df-op 4567 df-uni 4832 df-br 5060 df-opab 5122 df-mpt 5140 df-id 5453 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-iota 6307 df-fun 6350 df-fv 6356 df-topon 21514 |
This theorem is referenced by: toponrestid 21524 indisuni 21606 indistpsx 21613 letopuni 21810 dfac14 22221 unicntop 23389 sszcld 23420 reperflem 23421 cnperf 23423 iiuni 23484 abscncfALT 23523 cncfcnvcn 23524 cnheiborlem 23553 cnheibor 23554 cnllycmp 23555 bndth 23557 mbfimaopnlem 24251 limcnlp 24473 limcflflem 24475 limcflf 24476 limcmo 24477 limcres 24481 limccnp 24486 limccnp2 24487 perfdvf 24498 recnperf 24500 dvcnp2 24514 dvaddbr 24532 dvmulbr 24533 dvcobr 24540 dvcnvlem 24570 lhop1lem 24607 taylthlem2 24960 abelth 25027 cxpcn3 25327 lgamucov 25613 ftalem3 25650 blocni 28580 ipasslem8 28612 ubthlem1 28645 tpr2uni 31169 tpr2rico 31176 mndpluscn 31190 rmulccn 31192 raddcn 31193 cvxsconn 32511 cvmlift2lem11 32581 ivthALT 33704 poimir 34960 broucube 34961 dvtanlem 34976 ftc1cnnc 34999 dvasin 35011 dvacos 35012 dvreasin 35013 dvreacos 35014 areacirclem2 35016 reheibor 35150 islptre 41974 dirkercncf 42466 fourierdlem62 42527 |
Copyright terms: Public domain | W3C validator |