Metamath Proof Explorer


Theorem bj-restpw

Description: The elementwise intersection on a powerset is the powerset of the intersection. This allows to prove for instance that the topology induced on a subset by the discrete topology is the discrete topology on that subset. See also restdis (which uses distop and restopn2 ). (Contributed by BJ, 27-Apr-2021)

Ref Expression
Assertion bj-restpw YVAW𝒫Y𝑡A=𝒫YA

Proof

Step Hyp Ref Expression
1 pwexg YV𝒫YV
2 elrest 𝒫YVAWx𝒫Y𝑡Ay𝒫Yx=yA
3 1 2 sylan YVAWx𝒫Y𝑡Ay𝒫Yx=yA
4 velpw y𝒫YyY
5 4 anbi1i y𝒫Yx=yAyYx=yA
6 5 exbii yy𝒫Yx=yAyyYx=yA
7 sstr2 xyyYxY
8 7 com12 yYxyxY
9 inss1 yAy
10 sseq1 x=yAxyyAy
11 9 10 mpbiri x=yAxy
12 8 11 impel yYx=yAxY
13 inss2 yAA
14 sseq1 x=yAxAyAA
15 13 14 mpbiri x=yAxA
16 15 adantl yYx=yAxA
17 12 16 ssind yYx=yAxYA
18 17 exlimiv yyYx=yAxYA
19 inss1 YAY
20 sstr2 xYAYAYxY
21 19 20 mpi xYAxY
22 inss2 YAA
23 sstr2 xYAYAAxA
24 22 23 mpi xYAxA
25 ssidd xAxx
26 id xAxA
27 25 26 ssind xAxxA
28 inss1 xAx
29 28 a1i xAxAx
30 27 29 eqssd xAx=xA
31 vex xV
32 sseq1 y=xyYxY
33 ineq1 y=xyA=xA
34 33 eqeq2d y=xx=yAx=xA
35 32 34 anbi12d y=xyYx=yAxYx=xA
36 31 35 spcev xYx=xAyyYx=yA
37 30 36 sylan2 xYxAyyYx=yA
38 21 24 37 syl2anc xYAyyYx=yA
39 18 38 impbii yyYx=yAxYA
40 6 39 bitri yy𝒫Yx=yAxYA
41 df-rex y𝒫Yx=yAyy𝒫Yx=yA
42 velpw x𝒫YAxYA
43 40 41 42 3bitr4i y𝒫Yx=yAx𝒫YA
44 3 43 bitrdi YVAWx𝒫Y𝑡Ax𝒫YA
45 44 eqrdv YVAW𝒫Y𝑡A=𝒫YA