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	|- ( ( Y e. V /\ A e. W ) -> ( ~P Y |`t A ) = ~P ( Y i^i A ) )

Proof

Step	Hyp	Ref	Expression
1		pwexg	|- ( Y e. V -> ~P Y e. _V )
2		elrest	|- ( ( ~P Y e. _V /\ A e. W ) -> ( x e. ( ~P Y |`t A ) <-> E. y e. ~P Y x = ( y i^i A ) ) )
3	1 2	sylan	|- ( ( Y e. V /\ A e. W ) -> ( x e. ( ~P Y |`t A ) <-> E. y e. ~P Y x = ( y i^i A ) ) )
4		velpw	|- ( y e. ~P Y <-> y C_ Y )
5	4	anbi1i	|- ( ( y e. ~P Y /\ x = ( y i^i A ) ) <-> ( y C_ Y /\ x = ( y i^i A ) ) )
6	5	exbii	|- ( E. y ( y e. ~P Y /\ x = ( y i^i A ) ) <-> E. y ( y C_ Y /\ x = ( y i^i A ) ) )
7		sstr2	|- ( x C_ y -> ( y C_ Y -> x C_ Y ) )
8	7	com12	|- ( y C_ Y -> ( x C_ y -> x C_ Y ) )
9		inss1	|- ( y i^i A ) C_ y
10		sseq1	|- ( x = ( y i^i A ) -> ( x C_ y <-> ( y i^i A ) C_ y ) )
11	9 10	mpbiri	|- ( x = ( y i^i A ) -> x C_ y )
12	8 11	impel	|- ( ( y C_ Y /\ x = ( y i^i A ) ) -> x C_ Y )
13		inss2	|- ( y i^i A ) C_ A
14		sseq1	|- ( x = ( y i^i A ) -> ( x C_ A <-> ( y i^i A ) C_ A ) )
15	13 14	mpbiri	|- ( x = ( y i^i A ) -> x C_ A )
16	15	adantl	|- ( ( y C_ Y /\ x = ( y i^i A ) ) -> x C_ A )
17	12 16	ssind	|- ( ( y C_ Y /\ x = ( y i^i A ) ) -> x C_ ( Y i^i A ) )
18	17	exlimiv	|- ( E. y ( y C_ Y /\ x = ( y i^i A ) ) -> x C_ ( Y i^i A ) )
19		inss1	|- ( Y i^i A ) C_ Y
20		sstr2	|- ( x C_ ( Y i^i A ) -> ( ( Y i^i A ) C_ Y -> x C_ Y ) )
21	19 20	mpi	|- ( x C_ ( Y i^i A ) -> x C_ Y )
22		inss2	|- ( Y i^i A ) C_ A
23		sstr2	|- ( x C_ ( Y i^i A ) -> ( ( Y i^i A ) C_ A -> x C_ A ) )
24	22 23	mpi	|- ( x C_ ( Y i^i A ) -> x C_ A )
25		ssidd	|- ( x C_ A -> x C_ x )
26		id	|- ( x C_ A -> x C_ A )
27	25 26	ssind	|- ( x C_ A -> x C_ ( x i^i A ) )
28		inss1	|- ( x i^i A ) C_ x
29	28	a1i	|- ( x C_ A -> ( x i^i A ) C_ x )
30	27 29	eqssd	|- ( x C_ A -> x = ( x i^i A ) )
31		vex	|- x e. _V
32		sseq1	|- ( y = x -> ( y C_ Y <-> x C_ Y ) )
33		ineq1	|- ( y = x -> ( y i^i A ) = ( x i^i A ) )
34	33	eqeq2d	|- ( y = x -> ( x = ( y i^i A ) <-> x = ( x i^i A ) ) )
35	32 34	anbi12d	|- ( y = x -> ( ( y C_ Y /\ x = ( y i^i A ) ) <-> ( x C_ Y /\ x = ( x i^i A ) ) ) )
36	31 35	spcev	|- ( ( x C_ Y /\ x = ( x i^i A ) ) -> E. y ( y C_ Y /\ x = ( y i^i A ) ) )
37	30 36	sylan2	|- ( ( x C_ Y /\ x C_ A ) -> E. y ( y C_ Y /\ x = ( y i^i A ) ) )
38	21 24 37	syl2anc	|- ( x C_ ( Y i^i A ) -> E. y ( y C_ Y /\ x = ( y i^i A ) ) )
39	18 38	impbii	|- ( E. y ( y C_ Y /\ x = ( y i^i A ) ) <-> x C_ ( Y i^i A ) )
40	6 39	bitri	|- ( E. y ( y e. ~P Y /\ x = ( y i^i A ) ) <-> x C_ ( Y i^i A ) )
41		df-rex	|- ( E. y e. ~P Y x = ( y i^i A ) <-> E. y ( y e. ~P Y /\ x = ( y i^i A ) ) )
42		velpw	|- ( x e. ~P ( Y i^i A ) <-> x C_ ( Y i^i A ) )
43	40 41 42	3bitr4i	|- ( E. y e. ~P Y x = ( y i^i A ) <-> x e. ~P ( Y i^i A ) )
44	3 43	bitrdi	|- ( ( Y e. V /\ A e. W ) -> ( x e. ( ~P Y |`t A ) <-> x e. ~P ( Y i^i A ) ) )
45	44	eqrdv	|- ( ( Y e. V /\ A e. W ) -> ( ~P Y |`t A ) = ~P ( Y i^i A ) )