Nearby theorems
|
|
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
| Mirrors > Home > MPE Home > Th. List > unitg | Structured version Visualization version GIF version | ||
| Description: The topology generated by a basis π΅ is a topology on βͺ π΅. Importantly, this theorem means that we don't have to specify separately the base set for the topological space generated by a basis. In other words, any member of the class TopBases completely specifies the basis it corresponds to. (Contributed by NM, 16-Jul-2006.) (Proof shortened by OpenAI, 30-Mar-2020.) |
| Ref | Expression |
|---|---|
| unitg | β’ (π΅ β π β βͺ (topGenβπ΅) = βͺ π΅) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tg1 22897 | . . . . . 6 β’ (π₯ β (topGenβπ΅) β π₯ β βͺ π΅) | |
| 2 | velpw 4608 | . . . . . 6 β’ (π₯ β π« βͺ π΅ β π₯ β βͺ π΅) | |
| 3 | 1, 2 | sylibr 233 | . . . . 5 β’ (π₯ β (topGenβπ΅) β π₯ β π« βͺ π΅) |
| 4 | 3 | ssriv 3981 | . . . 4 β’ (topGenβπ΅) β π« βͺ π΅ |
| 5 | sspwuni 5103 | . . . 4 β’ ((topGenβπ΅) β π« βͺ π΅ β βͺ (topGenβπ΅) β βͺ π΅) | |
| 6 | 4, 5 | mpbi 229 | . . 3 β’ βͺ (topGenβπ΅) β βͺ π΅ |
| 7 | 6 | a1i 11 | . 2 β’ (π΅ β π β βͺ (topGenβπ΅) β βͺ π΅) |
| 8 | bastg 22899 | . . 3 β’ (π΅ β π β π΅ β (topGenβπ΅)) | |
| 9 | 8 | unissd 4918 | . 2 β’ (π΅ β π β βͺ π΅ β βͺ (topGenβπ΅)) |
| 10 | 7, 9 | eqssd 3995 | 1 β’ (π΅ β π β βͺ (topGenβπ΅) = βͺ π΅) |
| Colors of variables: wff setvar class |
| Syntax hints: β wi 4 = wceq 1533 β wcel 2098 β wss 3945 π« cpw 4603 βͺ cuni 4908 βcfv 6547 topGenctg 17418 |
| 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-10 2129 ax-11 2146 ax-12 2166 ax-ext 2696 ax-sep 5299 ax-nul 5306 ax-pow 5364 ax-pr 5428 ax-un 7739 |
| This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1536 df-fal 1546 df-ex 1774 df-nf 1778 df-sb 2060 df-mo 2528 df-eu 2557 df-clab 2703 df-cleq 2717 df-clel 2802 df-nfc 2877 df-ral 3052 df-rex 3061 df-rab 3420 df-v 3465 df-dif 3948 df-un 3950 df-in 3952 df-ss 3962 df-nul 4324 df-if 4530 df-pw 4605 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4909 df-br 5149 df-opab 5211 df-mpt 5232 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-iota 6499 df-fun 6549 df-fv 6555 df-topgen 17424 |
| This theorem is referenced by: tgcl 22902 tgtopon 22904 tgcmp 23335 2ndcsep 23393 txtopon 23525 ptuni 23528 xkouni 23533 prdstopn 23562 tgqtop 23646 alexsubb 23980 alexsubALTlem3 23983 alexsubALTlem4 23984 ptcmplem1 23986 uniretop 24709 fneval 35906 fnemeet1 35920 kelac2 42554 |
| Copyright terms: Public domain | W3C validator |