![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > topopn | Structured version Visualization version GIF version |
Description: The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.) |
Ref | Expression |
---|---|
1open.1 | ⊢ 𝑋 = ∪ 𝐽 |
Ref | Expression |
---|---|
topopn | ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1open.1 | . 2 ⊢ 𝑋 = ∪ 𝐽 | |
2 | ssid 3841 | . . 3 ⊢ 𝐽 ⊆ 𝐽 | |
3 | uniopn 21109 | . . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽) | |
4 | 2, 3 | mpan2 681 | . 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽) |
5 | 1, 4 | syl5eqel 2862 | 1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1601 ∈ wcel 2106 ⊆ wss 3791 ∪ cuni 4671 Topctop 21105 |
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 2054 ax-9 2115 ax-10 2134 ax-11 2149 ax-12 2162 ax-ext 2753 ax-sep 5017 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2763 df-cleq 2769 df-clel 2773 df-nfc 2920 df-ral 3094 df-rex 3095 df-v 3399 df-in 3798 df-ss 3805 df-pw 4380 df-uni 4672 df-top 21106 |
This theorem is referenced by: riinopn 21120 toponmax 21138 cldval 21235 ntrfval 21236 clsfval 21237 iscld 21239 ntrval 21248 clsval 21249 0cld 21250 clsval2 21262 ntrtop 21282 toponmre 21305 neifval 21311 neif 21312 neival 21314 isnei 21315 tpnei 21333 lpfval 21350 lpval 21351 restcld 21384 restcls 21393 restntr 21394 cnrest 21497 cmpsub 21612 hauscmplem 21618 cmpfi 21620 isconn2 21626 connsubclo 21636 1stcfb 21657 1stcelcls 21673 islly2 21696 lly1stc 21708 islocfin 21729 finlocfin 21732 cmpkgen 21763 llycmpkgen 21764 ptbasid 21787 ptpjpre2 21792 ptopn2 21796 xkoopn 21801 xkouni 21811 txcld 21815 txcn 21838 ptrescn 21851 txtube 21852 txhaus 21859 xkoptsub 21866 xkopt 21867 xkopjcn 21868 qtoptop 21912 qtopuni 21914 opnfbas 22054 flimval 22175 flimfil 22181 hausflim 22193 hauspwpwf1 22199 hauspwpwdom 22200 flimfnfcls 22240 cnpfcfi 22252 bcthlem5 23534 dvply1 24476 cldssbrsiga 30848 dya2iocucvr 30944 kur14lem7 31793 kur14lem9 31795 connpconn 31816 cvmliftmolem1 31862 ordtop 33018 ntrelmap 39361 clselmap 39363 dssmapntrcls 39364 dssmapclsntr 39365 reopn 40393 |
Copyright terms: Public domain | W3C validator |