Theorem compss

Description: Express image under of the complementation isomorphism. (Contributed by Stefan O'Rear, 5-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

	Ref	Expression
Hypothesis	compss.a	|- F = ( x e. ~P A |-> ( A \ x ) )
Assertion	compss	|- ( F " G ) = { y e. ~P A | ( A \ y ) e. G }

Proof

Step	Hyp	Ref	Expression
1		compss.a	|- F = ( x e. ~P A |-> ( A \ x ) )
2	1	compsscnv	|- `' F = F
3	2	imaeq1i	|- ( `' F " G ) = ( F " G )
4		difeq2	|- ( x = y -> ( A \ x ) = ( A \ y ) )
5	4	cbvmptv	|- ( x e. ~P A |-> ( A \ x ) ) = ( y e. ~P A |-> ( A \ y ) )
6	1 5	eqtri	|- F = ( y e. ~P A |-> ( A \ y ) )
7	6	mptpreima	|- ( `' F " G ) = { y e. ~P A | ( A \ y ) e. G }
8	3 7	eqtr3i	|- ( F " G ) = { y e. ~P A | ( A \ y ) e. G }