| 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 22919 | . . 3 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) | |
| 2 | id 22 | . . . 4 ⊢ (𝐴 ⊆ 𝑋 → 𝐴 ⊆ 𝑋) | |
| 3 | toponmax 22932 | . . . 4 ⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) | |
| 4 | ssexg 5323 | . . . 4 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑋 ∈ 𝐽) → 𝐴 ∈ V) | |
| 5 | 2, 3, 4 | syl2anr 597 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ V) |
| 6 | resttop 23168 | . . 3 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) ∈ Top) | |
| 7 | 1, 5, 6 | syl2an2r 685 | . 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ∈ Top) |
| 8 | simpr 484 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ 𝑋) | |
| 9 | sseqin2 4223 | . . . . . 6 ⊢ (𝐴 ⊆ 𝑋 ↔ (𝑋 ∩ 𝐴) = 𝐴) | |
| 10 | 8, 9 | sylib 218 | . . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) = 𝐴) |
| 11 | simpl 482 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐽 ∈ (TopOn‘𝑋)) | |
| 12 | 3 | adantr 480 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝑋 ∈ 𝐽) |
| 13 | elrestr 17473 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V ∧ 𝑋 ∈ 𝐽) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) | |
| 14 | 11, 5, 12, 13 | syl3anc 1373 | . . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑋 ∩ 𝐴) ∈ (𝐽 ↾t 𝐴)) |
| 15 | 10, 14 | eqeltrrd 2842 | . . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ∈ (𝐽 ↾t 𝐴)) |
| 16 | elssuni 4937 | . . . 4 ⊢ (𝐴 ∈ (𝐽 ↾t 𝐴) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴)) | |
| 17 | 15, 16 | syl 17 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 ⊆ ∪ (𝐽 ↾t 𝐴)) |
| 18 | restval 17471 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ V) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴))) | |
| 19 | 5, 18 | syldan 591 | . . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) = ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴))) |
| 20 | inss2 4238 | . . . . . . . . 9 ⊢ (𝑥 ∩ 𝐴) ⊆ 𝐴 | |
| 21 | vex 3484 | . . . . . . . . . . 11 ⊢ 𝑥 ∈ V | |
| 22 | 21 | inex1 5317 | . . . . . . . . . 10 ⊢ (𝑥 ∩ 𝐴) ∈ V |
| 23 | 22 | elpw 4604 | . . . . . . . . 9 ⊢ ((𝑥 ∩ 𝐴) ∈ 𝒫 𝐴 ↔ (𝑥 ∩ 𝐴) ⊆ 𝐴) |
| 24 | 20, 23 | mpbir 231 | . . . . . . . 8 ⊢ (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴 |
| 25 | 24 | a1i 11 | . . . . . . 7 ⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) ∧ 𝑥 ∈ 𝐽) → (𝑥 ∩ 𝐴) ∈ 𝒫 𝐴) |
| 26 | 25 | fmpttd 7135 | . . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)):𝐽⟶𝒫 𝐴) |
| 27 | 26 | frnd 6744 | . . . . 5 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ran (𝑥 ∈ 𝐽 ↦ (𝑥 ∩ 𝐴)) ⊆ 𝒫 𝐴) |
| 28 | 19, 27 | eqsstrd 4018 | . . . 4 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → (𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴) |
| 29 | sspwuni 5100 | . . . 4 ⊢ ((𝐽 ↾t 𝐴) ⊆ 𝒫 𝐴 ↔ ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴) | |
| 30 | 28, 29 | sylib 218 | . . 3 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → ∪ (𝐽 ↾t 𝐴) ⊆ 𝐴) |
| 31 | 17, 30 | eqssd 4001 | . 2 ⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ⊆ 𝑋) → 𝐴 = ∪ (𝐽 ↾t 𝐴)) |
| 32 | istopon 22918 | . 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 395 = wceq 1540 ∈ wcel 2108 Vcvv 3480 ∩ cin 3950 ⊆ wss 3951 𝒫 cpw 4600 ∪ cuni 4907 ↦ cmpt 5225 ran crn 5686 ‘cfv 6561 (class class class)co 7431 ↾t crest 17465 Topctop 22899 TopOnctopon 22916 |
| 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 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-ov 7434 df-oprab 7435 df-mpo 7436 df-om 7888 df-1st 8014 df-2nd 8015 df-en 8986 df-fin 8989 df-fi 9451 df-rest 17467 df-topgen 17488 df-top 22900 df-topon 22917 df-bases 22953 |
| This theorem is referenced by: restuni 23170 stoig 23171 restsn2 23179 restlp 23191 restperf 23192 perfopn 23193 cnrest 23293 cnrest2 23294 cnrest2r 23295 cnpresti 23296 cnprest 23297 cnprest2 23298 restcnrm 23370 connsuba 23428 kgentopon 23546 1stckgenlem 23561 kgen2ss 23563 kgencn 23564 xkoinjcn 23695 qtoprest 23725 flimrest 23991 fclsrest 24032 flfcntr 24051 efmndtmd 24109 symgtgp 24114 dvrcn 24192 sszcld 24839 divcnOLD 24890 divcn 24892 cncfmptc 24938 cncfmptid 24939 cncfmpt2f 24941 cdivcncf 24947 cnmpopc 24955 icchmeo 24971 icchmeoOLD 24972 htpycc 25012 pcocn 25050 pcohtpylem 25052 pcopt 25055 pcopt2 25056 pcoass 25057 pcorevlem 25059 relcmpcmet 25352 mulcncf 25480 limcvallem 25906 ellimc2 25912 limcres 25921 cnplimc 25922 cnlimc 25923 limccnp 25926 limccnp2 25927 dvbss 25936 perfdvf 25938 dvreslem 25944 dvres2lem 25945 dvcnp2 25955 dvcnp2OLD 25956 dvcn 25957 dvaddbr 25974 dvmulbr 25975 dvmulbrOLD 25976 dvcmulf 25982 dvmptres2 26000 dvmptcmul 26002 dvmptntr 26009 dvmptfsum 26013 dvcnvlem 26014 dvcnv 26015 lhop1lem 26052 lhop2 26054 lhop 26055 dvcnvrelem2 26057 dvcnvre 26058 ftc1lem3 26079 ftc1cn 26084 taylthlem1 26415 ulmdvlem3 26445 psercn 26470 abelth 26485 logcn 26689 cxpcn 26787 cxpcnOLD 26788 cxpcn2 26789 cxpcn3 26791 resqrtcn 26792 sqrtcn 26793 loglesqrt 26804 xrlimcnp 27011 efrlim 27012 efrlimOLD 27013 ftalem3 27118 xrge0pluscn 33939 xrge0mulc1cn 33940 lmlimxrge0 33947 pnfneige0 33950 lmxrge0 33951 esumcvg 34087 cxpcncf1 34610 cvxpconn 35247 cvxsconn 35248 cvmsf1o 35277 cvmliftlem8 35297 cvmlift2lem9a 35308 cvmlift2lem11 35318 cvmlift3lem6 35329 ivthALT 36336 poimir 37660 broucube 37661 cnambfre 37675 ftc1cnnc 37699 areacirclem2 37716 areacirclem4 37718 fsumcncf 45893 ioccncflimc 45900 cncfuni 45901 icccncfext 45902 icocncflimc 45904 cncfiooicclem1 45908 cxpcncf2 45914 dvmptconst 45930 dvmptidg 45932 dvresntr 45933 itgsubsticclem 45990 dirkercncflem2 46119 dirkercncflem4 46121 fourierdlem32 46154 fourierdlem33 46155 fourierdlem62 46183 fourierdlem93 46214 fourierdlem101 46222 |
| Copyright terms: Public domain | W3C validator |