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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pwexg | |
|
2 | elrest | |
|
3 | 1 2 | sylan | |
4 | velpw | |
|
5 | 4 | anbi1i | |
6 | 5 | exbii | |
7 | sstr2 | |
|
8 | 7 | com12 | |
9 | inss1 | |
|
10 | sseq1 | |
|
11 | 9 10 | mpbiri | |
12 | 8 11 | impel | |
13 | inss2 | |
|
14 | sseq1 | |
|
15 | 13 14 | mpbiri | |
16 | 15 | adantl | |
17 | 12 16 | ssind | |
18 | 17 | exlimiv | |
19 | inss1 | |
|
20 | sstr2 | |
|
21 | 19 20 | mpi | |
22 | inss2 | |
|
23 | sstr2 | |
|
24 | 22 23 | mpi | |
25 | ssidd | |
|
26 | id | |
|
27 | 25 26 | ssind | |
28 | inss1 | |
|
29 | 28 | a1i | |
30 | 27 29 | eqssd | |
31 | vex | |
|
32 | sseq1 | |
|
33 | ineq1 | |
|
34 | 33 | eqeq2d | |
35 | 32 34 | anbi12d | |
36 | 31 35 | spcev | |
37 | 30 36 | sylan2 | |
38 | 21 24 37 | syl2anc | |
39 | 18 38 | impbii | |
40 | 6 39 | bitri | |
41 | df-rex | |
|
42 | velpw | |
|
43 | 40 41 42 | 3bitr4i | |
44 | 3 43 | bitrdi | |
45 | 44 | eqrdv | |