![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > topopn | Structured version Visualization version Unicode 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 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1open.1 |
. 2
![]() ![]() ![]() ![]() ![]() | |
2 | ssid 3462 |
. . 3
![]() ![]() ![]() ![]() | |
3 | uniopn 19975 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | mpan2 682 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | syl5eqel 2543 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 ax-sep 4538 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-nfc 2591 df-ral 2753 df-rex 2754 df-v 3058 df-in 3422 df-ss 3429 df-pw 3964 df-uni 4212 df-top 19969 |
This theorem is referenced by: riinopn 19986 toponmax 19991 cldval 20086 ntrfval 20087 clsfval 20088 iscld 20090 ntrval 20099 clsval 20100 0cld 20101 clsval2 20113 ntrtop 20134 toponmre 20157 neifval 20163 neif 20164 neival 20166 isnei 20167 tpnei 20185 lpfval 20202 lpval 20203 restcld 20236 restcls 20245 restntr 20246 cnrest 20349 cmpsub 20463 hauscmplem 20469 cmpfi 20471 iscon2 20477 consubclo 20487 1stcfb 20508 1stcelcls 20524 islly2 20547 lly1stc 20559 islocfin 20580 finlocfin 20583 cmpkgen 20614 llycmpkgen 20615 ptbasid 20638 ptpjpre2 20643 ptopn2 20647 xkoopn 20652 xkouni 20662 txcld 20666 txcn 20689 ptrescn 20702 txtube 20703 txhaus 20710 xkoptsub 20717 xkopt 20718 xkopjcn 20719 qtoptop 20763 qtopuni 20765 opnfbas 20905 flimval 21026 flimfil 21032 hausflim 21044 hauspwpwf1 21050 hauspwpwdom 21051 flimfnfcls 21091 cnpfcfi 21103 bcthlem5 22344 dvply1 23285 cldssbrsiga 29057 dya2iocucvr 29154 kur14lem7 29983 kur14lem9 29985 conpcon 30006 cvmliftmolem1 30052 ordtop 31144 reopn 37539 |
Copyright terms: Public domain | W3C validator |