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	⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝒫 𝑌 ↾t 𝐴 ) = 𝒫 ( 𝑌 ∩ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		pwexg	⊢ ( 𝑌 ∈ 𝑉 → 𝒫 𝑌 ∈ V )
2		elrest	⊢ ( ( 𝒫 𝑌 ∈ V ∧ 𝐴 ∈ 𝑊 ) → ( 𝑥 ∈ ( 𝒫 𝑌 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝒫 𝑌 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
3	1 2	sylan	⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑥 ∈ ( 𝒫 𝑌 ↾t 𝐴 ) ↔ ∃ 𝑦 ∈ 𝒫 𝑌 𝑥 = ( 𝑦 ∩ 𝐴 ) ) )
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	⊢ 𝑥 ∈ V
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	⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝑥 ∈ ( 𝒫 𝑌 ↾t 𝐴 ) ↔ 𝑥 ∈ 𝒫 ( 𝑌 ∩ 𝐴 ) ) )
45	44	eqrdv	⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝐴 ∈ 𝑊 ) → ( 𝒫 𝑌 ↾t 𝐴 ) = 𝒫 ( 𝑌 ∩ 𝐴 ) )