This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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