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	$$⊢\left(Y\in V\wedge A\in W\right)\to 𝒫Y{\upharpoonright }_{𝑡}A=𝒫\left(Y\cap A\right)$$

Proof

Step	Hyp	Ref	Expression
1		pwexg	$$⊢Y\in V\to 𝒫Y\in \mathrm{V}$$
2		elrest	$$⊢\left(𝒫Y\in \mathrm{V}\wedge A\in W\right)\to \left(x\in \left(𝒫Y{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists y\in 𝒫Yx=y\cap A\right)$$
3	1 2	sylan	$$⊢\left(Y\in V\wedge A\in W\right)\to \left(x\in \left(𝒫Y{\upharpoonright }_{𝑡}A\right)\leftrightarrow \exists y\in 𝒫Yx=y\cap A\right)$$
4		velpw	$$⊢y\in 𝒫Y\leftrightarrow y\subseteq Y$$
5	4	anbi1i	$$⊢\left(y\in 𝒫Y\wedge x=y\cap A\right)\leftrightarrow \left(y\subseteq Y\wedge x=y\cap A\right)$$
6	5	exbii	$$⊢\exists y\left(y\in 𝒫Y\wedge x=y\cap A\right)\leftrightarrow \exists y\left(y\subseteq Y\wedge x=y\cap A\right)$$
7		sstr2	$$⊢x\subseteq y\to \left(y\subseteq Y\to x\subseteq Y\right)$$
8	7	com12	$$⊢y\subseteq Y\to \left(x\subseteq y\to x\subseteq Y\right)$$
9		inss1	$$⊢y\cap A\subseteq y$$
10		sseq1	$$⊢x=y\cap A\to \left(x\subseteq y\leftrightarrow y\cap A\subseteq y\right)$$
11	9 10	mpbiri	$$⊢x=y\cap A\to x\subseteq y$$
12	8 11	impel	$$⊢\left(y\subseteq Y\wedge x=y\cap A\right)\to x\subseteq Y$$
13		inss2	$$⊢y\cap A\subseteq A$$
14		sseq1	$$⊢x=y\cap A\to \left(x\subseteq A\leftrightarrow y\cap A\subseteq A\right)$$
15	13 14	mpbiri	$$⊢x=y\cap A\to x\subseteq A$$
16	15	adantl	$$⊢\left(y\subseteq Y\wedge x=y\cap A\right)\to x\subseteq A$$
17	12 16	ssind	$$⊢\left(y\subseteq Y\wedge x=y\cap A\right)\to x\subseteq Y\cap A$$
18	17	exlimiv	$$⊢\exists y\left(y\subseteq Y\wedge x=y\cap A\right)\to x\subseteq Y\cap A$$
19		inss1	$$⊢Y\cap A\subseteq Y$$
20		sstr2	$$⊢x\subseteq Y\cap A\to \left(Y\cap A\subseteq Y\to x\subseteq Y\right)$$
21	19 20	mpi	$$⊢x\subseteq Y\cap A\to x\subseteq Y$$
22		inss2	$$⊢Y\cap A\subseteq A$$
23		sstr2	$$⊢x\subseteq Y\cap A\to \left(Y\cap A\subseteq A\to x\subseteq A\right)$$
24	22 23	mpi	$$⊢x\subseteq Y\cap A\to x\subseteq A$$
25		ssidd	$$⊢x\subseteq A\to x\subseteq x$$
26		id	$$⊢x\subseteq A\to x\subseteq A$$
27	25 26	ssind	$$⊢x\subseteq A\to x\subseteq x\cap A$$
28		inss1	$$⊢x\cap A\subseteq x$$
29	28	a1i	$$⊢x\subseteq A\to x\cap A\subseteq x$$
30	27 29	eqssd	$$⊢x\subseteq A\to x=x\cap A$$
31		vex	$$⊢x\in \mathrm{V}$$
32		sseq1	$$⊢y=x\to \left(y\subseteq Y\leftrightarrow x\subseteq Y\right)$$
33		ineq1	$$⊢y=x\to y\cap A=x\cap A$$
34	33	eqeq2d	$$⊢y=x\to \left(x=y\cap A\leftrightarrow x=x\cap A\right)$$
35	32 34	anbi12d	$$⊢y=x\to \left(\left(y\subseteq Y\wedge x=y\cap A\right)\leftrightarrow \left(x\subseteq Y\wedge x=x\cap A\right)\right)$$
36	31 35	spcev	$$⊢\left(x\subseteq Y\wedge x=x\cap A\right)\to \exists y\left(y\subseteq Y\wedge x=y\cap A\right)$$
37	30 36	sylan2	$$⊢\left(x\subseteq Y\wedge x\subseteq A\right)\to \exists y\left(y\subseteq Y\wedge x=y\cap A\right)$$
38	21 24 37	syl2anc	$$⊢x\subseteq Y\cap A\to \exists y\left(y\subseteq Y\wedge x=y\cap A\right)$$
39	18 38	impbii	$$⊢\exists y\left(y\subseteq Y\wedge x=y\cap A\right)\leftrightarrow x\subseteq Y\cap A$$
40	6 39	bitri	$$⊢\exists y\left(y\in 𝒫Y\wedge x=y\cap A\right)\leftrightarrow x\subseteq Y\cap A$$
41		df-rex	$$⊢\exists y\in 𝒫Yx=y\cap A\leftrightarrow \exists y\left(y\in 𝒫Y\wedge x=y\cap A\right)$$
42		velpw	$$⊢x\in 𝒫\left(Y\cap A\right)\leftrightarrow x\subseteq Y\cap A$$
43	40 41 42	3bitr4i	$$⊢\exists y\in 𝒫Yx=y\cap A\leftrightarrow x\in 𝒫\left(Y\cap A\right)$$
44	3 43	bitrdi	$$⊢\left(Y\in V\wedge A\in W\right)\to \left(x\in \left(𝒫Y{\upharpoonright }_{𝑡}A\right)\leftrightarrow x\in 𝒫\left(Y\cap A\right)\right)$$
45	44	eqrdv	$$⊢\left(Y\in V\wedge A\in W\right)\to 𝒫Y{\upharpoonright }_{𝑡}A=𝒫\left(Y\cap A\right)$$