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	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
Assertion	compss	⊢ ( 𝐹 “ 𝐺 ) = { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑦 ) ∈ 𝐺 }

Proof

Step	Hyp	Ref	Expression
1		compss.a	⊢ 𝐹 = ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) )
2	1	compsscnv	⊢ ◡ 𝐹 = 𝐹
3	2	imaeq1i	⊢ ( ◡ 𝐹 “ 𝐺 ) = ( 𝐹 “ 𝐺 )
4		difeq2	⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∖ 𝑥 ) = ( 𝐴 ∖ 𝑦 ) )
5	4	cbvmptv	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑥 ) ) = ( 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑦 ) )
6	1 5	eqtri	⊢ 𝐹 = ( 𝑦 ∈ 𝒫 𝐴 ↦ ( 𝐴 ∖ 𝑦 ) )
7	6	mptpreima	⊢ ( ◡ 𝐹 “ 𝐺 ) = { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑦 ) ∈ 𝐺 }
8	3 7	eqtr3i	⊢ ( 𝐹 “ 𝐺 ) = { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝐴 ∖ 𝑦 ) ∈ 𝐺 }