![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > toponmax | Structured version Visualization version GIF version |
Description: The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
Ref | Expression |
---|---|
toponmax | ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | toponuni 21126 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) | |
2 | topontop 21125 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) | |
3 | eqid 2778 | . . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
4 | 3 | topopn 21118 | . . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽) |
5 | 2, 4 | syl 17 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽) |
6 | 1, 5 | eqeltrd 2859 | 1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2107 ∪ cuni 4671 ‘cfv 6135 Topctop 21105 TopOnctopon 21122 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-8 2109 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 ax-sep 5017 ax-nul 5025 ax-pow 5077 ax-pr 5138 ax-un 7226 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-mo 2551 df-eu 2587 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ral 3095 df-rex 3096 df-rab 3099 df-v 3400 df-sbc 3653 df-dif 3795 df-un 3797 df-in 3799 df-ss 3806 df-nul 4142 df-if 4308 df-pw 4381 df-sn 4399 df-pr 4401 df-op 4405 df-uni 4672 df-br 4887 df-opab 4949 df-mpt 4966 df-id 5261 df-xp 5361 df-rel 5362 df-cnv 5363 df-co 5364 df-dm 5365 df-iota 6099 df-fun 6137 df-fv 6143 df-top 21106 df-topon 21123 |
This theorem is referenced by: topgele 21142 eltpsg 21155 en2top 21197 resttopon 21373 ordtrest 21414 ordtrest2lem 21415 ordtrest2 21416 lmfval 21444 cnpfval 21446 iscn 21447 iscnp 21449 lmbrf 21472 cncls 21486 cnconst2 21495 cnrest2 21498 cndis 21503 cnindis 21504 cnpdis 21505 lmfss 21508 lmres 21512 lmff 21513 ist1-3 21561 connsuba 21632 unconn 21641 kgenval 21747 elkgen 21748 kgentopon 21750 pttoponconst 21809 tx1cn 21821 tx2cn 21822 ptcls 21828 xkoccn 21831 txlm 21860 cnmpt2res 21889 xkoinjcn 21899 qtoprest 21929 ordthmeolem 22013 pt1hmeo 22018 xkocnv 22026 flimclslem 22196 flfval 22202 flfnei 22203 isflf 22205 flfcnp 22216 txflf 22218 supnfcls 22232 fclscf 22237 fclscmp 22242 fcfval 22245 isfcf 22246 uffcfflf 22251 cnpfcf 22253 mopnm 22657 isxms2 22661 prdsxmslem2 22742 bcth2 23536 dvmptid 24157 dvmptc 24158 dvtaylp 24561 taylthlem1 24564 taylthlem2 24565 pige3 24707 dvcxp1 24921 cxpcn3 24929 ordtrestNEW 30565 ordtrest2NEWlem 30566 ordtrest2NEW 30567 topjoin 32948 areacirclem1 34127 |
Copyright terms: Public domain | W3C validator |