Theorem compsscnv

Description: Complementation on a power set lattice is an involution. (Contributed by Mario Carneiro, 17-May-2015)

	Ref	Expression
Hypothesis	compss.a	$$⊢F=\left(x\in 𝒫A⟼A\setminus x\right)$$
Assertion	compsscnv	$$⊢F^{-1}=F$$

Proof

Step	Hyp	Ref	Expression
1		compss.a	$$⊢F=\left(x\in 𝒫A⟼A\setminus x\right)$$
2		cnvopab	$$⊢{\left\{⟨y,x⟩|\left(y\in 𝒫A\wedge x=A\setminus y\right)\right\}}^{-1}=\left\{⟨x,y⟩|\left(y\in 𝒫A\wedge x=A\setminus y\right)\right\}$$
3		difeq2	$$⊢x=y\to A\setminus x=A\setminus y$$
4	3	cbvmptv	$$⊢\left(x\in 𝒫A⟼A\setminus x\right)=\left(y\in 𝒫A⟼A\setminus y\right)$$
5		df-mpt	$$⊢\left(y\in 𝒫A⟼A\setminus y\right)=\left\{⟨y,x⟩|\left(y\in 𝒫A\wedge x=A\setminus y\right)\right\}$$
6	1 4 5	3eqtri	$$⊢F=\left\{⟨y,x⟩|\left(y\in 𝒫A\wedge x=A\setminus y\right)\right\}$$
7	6	cnveqi	$$⊢F^{-1}={\left\{⟨y,x⟩|\left(y\in 𝒫A\wedge x=A\setminus y\right)\right\}}^{-1}$$
8		df-mpt	$$⊢\left(x\in 𝒫A⟼A\setminus x\right)=\left\{⟨x,y⟩|\left(x\in 𝒫A\wedge y=A\setminus x\right)\right\}$$
9		compsscnvlem	$$⊢\left(y\in 𝒫A\wedge x=A\setminus y\right)\to \left(x\in 𝒫A\wedge y=A\setminus x\right)$$
10		compsscnvlem	$$⊢\left(x\in 𝒫A\wedge y=A\setminus x\right)\to \left(y\in 𝒫A\wedge x=A\setminus y\right)$$
11	9 10	impbii	$$⊢\left(y\in 𝒫A\wedge x=A\setminus y\right)\leftrightarrow \left(x\in 𝒫A\wedge y=A\setminus x\right)$$
12	11	opabbii	$$⊢\left\{⟨x,y⟩|\left(y\in 𝒫A\wedge x=A\setminus y\right)\right\}=\left\{⟨x,y⟩|\left(x\in 𝒫A\wedge y=A\setminus x\right)\right\}$$
13	8 1 12	3eqtr4i	$$⊢F=\left\{⟨x,y⟩|\left(y\in 𝒫A\wedge x=A\setminus y\right)\right\}$$
14	2 7 13	3eqtr4i	$$⊢F^{-1}=F$$