![]() |
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 20939 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) | |
2 | topontop 20938 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) | |
3 | eqid 2771 | . . . 4 ⊢ ∪ 𝐽 = ∪ 𝐽 | |
4 | 3 | topopn 20931 | . . 3 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽) |
5 | 2, 4 | syl 17 | . 2 ⊢ (𝐽 ∈ (TopOn‘𝐵) → ∪ 𝐽 ∈ 𝐽) |
6 | 1, 5 | eqeltrd 2850 | 1 ⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2145 ∪ cuni 4574 ‘cfv 6031 Topctop 20918 TopOnctopon 20935 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-8 2147 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 ax-sep 4915 ax-nul 4923 ax-pow 4974 ax-pr 5034 ax-un 7096 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-3an 1073 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-eu 2622 df-mo 2623 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ne 2944 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3353 df-sbc 3588 df-dif 3726 df-un 3728 df-in 3730 df-ss 3737 df-nul 4064 df-if 4226 df-pw 4299 df-sn 4317 df-pr 4319 df-op 4323 df-uni 4575 df-br 4787 df-opab 4847 df-mpt 4864 df-id 5157 df-xp 5255 df-rel 5256 df-cnv 5257 df-co 5258 df-dm 5259 df-iota 5994 df-fun 6033 df-fv 6039 df-top 20919 df-topon 20936 |
This theorem is referenced by: topgele 20955 eltpsg 20968 en2top 21010 resttopon 21186 ordtrest 21227 ordtrest2lem 21228 ordtrest2 21229 lmfval 21257 cnpfval 21259 iscn 21260 iscnp 21262 lmbrf 21285 cncls 21299 cnconst2 21308 cnrest2 21311 cndis 21316 cnindis 21317 cnpdis 21318 lmfss 21321 lmres 21325 lmff 21326 ist1-3 21374 connsuba 21444 unconn 21453 kgenval 21559 elkgen 21560 kgentopon 21562 pttoponconst 21621 tx1cn 21633 tx2cn 21634 ptcls 21640 xkoccn 21643 txlm 21672 cnmpt2res 21701 xkoinjcn 21711 qtoprest 21741 ordthmeolem 21825 pt1hmeo 21830 xkocnv 21838 flimclslem 22008 flfval 22014 flfnei 22015 isflf 22017 flfcnp 22028 txflf 22030 supnfcls 22044 fclscf 22049 fclscmp 22054 fcfval 22057 isfcf 22058 uffcfflf 22063 cnpfcf 22065 mopnm 22469 isxms2 22473 prdsxmslem2 22554 bcth2 23346 dvmptid 23940 dvmptc 23941 dvtaylp 24344 taylthlem1 24347 taylthlem2 24348 pige3 24490 dvcxp1 24702 cxpcn3 24710 ordtrestNEW 30307 ordtrest2NEWlem 30308 ordtrest2NEW 30309 topjoin 32697 areacirclem1 33832 |
Copyright terms: Public domain | W3C validator |