![]() |
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 21209 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) | |
2 | id 22 | . . . 4 ⊢ (𝐴 ⊆ 𝑋 → 𝐴 ⊆ 𝑋) | |
3 | toponmax 21222 | . . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) | |
4 | ssexg 5125 | . . . 4 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝐴 ∈ V) | |
5 | 2, 3, 4 | syl2anr 596 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V) |
6 | resttop 21456 | . . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top) | |
7 | 1, 5, 6 | syl2an2r 681 | . 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ Top) |
8 | simpr 485 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋) | |
9 | sseqin2 4118 | . . . . . 6 ⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴) | |
10 | 8, 9 | sylib 219 | . . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) = 𝐴) |
11 | simpl 483 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐽 ∈ (TopOn‘𝑋)) | |
12 | 3 | adantr 481 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ 𝐽) |
13 | elrestr 16535 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V ∧ 𝑋 ∈ 𝐽) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) | |
14 | 11, 5, 12, 13 | syl3anc 1364 | . . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
15 | 10, 14 | eqeltrrd 2886 | . . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ (𝐽 ↾t 𝐴)) |
16 | elssuni 4780 | . . . 4 ⊢ (𝐴 ∈ (𝐽 ↾t 𝐴) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴)) | |
17 | 15, 16 | syl 17 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴)) |
18 | restval 16533 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴))) | |
19 | 5, 18 | syldan 591 | . . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴))) |
20 | inss2 4132 | . . . . . . . . 9 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴 | |
21 | vex 3443 | . . . . . . . . . . 11 ⊢ 𝑥 ∈ V | |
22 | 21 | inex1 5119 | . . . . . . . . . 10 ⊢ (𝑥 ∩ 𝐴) ∈ V |
23 | 22 | elpw 4465 | . . . . . . . . 9 ⊢ ((𝑥 ∩ 𝐴) ∈ 𝒫 𝐴 ↔ (𝑥 ∩ 𝐴) ⊆ 𝐴) |
24 | 20, 23 | mpbir 232 | . . . . . . . 8 ⊢ (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴 |
25 | 24 | a1i 11 | . . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) → (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴) |
26 | 25 | fmpttd 6749 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)):𝐽⟶𝒫 𝐴) |
27 | 26 | frnd 6396 | . . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)) ⊆ 𝒫 𝐴) |
28 | 19, 27 | eqsstrd 3932 | . . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴) |
29 | sspwuni 4927 | . . . 4 ⊢ ((𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 ↔ ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴) | |
30 | 28, 29 | sylib 219 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴) |
31 | 17, 30 | eqssd 3912 | . 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
32 | istopon 21208 | . 2 ⊢ ((𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴) ↔ ((𝐽 ↾t 𝐴) ∈ Top ∧ 𝐴 = ∪ (𝐽 ↾t 𝐴))) | |
33 | 7, 31, 32 | sylanbrc 583 | 1 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ (TopOn‘𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1525 ∈ wcel 2083 Vcvv 3440 ∩ cin 3864 ⊆ wss 3865 𝒫 cpw 4459 ∪ cuni 4751 ↦ cmpt 5047 ran crn 5451 ‘cfv 6232 (class class class)co 7023 ↾t crest 16527 Topctop 21189 TopOnctopon 21206 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1781 ax-4 1795 ax-5 1892 ax-6 1951 ax-7 1996 ax-8 2085 ax-9 2093 ax-10 2114 ax-11 2128 ax-12 2143 ax-13 2346 ax-ext 2771 ax-rep 5088 ax-sep 5101 ax-nul 5108 ax-pow 5164 ax-pr 5228 ax-un 7326 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3or 1081 df-3an 1082 df-tru 1528 df-ex 1766 df-nf 1770 df-sb 2045 df-mo 2578 df-eu 2614 df-clab 2778 df-cleq 2790 df-clel 2865 df-nfc 2937 df-ne 2987 df-ral 3112 df-rex 3113 df-reu 3114 df-rab 3116 df-v 3442 df-sbc 3712 df-csb 3818 df-dif 3868 df-un 3870 df-in 3872 df-ss 3880 df-pss 3882 df-nul 4218 df-if 4388 df-pw 4461 df-sn 4479 df-pr 4481 df-tp 4483 df-op 4485 df-uni 4752 df-int 4789 df-iun 4833 df-br 4969 df-opab 5031 df-mpt 5048 df-tr 5071 df-id 5355 df-eprel 5360 df-po 5369 df-so 5370 df-fr 5409 df-we 5411 df-xp 5456 df-rel 5457 df-cnv 5458 df-co 5459 df-dm 5460 df-rn 5461 df-res 5462 df-ima 5463 df-pred 6030 df-ord 6076 df-on 6077 df-lim 6078 df-suc 6079 df-iota 6196 df-fun 6234 df-fn 6235 df-f 6236 df-f1 6237 df-fo 6238 df-f1o 6239 df-fv 6240 df-ov 7026 df-oprab 7027 df-mpo 7028 df-om 7444 df-1st 7552 df-2nd 7553 df-wrecs 7805 df-recs 7867 df-rdg 7905 df-oadd 7964 df-er 8146 df-en 8365 df-fin 8368 df-fi 8728 df-rest 16529 df-topgen 16550 df-top 21190 df-topon 21207 df-bases 21242 |
This theorem is referenced by: restuni 21458 stoig 21459 restsn2 21467 restlp 21479 restperf 21480 perfopn 21481 cnrest 21581 cnrest2 21582 cnrest2r 21583 cnpresti 21584 cnprest 21585 cnprest2 21586 restcnrm 21658 connsuba 21716 kgentopon 21834 1stckgenlem 21849 kgen2ss 21851 kgencn 21852 xkoinjcn 21983 qtoprest 22013 flimrest 22279 fclsrest 22320 flfcntr 22339 symgtgp 22397 dvrcn 22479 sszcld 23112 divcn 23163 cncfmptc 23206 cncfmptid 23207 cncfmpt2f 23209 cdivcncf 23212 cnmpopc 23219 icchmeo 23232 htpycc 23271 pcocn 23308 pcohtpylem 23310 pcopt 23313 pcopt2 23314 pcoass 23315 pcorevlem 23317 relcmpcmet 23608 limcvallem 24156 ellimc2 24162 limcres 24171 cnplimc 24172 cnlimc 24173 limccnp 24176 limccnp2 24177 dvbss 24186 perfdvf 24188 dvreslem 24194 dvres2lem 24195 dvcnp2 24204 dvcn 24205 dvaddbr 24222 dvmulbr 24223 dvcmulf 24229 dvmptres2 24246 dvmptcmul 24248 dvmptntr 24255 dvmptfsum 24259 dvcnvlem 24260 dvcnv 24261 lhop1lem 24297 lhop2 24299 lhop 24300 dvcnvrelem2 24302 dvcnvre 24303 ftc1lem3 24322 ftc1cn 24327 taylthlem1 24648 ulmdvlem3 24677 psercn 24701 abelth 24716 logcn 24915 cxpcn 25011 cxpcn2 25012 cxpcn3 25014 resqrtcn 25015 sqrtcn 25016 loglesqrt 25024 xrlimcnp 25232 efrlim 25233 ftalem3 25338 xrge0pluscn 30796 xrge0mulc1cn 30797 lmlimxrge0 30804 pnfneige0 30807 lmxrge0 30808 esumcvg 30958 cxpcncf1 31479 cvxpconn 32099 cvxsconn 32100 cvmsf1o 32129 cvmliftlem8 32149 cvmlift2lem9a 32160 cvmlift2lem11 32170 cvmlift3lem6 32181 ivthALT 33294 poimir 34477 broucube 34478 cnambfre 34492 ftc1cnnc 34518 areacirclem2 34535 areacirclem4 34537 fsumcncf 41724 ioccncflimc 41731 cncfuni 41732 icccncfext 41733 icocncflimc 41735 cncfiooicclem1 41739 cxpcncf2 41746 dvmptconst 41762 dvmptidg 41764 dvresntr 41765 itgsubsticclem 41823 dirkercncflem2 41953 dirkercncflem4 41955 fourierdlem32 41988 fourierdlem33 41989 fourierdlem62 42017 fourierdlem93 42048 fourierdlem101 42056 |
Copyright terms: Public domain | W3C validator |