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 21783 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ 𝐵 = ∪ 𝐽 |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1543 ∈ wcel 2110 ∪ cuni 4809 ‘cfv 6369 TopOnctopon 21779 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2706 ax-sep 5181 ax-nul 5188 ax-pow 5247 ax-pr 5311 ax-un 7512 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2537 df-eu 2566 df-clab 2713 df-cleq 2726 df-clel 2812 df-nfc 2882 df-ne 2936 df-ral 3059 df-rex 3060 df-rab 3063 df-v 3403 df-sbc 3688 df-dif 3860 df-un 3862 df-in 3864 df-ss 3874 df-nul 4228 df-if 4430 df-pw 4505 df-sn 4532 df-pr 4534 df-op 4538 df-uni 4810 df-br 5044 df-opab 5106 df-mpt 5125 df-id 5444 df-xp 5546 df-rel 5547 df-cnv 5548 df-co 5549 df-dm 5550 df-iota 6327 df-fun 6371 df-fv 6377 df-topon 21780 |
This theorem is referenced by: toponrestid 21790 indisuni 21872 indistpsx 21879 letopuni 22076 dfac14 22487 unicntop 23655 sszcld 23686 reperflem 23687 cnperf 23689 iiuni 23750 abscncfALT 23793 cncfcnvcn 23794 cnheiborlem 23823 cnheibor 23824 cnllycmp 23825 bndth 23827 mbfimaopnlem 24524 limcnlp 24747 limcflflem 24749 limcflf 24750 limcmo 24751 limcres 24755 limccnp 24760 limccnp2 24761 perfdvf 24772 recnperf 24774 dvcnp2 24789 dvaddbr 24807 dvmulbr 24808 dvcobr 24815 dvcnvlem 24845 lhop1lem 24882 taylthlem2 25238 abelth 25305 cxpcn3 25606 lgamucov 25892 ftalem3 25929 blocni 28858 ipasslem8 28890 ubthlem1 28923 tpr2uni 31541 tpr2rico 31548 mndpluscn 31562 rmulccn 31564 raddcn 31565 cvxsconn 32890 cvmlift2lem11 32960 ivthALT 34218 poimir 35504 broucube 35505 dvtanlem 35520 ftc1cnnc 35543 dvasin 35555 dvacos 35556 dvreasin 35557 dvreacos 35558 areacirclem2 35560 reheibor 35691 islptre 42789 dirkercncf 43277 fourierdlem62 43338 |
Copyright terms: Public domain | W3C validator |