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 = ( x e. ~P A |-> ( A \ x ) )
Assertion	compsscnv	|- `' F = F

Proof

Step	Hyp	Ref	Expression
1		compss.a	|- F = ( x e. ~P A |-> ( A \ x ) )
2		cnvopab	|- `' { <. y , x >. | ( y e. ~P A /\ x = ( A \ y ) ) } = { <. x , y >. | ( y e. ~P A /\ x = ( A \ y ) ) }
3		difeq2	|- ( x = y -> ( A \ x ) = ( A \ y ) )
4	3	cbvmptv	|- ( x e. ~P A |-> ( A \ x ) ) = ( y e. ~P A |-> ( A \ y ) )
5		df-mpt	|- ( y e. ~P A |-> ( A \ y ) ) = { <. y , x >. | ( y e. ~P A /\ x = ( A \ y ) ) }
6	1 4 5	3eqtri	|- F = { <. y , x >. | ( y e. ~P A /\ x = ( A \ y ) ) }
7	6	cnveqi	|- `' F = `' { <. y , x >. | ( y e. ~P A /\ x = ( A \ y ) ) }
8		df-mpt	|- ( x e. ~P A |-> ( A \ x ) ) = { <. x , y >. | ( x e. ~P A /\ y = ( A \ x ) ) }
9		compsscnvlem	|- ( ( y e. ~P A /\ x = ( A \ y ) ) -> ( x e. ~P A /\ y = ( A \ x ) ) )
10		compsscnvlem	|- ( ( x e. ~P A /\ y = ( A \ x ) ) -> ( y e. ~P A /\ x = ( A \ y ) ) )
11	9 10	impbii	|- ( ( y e. ~P A /\ x = ( A \ y ) ) <-> ( x e. ~P A /\ y = ( A \ x ) ) )
12	11	opabbii	|- { <. x , y >. | ( y e. ~P A /\ x = ( A \ y ) ) } = { <. x , y >. | ( x e. ~P A /\ y = ( A \ x ) ) }
13	8 1 12	3eqtr4i	|- F = { <. x , y >. | ( y e. ~P A /\ x = ( A \ y ) ) }
14	2 7 13	3eqtr4i	|- `' F = F