Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > resttop | Structured version Visualization version GIF version |
Description: A subspace topology is a topology. Definition of subspace topology in [Munkres] p. 89. π΄ is normally a subset of the base set of π½. (Contributed by FL, 15-Apr-2007.) (Revised by Mario Carneiro, 1-May-2015.) |
Ref | Expression |
---|---|
resttop | β’ ((π½ β Top β§ π΄ β π) β (π½ βΎt π΄) β Top) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tgrest 22351 | . . 3 β’ ((π½ β Top β§ π΄ β π) β (topGenβ(π½ βΎt π΄)) = ((topGenβπ½) βΎt π΄)) | |
2 | tgtop 22164 | . . . . 5 β’ (π½ β Top β (topGenβπ½) = π½) | |
3 | 2 | adantr 482 | . . . 4 β’ ((π½ β Top β§ π΄ β π) β (topGenβπ½) = π½) |
4 | 3 | oveq1d 7318 | . . 3 β’ ((π½ β Top β§ π΄ β π) β ((topGenβπ½) βΎt π΄) = (π½ βΎt π΄)) |
5 | 1, 4 | eqtrd 2776 | . 2 β’ ((π½ β Top β§ π΄ β π) β (topGenβ(π½ βΎt π΄)) = (π½ βΎt π΄)) |
6 | topbas 22163 | . . . 4 β’ (π½ β Top β π½ β TopBases) | |
7 | 6 | adantr 482 | . . 3 β’ ((π½ β Top β§ π΄ β π) β π½ β TopBases) |
8 | restbas 22350 | . . 3 β’ (π½ β TopBases β (π½ βΎt π΄) β TopBases) | |
9 | tgcl 22160 | . . 3 β’ ((π½ βΎt π΄) β TopBases β (topGenβ(π½ βΎt π΄)) β Top) | |
10 | 7, 8, 9 | 3syl 18 | . 2 β’ ((π½ β Top β§ π΄ β π) β (topGenβ(π½ βΎt π΄)) β Top) |
11 | 5, 10 | eqeltrrd 2838 | 1 β’ ((π½ β Top β§ π΄ β π) β (π½ βΎt π΄) β Top) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 397 = wceq 1539 β wcel 2104 βcfv 6454 (class class class)co 7303 βΎt crest 17172 topGenctg 17189 Topctop 22083 TopBasesctb 22136 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-rep 5218 ax-sep 5232 ax-nul 5239 ax-pow 5297 ax-pr 5361 ax-un 7616 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-reu 3286 df-rab 3287 df-v 3439 df-sbc 3722 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-pss 3911 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-int 4887 df-iun 4933 df-br 5082 df-opab 5144 df-mpt 5165 df-tr 5199 df-id 5496 df-eprel 5502 df-po 5510 df-so 5511 df-fr 5551 df-we 5553 df-xp 5602 df-rel 5603 df-cnv 5604 df-co 5605 df-dm 5606 df-rn 5607 df-res 5608 df-ima 5609 df-ord 6280 df-on 6281 df-lim 6282 df-suc 6283 df-iota 6406 df-fun 6456 df-fn 6457 df-f 6458 df-f1 6459 df-fo 6460 df-f1o 6461 df-fv 6462 df-ov 7306 df-oprab 7307 df-mpo 7308 df-om 7741 df-1st 7859 df-2nd 7860 df-en 8761 df-fin 8764 df-fi 9210 df-rest 17174 df-topgen 17195 df-top 22084 df-bases 22137 |
This theorem is referenced by: resttopon 22353 resttopon2 22360 rest0 22361 restcld 22364 neitr 22372 restcls 22373 restntr 22374 ordtrest 22394 cmpsub 22592 fiuncmp 22596 1stcrest 22645 subislly 22673 llyrest 22677 nllyrest 22678 toplly 22682 cldllycmp 22687 kgencmp2 22738 llycmpkgen2 22742 1stckgen 22746 txkgen 22844 cnextfres1 23260 zdis 24020 cnmpopc 24132 dvbss 25106 dvreslem 25114 dvres2lem 25115 dvcnp2 25125 dvmptres 25168 ulmdvlem3 25602 psercn 25626 abelth 25641 zarmxt1 31871 ordtrestNEW 31912 cvxpconn 33245 cvmscld 33276 ptrest 35817 poimirlem29 35847 cnambfre 35866 limcresiooub 43231 limcresioolb 43232 cncfuni 43475 cncfiooicclem1 43482 fourierdlem32 43728 fourierdlem33 43729 fourierdlem48 43743 fourierdlem49 43744 fouriersw 43820 iscnrm3lem1 46284 iscnrm3rlem7 46297 |
Copyright terms: Public domain | W3C validator |