![]() |
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 22416 | . 2 β’ (π½ β (TopOnβπ΅) β π΅ = βͺ π½) | |
2 | topontop 22415 | . . 3 β’ (π½ β (TopOnβπ΅) β π½ β Top) | |
3 | eqid 2733 | . . . 4 β’ βͺ π½ = βͺ π½ | |
4 | 3 | topopn 22408 | . . 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 4909 βcfv 6544 Topctop 22395 TopOnctopon 22412 |
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 5300 ax-nul 5307 ax-pow 5364 ax-pr 5428 ax-un 7725 |
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 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-mpt 5233 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-iota 6496 df-fun 6546 df-fv 6552 df-top 22396 df-topon 22413 |
This theorem is referenced by: topgele 22432 eltpsg 22445 eltpsgOLD 22446 en2top 22488 resttopon 22665 ordtrest 22706 ordtrest2lem 22707 ordtrest2 22708 lmfval 22736 cnpfval 22738 iscn 22739 iscnp 22741 lmbrf 22764 cncls 22778 cnconst2 22787 cnrest2 22790 cndis 22795 cnindis 22796 cnpdis 22797 lmfss 22800 lmres 22804 lmff 22805 ist1-3 22853 connsuba 22924 unconn 22933 kgenval 23039 elkgen 23040 kgentopon 23042 pttoponconst 23101 tx1cn 23113 tx2cn 23114 ptcls 23120 xkoccn 23123 txlm 23152 cnmpt2res 23181 xkoinjcn 23191 qtoprest 23221 ordthmeolem 23305 pt1hmeo 23310 xkocnv 23318 flimclslem 23488 flfval 23494 flfnei 23495 isflf 23497 flfcnp 23508 txflf 23510 supnfcls 23524 fclscf 23529 fclscmp 23534 fcfval 23537 isfcf 23538 uffcfflf 23543 cnpfcf 23545 mopnm 23950 isxms2 23954 prdsxmslem2 24038 bcth2 24847 dvmptid 25474 dvmptc 25475 dvtaylp 25882 taylthlem1 25885 taylthlem2 25886 pige3ALT 26029 dvcxp1 26248 cxpcn3 26256 ordtrestNEW 32901 ordtrest2NEWlem 32902 ordtrest2NEW 32903 topjoin 35250 areacirclem1 36576 |
Copyright terms: Public domain | W3C validator |