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=\left(x\in 𝒫A⟼A\setminus x\right)$$
Assertion	compss	$$⊢F\left[G\right]=\left\{y\in 𝒫A|A\setminus y\in G\right\}$$

Proof

Step	Hyp	Ref	Expression
1		compss.a	$$⊢F=\left(x\in 𝒫A⟼A\setminus x\right)$$
2	1	compsscnv	$$⊢F^{-1}=F$$
3	2	imaeq1i	$$⊢F^{-1}\left[G\right]=F\left[G\right]$$
4		difeq2	$$⊢x=y\to A\setminus x=A\setminus y$$
5	4	cbvmptv	$$⊢\left(x\in 𝒫A⟼A\setminus x\right)=\left(y\in 𝒫A⟼A\setminus y\right)$$
6	1 5	eqtri	$$⊢F=\left(y\in 𝒫A⟼A\setminus y\right)$$
7	6	mptpreima	$$⊢F^{-1}\left[G\right]=\left\{y\in 𝒫A|A\setminus y\in G\right\}$$
8	3 7	eqtr3i	$$⊢F\left[G\right]=\left\{y\in 𝒫A|A\setminus y\in G\right\}$$