![]() |
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 22906 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) | |
2 | id 22 | . . . 4 ⊢ (𝐴 ⊆ 𝑋 → 𝐴 ⊆ 𝑋) | |
3 | toponmax 22919 | . . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) | |
4 | ssexg 5328 | . . . 4 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝐴 ∈ V) | |
5 | 2, 3, 4 | syl2anr 595 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V) |
6 | resttop 23155 | . . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top) | |
7 | 1, 5, 6 | syl2an2r 683 | . 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ Top) |
8 | simpr 483 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋) | |
9 | sseqin2 4216 | . . . . . 6 ⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴) | |
10 | 8, 9 | sylib 217 | . . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) = 𝐴) |
11 | simpl 481 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐽 ∈ (TopOn‘𝑋)) | |
12 | 3 | adantr 479 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ 𝐽) |
13 | elrestr 17443 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V ∧ 𝑋 ∈ 𝐽) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) | |
14 | 11, 5, 12, 13 | syl3anc 1368 | . . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
15 | 10, 14 | eqeltrrd 2827 | . . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ (𝐽 ↾t 𝐴)) |
16 | elssuni 4945 | . . . 4 ⊢ (𝐴 ∈ (𝐽 ↾t 𝐴) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴)) | |
17 | 15, 16 | syl 17 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴)) |
18 | restval 17441 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴))) | |
19 | 5, 18 | syldan 589 | . . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴))) |
20 | inss2 4231 | . . . . . . . . 9 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴 | |
21 | vex 3466 | . . . . . . . . . . 11 ⊢ 𝑥 ∈ V | |
22 | 21 | inex1 5322 | . . . . . . . . . 10 ⊢ (𝑥 ∩ 𝐴) ∈ V |
23 | 22 | elpw 4611 | . . . . . . . . 9 ⊢ ((𝑥 ∩ 𝐴) ∈ 𝒫 𝐴 ↔ (𝑥 ∩ 𝐴) ⊆ 𝐴) |
24 | 20, 23 | mpbir 230 | . . . . . . . 8 ⊢ (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴 |
25 | 24 | a1i 11 | . . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) → (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴) |
26 | 25 | fmpttd 7129 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)):𝐽⟶𝒫 𝐴) |
27 | 26 | frnd 6736 | . . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)) ⊆ 𝒫 𝐴) |
28 | 19, 27 | eqsstrd 4018 | . . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴) |
29 | sspwuni 5108 | . . . 4 ⊢ ((𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 ↔ ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴) | |
30 | 28, 29 | sylib 217 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴) |
31 | 17, 30 | eqssd 3997 | . 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
32 | istopon 22905 | . 2 ⊢ ((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) ↔ ((𝐽 ↾t 𝐴) ∈ Top ∧ 𝐴 = ∪ (𝐽 ↾t 𝐴))) | |
33 | 7, 31, 32 | sylanbrc 581 | 1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 ∈ wcel 2099 Vcvv 3462 ∩ cin 3946 ⊆ wss 3947 𝒫 cpw 4607 ∪ cuni 4913 ↦ cmpt 5236 ran crn 5683 ‘cfv 6554 (class class class)co 7424 ↾t crest 17435 Topctop 22886 TopOnctopon 22903 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5290 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746 |
This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-ral 3052 df-rex 3061 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-int 4955 df-iun 5003 df-br 5154 df-opab 5216 df-mpt 5237 df-tr 5271 df-id 5580 df-eprel 5586 df-po 5594 df-so 5595 df-fr 5637 df-we 5639 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-ord 6379 df-on 6380 df-lim 6381 df-suc 6382 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-ov 7427 df-oprab 7428 df-mpo 7429 df-om 7877 df-1st 8003 df-2nd 8004 df-en 8975 df-fin 8978 df-fi 9454 df-rest 17437 df-topgen 17458 df-top 22887 df-topon 22904 df-bases 22940 |
This theorem is referenced by: restuni 23157 stoig 23158 restsn2 23166 restlp 23178 restperf 23179 perfopn 23180 cnrest 23280 cnrest2 23281 cnrest2r 23282 cnpresti 23283 cnprest 23284 cnprest2 23285 restcnrm 23357 connsuba 23415 kgentopon 23533 1stckgenlem 23548 kgen2ss 23550 kgencn 23551 xkoinjcn 23682 qtoprest 23712 flimrest 23978 fclsrest 24019 flfcntr 24038 efmndtmd 24096 symgtgp 24101 dvrcn 24179 sszcld 24824 divcnOLD 24875 divcn 24877 cncfmptc 24923 cncfmptid 24924 cncfmpt2f 24926 cdivcncf 24932 cnmpopc 24940 icchmeo 24956 icchmeoOLD 24957 htpycc 24997 pcocn 25035 pcohtpylem 25037 pcopt 25040 pcopt2 25041 pcoass 25042 pcorevlem 25044 relcmpcmet 25337 mulcncf 25465 limcvallem 25891 ellimc2 25897 limcres 25906 cnplimc 25907 cnlimc 25908 limccnp 25911 limccnp2 25912 dvbss 25921 perfdvf 25923 dvreslem 25929 dvres2lem 25930 dvcnp2 25940 dvcnp2OLD 25941 dvcn 25942 dvaddbr 25959 dvmulbr 25960 dvmulbrOLD 25961 dvcmulf 25967 dvmptres2 25985 dvmptcmul 25987 dvmptntr 25994 dvmptfsum 25998 dvcnvlem 25999 dvcnv 26000 lhop1lem 26037 lhop2 26039 lhop 26040 dvcnvrelem2 26042 dvcnvre 26043 ftc1lem3 26064 ftc1cn 26069 taylthlem1 26401 ulmdvlem3 26431 psercn 26456 abelth 26471 logcn 26674 cxpcn 26772 cxpcnOLD 26773 cxpcn2 26774 cxpcn3 26776 resqrtcn 26777 sqrtcn 26778 loglesqrt 26789 xrlimcnp 26996 efrlim 26997 efrlimOLD 26998 ftalem3 27103 xrge0pluscn 33755 xrge0mulc1cn 33756 lmlimxrge0 33763 pnfneige0 33766 lmxrge0 33767 esumcvg 33919 cxpcncf1 34441 cvxpconn 35070 cvxsconn 35071 cvmsf1o 35100 cvmliftlem8 35120 cvmlift2lem9a 35131 cvmlift2lem11 35141 cvmlift3lem6 35152 ivthALT 36047 poimir 37354 broucube 37355 cnambfre 37369 ftc1cnnc 37393 areacirclem2 37410 areacirclem4 37412 fsumcncf 45499 ioccncflimc 45506 cncfuni 45507 icccncfext 45508 icocncflimc 45510 cncfiooicclem1 45514 cxpcncf2 45520 dvmptconst 45536 dvmptidg 45538 dvresntr 45539 itgsubsticclem 45596 dirkercncflem2 45725 dirkercncflem4 45727 fourierdlem32 45760 fourierdlem33 45761 fourierdlem62 45789 fourierdlem93 45820 fourierdlem101 45828 |
Copyright terms: Public domain | W3C validator |