![]() |
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 22286 | . 2 β’ (π½ β (TopOnβπ΅) β π΅ = βͺ π½) | |
2 | topontop 22285 | . . 3 β’ (π½ β (TopOnβπ΅) β π½ β Top) | |
3 | eqid 2733 | . . . 4 β’ βͺ π½ = βͺ π½ | |
4 | 3 | topopn 22278 | . . 3 β’ (π½ β Top β βͺ π½ β π½) |
5 | 2, 4 | syl 17 | . 2 β’ (π½ β (TopOnβπ΅) β βͺ π½ β π½) |
6 | 1, 5 | eqeltrd 2834 | 1 β’ (π½ β (TopOnβπ΅) β π΅ β π½) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β wcel 2107 βͺ cuni 4869 βcfv 6500 Topctop 22265 TopOnctopon 22282 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5260 ax-nul 5267 ax-pow 5324 ax-pr 5388 ax-un 7676 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2886 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3449 df-dif 3917 df-un 3919 df-in 3921 df-ss 3931 df-nul 4287 df-if 4491 df-pw 4566 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4870 df-br 5110 df-opab 5172 df-mpt 5193 df-id 5535 df-xp 5643 df-rel 5644 df-cnv 5645 df-co 5646 df-dm 5647 df-iota 6452 df-fun 6502 df-fv 6508 df-top 22266 df-topon 22283 |
This theorem is referenced by: topgele 22302 eltpsg 22315 eltpsgOLD 22316 en2top 22358 resttopon 22535 ordtrest 22576 ordtrest2lem 22577 ordtrest2 22578 lmfval 22606 cnpfval 22608 iscn 22609 iscnp 22611 lmbrf 22634 cncls 22648 cnconst2 22657 cnrest2 22660 cndis 22665 cnindis 22666 cnpdis 22667 lmfss 22670 lmres 22674 lmff 22675 ist1-3 22723 connsuba 22794 unconn 22803 kgenval 22909 elkgen 22910 kgentopon 22912 pttoponconst 22971 tx1cn 22983 tx2cn 22984 ptcls 22990 xkoccn 22993 txlm 23022 cnmpt2res 23051 xkoinjcn 23061 qtoprest 23091 ordthmeolem 23175 pt1hmeo 23180 xkocnv 23188 flimclslem 23358 flfval 23364 flfnei 23365 isflf 23367 flfcnp 23378 txflf 23380 supnfcls 23394 fclscf 23399 fclscmp 23404 fcfval 23407 isfcf 23408 uffcfflf 23413 cnpfcf 23415 mopnm 23820 isxms2 23824 prdsxmslem2 23908 bcth2 24717 dvmptid 25344 dvmptc 25345 dvtaylp 25752 taylthlem1 25755 taylthlem2 25756 pige3ALT 25899 dvcxp1 26116 cxpcn3 26124 ordtrestNEW 32566 ordtrest2NEWlem 32567 ordtrest2NEW 32568 topjoin 34890 areacirclem1 36216 |
Copyright terms: Public domain | W3C validator |