![]() |
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 3999 | . . 3 ⊢ 𝐽 ⊆ 𝐽 | |
3 | uniopn 22843 | . . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐽 ⊆ 𝐽) → ∪ 𝐽 ∈ 𝐽) | |
4 | 2, 3 | mpan2 689 | . 2 ⊢ (𝐽 ∈ Top → ∪ 𝐽 ∈ 𝐽) |
5 | 1, 4 | eqeltrid 2829 | 1 ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1533 ∈ wcel 2098 ⊆ wss 3944 ∪ cuni 4909 Topctop 22839 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 ax-sep 5300 |
This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1086 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 df-rex 3060 df-rab 3419 df-v 3463 df-in 3951 df-ss 3961 df-pw 4606 df-uni 4910 df-top 22840 |
This theorem is referenced by: riinopn 22854 toponmax 22872 cldval 22971 ntrfval 22972 clsfval 22973 iscld 22975 ntrval 22984 clsval 22985 0cld 22986 clsval2 22998 ntrtop 23018 toponmre 23041 neifval 23047 neif 23048 neival 23050 isnei 23051 tpnei 23069 lpfval 23086 lpval 23087 restcld 23120 restcls 23129 restntr 23130 cnrest 23233 cmpsub 23348 hauscmplem 23354 cmpfi 23356 isconn2 23362 connsubclo 23372 1stcfb 23393 1stcelcls 23409 islly2 23432 lly1stc 23444 islocfin 23465 finlocfin 23468 cmpkgen 23499 llycmpkgen 23500 ptbasid 23523 ptpjpre2 23528 ptopn2 23532 xkoopn 23537 xkouni 23547 txcld 23551 txcn 23574 ptrescn 23587 txtube 23588 txhaus 23595 xkoptsub 23602 xkopt 23603 xkopjcn 23604 qtoptop 23648 qtopuni 23650 opnfbas 23790 flimval 23911 flimfil 23917 hausflim 23929 hauspwpwf1 23935 hauspwpwdom 23936 flimfnfcls 23976 cnpfcfi 23988 bcthlem5 25300 dvply1 26263 cldssbrsiga 33937 dya2iocucvr 34035 kur14lem7 34953 kur14lem9 34955 connpconn 34976 cvmliftmolem1 35022 ordtop 36051 pibt2 37027 ntrelmap 43697 clselmap 43699 dssmapntrcls 43700 dssmapclsntr 43701 toprestsubel 44664 reopn 44809 toplatglb0 48196 |
Copyright terms: Public domain | W3C validator |