![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > resttopon | Structured version Visualization version GIF version |
Description: A subspace topology is a topology on the base set. (Contributed by Mario Carneiro, 13-Aug-2015.) |
Ref | Expression |
---|---|
resttopon | β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π΄) β (TopOnβπ΄)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | topontop 22636 | . . 3 β’ (π½ β (TopOnβπ) β π½ β Top) | |
2 | id 22 | . . . 4 β’ (π΄ β π β π΄ β π) | |
3 | toponmax 22649 | . . . 4 β’ (π½ β (TopOnβπ) β π β π½) | |
4 | ssexg 5323 | . . . 4 β’ ((π΄ β π β§ π β π½) β π΄ β V) | |
5 | 2, 3, 4 | syl2anr 596 | . . 3 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β V) |
6 | resttop 22885 | . . 3 β’ ((π½ β Top β§ π΄ β V) β (π½ βΎt π΄) β Top) | |
7 | 1, 5, 6 | syl2an2r 682 | . 2 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π΄) β Top) |
8 | simpr 484 | . . . . . 6 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β π) | |
9 | sseqin2 4215 | . . . . . 6 β’ (π΄ β π β (π β© π΄) = π΄) | |
10 | 8, 9 | sylib 217 | . . . . 5 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π β© π΄) = π΄) |
11 | simpl 482 | . . . . . 6 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π½ β (TopOnβπ)) | |
12 | 3 | adantr 480 | . . . . . 6 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π β π½) |
13 | elrestr 17379 | . . . . . 6 β’ ((π½ β (TopOnβπ) β§ π΄ β V β§ π β π½) β (π β© π΄) β (π½ βΎt π΄)) | |
14 | 11, 5, 12, 13 | syl3anc 1370 | . . . . 5 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π β© π΄) β (π½ βΎt π΄)) |
15 | 10, 14 | eqeltrrd 2833 | . . . 4 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β (π½ βΎt π΄)) |
16 | elssuni 4941 | . . . 4 β’ (π΄ β (π½ βΎt π΄) β π΄ β βͺ (π½ βΎt π΄)) | |
17 | 15, 16 | syl 17 | . . 3 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ β βͺ (π½ βΎt π΄)) |
18 | restval 17377 | . . . . . 6 β’ ((π½ β (TopOnβπ) β§ π΄ β V) β (π½ βΎt π΄) = ran (π₯ β π½ β¦ (π₯ β© π΄))) | |
19 | 5, 18 | syldan 590 | . . . . 5 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π΄) = ran (π₯ β π½ β¦ (π₯ β© π΄))) |
20 | inss2 4229 | . . . . . . . . 9 β’ (π₯ β© π΄) β π΄ | |
21 | vex 3477 | . . . . . . . . . . 11 β’ π₯ β V | |
22 | 21 | inex1 5317 | . . . . . . . . . 10 β’ (π₯ β© π΄) β V |
23 | 22 | elpw 4606 | . . . . . . . . 9 β’ ((π₯ β© π΄) β π« π΄ β (π₯ β© π΄) β π΄) |
24 | 20, 23 | mpbir 230 | . . . . . . . 8 β’ (π₯ β© π΄) β π« π΄ |
25 | 24 | a1i 11 | . . . . . . 7 β’ (((π½ β (TopOnβπ) β§ π΄ β π) β§ π₯ β π½) β (π₯ β© π΄) β π« π΄) |
26 | 25 | fmpttd 7116 | . . . . . 6 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π₯ β π½ β¦ (π₯ β© π΄)):π½βΆπ« π΄) |
27 | 26 | frnd 6725 | . . . . 5 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β ran (π₯ β π½ β¦ (π₯ β© π΄)) β π« π΄) |
28 | 19, 27 | eqsstrd 4020 | . . . 4 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π΄) β π« π΄) |
29 | sspwuni 5103 | . . . 4 β’ ((π½ βΎt π΄) β π« π΄ β βͺ (π½ βΎt π΄) β π΄) | |
30 | 28, 29 | sylib 217 | . . 3 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β βͺ (π½ βΎt π΄) β π΄) |
31 | 17, 30 | eqssd 3999 | . 2 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β π΄ = βͺ (π½ βΎt π΄)) |
32 | istopon 22635 | . 2 β’ ((π½ βΎt π΄) β (TopOnβπ΄) β ((π½ βΎt π΄) β Top β§ π΄ = βͺ (π½ βΎt π΄))) | |
33 | 7, 31, 32 | sylanbrc 582 | 1 β’ ((π½ β (TopOnβπ) β§ π΄ β π) β (π½ βΎt π΄) β (TopOnβπ΄)) |
Colors of variables: wff setvar class |
Syntax hints: β wi 4 β§ wa 395 = wceq 1540 β wcel 2105 Vcvv 3473 β© cin 3947 β wss 3948 π« cpw 4602 βͺ cuni 4908 β¦ cmpt 5231 ran crn 5677 βcfv 6543 (class class class)co 7412 βΎt crest 17371 Topctop 22616 TopOnctopon 22633 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2702 ax-rep 5285 ax-sep 5299 ax-nul 5306 ax-pow 5363 ax-pr 5427 ax-un 7729 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2533 df-eu 2562 df-clab 2709 df-cleq 2723 df-clel 2809 df-nfc 2884 df-ne 2940 df-ral 3061 df-rex 3070 df-reu 3376 df-rab 3432 df-v 3475 df-sbc 3778 df-csb 3894 df-dif 3951 df-un 3953 df-in 3955 df-ss 3965 df-pss 3967 df-nul 4323 df-if 4529 df-pw 4604 df-sn 4629 df-pr 4631 df-op 4635 df-uni 4909 df-int 4951 df-iun 4999 df-br 5149 df-opab 5211 df-mpt 5232 df-tr 5266 df-id 5574 df-eprel 5580 df-po 5588 df-so 5589 df-fr 5631 df-we 5633 df-xp 5682 df-rel 5683 df-cnv 5684 df-co 5685 df-dm 5686 df-rn 5687 df-res 5688 df-ima 5689 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6495 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-ov 7415 df-oprab 7416 df-mpo 7417 df-om 7860 df-1st 7979 df-2nd 7980 df-en 8944 df-fin 8947 df-fi 9410 df-rest 17373 df-topgen 17394 df-top 22617 df-topon 22634 df-bases 22670 |
This theorem is referenced by: restuni 22887 stoig 22888 restsn2 22896 restlp 22908 restperf 22909 perfopn 22910 cnrest 23010 cnrest2 23011 cnrest2r 23012 cnpresti 23013 cnprest 23014 cnprest2 23015 restcnrm 23087 connsuba 23145 kgentopon 23263 1stckgenlem 23278 kgen2ss 23280 kgencn 23281 xkoinjcn 23412 qtoprest 23442 flimrest 23708 fclsrest 23749 flfcntr 23768 efmndtmd 23826 symgtgp 23831 dvrcn 23909 sszcld 24554 divcnOLD 24605 divcn 24607 cncfmptc 24653 cncfmptid 24654 cncfmpt2f 24656 cdivcncf 24662 cnmpopc 24670 icchmeo 24686 icchmeoOLD 24687 htpycc 24727 pcocn 24765 pcohtpylem 24767 pcopt 24770 pcopt2 24771 pcoass 24772 pcorevlem 24774 relcmpcmet 25067 mulcncf 25195 limcvallem 25621 ellimc2 25627 limcres 25636 cnplimc 25637 cnlimc 25638 limccnp 25641 limccnp2 25642 dvbss 25651 perfdvf 25653 dvreslem 25659 dvres2lem 25660 dvcnp2 25670 dvcnp2OLD 25671 dvcn 25672 dvaddbr 25689 dvmulbr 25690 dvmulbrOLD 25691 dvcmulf 25697 dvmptres2 25715 dvmptcmul 25717 dvmptntr 25724 dvmptfsum 25728 dvcnvlem 25729 dvcnv 25730 lhop1lem 25766 lhop2 25768 lhop 25769 dvcnvrelem2 25771 dvcnvre 25772 ftc1lem3 25791 ftc1cn 25796 taylthlem1 26122 ulmdvlem3 26151 psercn 26175 abelth 26190 logcn 26392 cxpcn 26490 cxpcn2 26491 cxpcn3 26493 resqrtcn 26494 sqrtcn 26495 loglesqrt 26503 xrlimcnp 26710 efrlim 26711 ftalem3 26816 xrge0pluscn 33219 xrge0mulc1cn 33220 lmlimxrge0 33227 pnfneige0 33230 lmxrge0 33231 esumcvg 33383 cxpcncf1 33906 cvxpconn 34532 cvxsconn 34533 cvmsf1o 34562 cvmliftlem8 34582 cvmlift2lem9a 34593 cvmlift2lem11 34603 cvmlift3lem6 34614 gg-cxpcn 35471 ivthALT 35524 poimir 36825 broucube 36826 cnambfre 36840 ftc1cnnc 36864 areacirclem2 36881 areacirclem4 36883 fsumcncf 44893 ioccncflimc 44900 cncfuni 44901 icccncfext 44902 icocncflimc 44904 cncfiooicclem1 44908 cxpcncf2 44914 dvmptconst 44930 dvmptidg 44932 dvresntr 44933 itgsubsticclem 44990 dirkercncflem2 45119 dirkercncflem4 45121 fourierdlem32 45154 fourierdlem33 45155 fourierdlem62 45183 fourierdlem93 45214 fourierdlem101 45222 |
Copyright terms: Public domain | W3C validator |