![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > restid | Structured version Visualization version GIF version |
Description: The subspace topology of the base set is the original topology. (Contributed by Jeff Hankins, 9-Jul-2009.) (Revised by Mario Carneiro, 13-Aug-2015.) |
Ref | Expression |
---|---|
restid.1 | ⊢ 𝑋 = ∪ 𝐽 |
Ref | Expression |
---|---|
restid | ⊢ (𝐽 ∈ 𝑉 → (𝐽 ↾t 𝑋) = 𝐽) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | restid.1 | . . 3 ⊢ 𝑋 = ∪ 𝐽 | |
2 | uniexg 7112 | . . 3 ⊢ (𝐽 ∈ 𝑉 → ∪ 𝐽 ∈ V) | |
3 | 1, 2 | syl5eqel 2835 | . 2 ⊢ (𝐽 ∈ 𝑉 → 𝑋 ∈ V) |
4 | 1 | eqimss2i 3793 | . . 3 ⊢ ∪ 𝐽 ⊆ 𝑋 |
5 | sspwuni 4755 | . . 3 ⊢ (𝐽 ⊆ 𝒫 𝑋 ↔ ∪ 𝐽 ⊆ 𝑋) | |
6 | 4, 5 | mpbir 221 | . 2 ⊢ 𝐽 ⊆ 𝒫 𝑋 |
7 | restid2 16285 | . 2 ⊢ ((𝑋 ∈ V ∧ 𝐽 ⊆ 𝒫 𝑋) → (𝐽 ↾t 𝑋) = 𝐽) | |
8 | 3, 6, 7 | sylancl 697 | 1 ⊢ (𝐽 ∈ 𝑉 → (𝐽 ↾t 𝑋) = 𝐽) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1624 ∈ wcel 2131 Vcvv 3332 ⊆ wss 3707 𝒫 cpw 4294 ∪ cuni 4580 (class class class)co 6805 ↾t crest 16275 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1863 ax-4 1878 ax-5 1980 ax-6 2046 ax-7 2082 ax-8 2133 ax-9 2140 ax-10 2160 ax-11 2175 ax-12 2188 ax-13 2383 ax-ext 2732 ax-rep 4915 ax-sep 4925 ax-nul 4933 ax-pow 4984 ax-pr 5047 ax-un 7106 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1627 df-ex 1846 df-nf 1851 df-sb 2039 df-eu 2603 df-mo 2604 df-clab 2739 df-cleq 2745 df-clel 2748 df-nfc 2883 df-ne 2925 df-ral 3047 df-rex 3048 df-reu 3049 df-rab 3051 df-v 3334 df-sbc 3569 df-csb 3667 df-dif 3710 df-un 3712 df-in 3714 df-ss 3721 df-nul 4051 df-if 4223 df-pw 4296 df-sn 4314 df-pr 4316 df-op 4320 df-uni 4581 df-iun 4666 df-br 4797 df-opab 4857 df-mpt 4874 df-id 5166 df-xp 5264 df-rel 5265 df-cnv 5266 df-co 5267 df-dm 5268 df-rn 5269 df-res 5270 df-ima 5271 df-iota 6004 df-fun 6043 df-fn 6044 df-f 6045 df-f1 6046 df-fo 6047 df-f1o 6048 df-fv 6049 df-ov 6808 df-oprab 6809 df-mpt2 6810 df-rest 16277 |
This theorem is referenced by: restin 21164 cnrmnrm 21359 cmpkgen 21548 xkopt 21652 xkoinjcn 21684 ussid 22257 tuslem 22264 cnperf 22816 retopconn 22825 cncfcn1 22906 cncfmpt2f 22910 cdivcncf 22913 abscncfALT 22916 cnmpt2pc 22920 cnrehmeo 22945 cnlimc 23843 recnperf 23860 dvidlem 23870 dvcnp2 23874 dvcn 23875 dvnres 23885 dvaddbr 23892 dvmulbr 23893 dvcobr 23900 dvcjbr 23903 dvrec 23909 dvexp3 23932 dveflem 23933 dvlipcn 23948 lhop1lem 23967 ftc1cn 23997 dvply1 24230 dvtaylp 24315 taylthlem2 24319 psercn 24371 pserdvlem2 24373 pserdv 24374 abelth 24386 logcn 24584 dvloglem 24585 dvlog 24588 dvlog2 24590 efopnlem2 24594 logtayl 24597 cxpcn 24677 cxpcn2 24678 cxpcn3 24680 resqrtcn 24681 sqrtcn 24682 dvatan 24853 ftalem3 24992 cxpcncf1 30974 retopsconn 31530 ivthALT 32628 knoppcnlem10 32790 knoppcnlem11 32791 dvtan 33765 ftc1cnnc 33789 dvasin 33801 dvacos 33802 binomcxplemdvbinom 39046 binomcxplemnotnn0 39049 fsumcncf 40586 ioccncflimc 40593 cncfuni 40594 icocncflimc 40597 cncfiooicclem1 40601 cxpcncf2 40608 itgsubsticclem 40686 dirkercncflem2 40816 dirkercncflem4 40818 fourierdlem32 40851 fourierdlem33 40852 fourierdlem62 40880 fourierdlem93 40911 fourierdlem101 40919 |
Copyright terms: Public domain | W3C validator |