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

Metamath Proof Explorer

Theorem compssiso

Description: Complementation is an antiautomorphism on power set lattices. (Contributed by Stefan O'Rear, 4-Nov-2014) (Proof shortened by Mario Carneiro, 17-May-2015)

Ref Expression
Hypothesis compss.a 
|- F = ( x e. ~P A |-> ( A \ x ) )
Assertion compssiso 
|- ( A e. V -> F Isom [C.] , `' [C.] ( ~P A , ~P A ) )

Proof

Step Hyp Ref Expression
1 compss.a 
 |-  F = ( x e. ~P A |-> ( A \ x ) )
2 difexg 
 |-  ( A e. V -> ( A \ x ) e. _V )
3 2 ralrimivw 
 |-  ( A e. V -> A. x e. ~P A ( A \ x ) e. _V )
4 1 fnmpt 
 |-  ( A. x e. ~P A ( A \ x ) e. _V -> F Fn ~P A )
5 3 4 syl 
 |-  ( A e. V -> F Fn ~P A )
6 1 compsscnv 
 |-  `' F = F
7 6 fneq1i 
 |-  ( `' F Fn ~P A <-> F Fn ~P A )
8 5 7 sylibr 
 |-  ( A e. V -> `' F Fn ~P A )
9 dff1o4 
 |-  ( F : ~P A -1-1-onto-> ~P A <-> ( F Fn ~P A /\ `' F Fn ~P A ) )
10 5 8 9 sylanbrc 
 |-  ( A e. V -> F : ~P A -1-1-onto-> ~P A )
11 elpwi 
 |-  ( b e. ~P A -> b C_ A )
12 11 ad2antll 
 |-  ( ( A e. V /\ ( a e. ~P A /\ b e. ~P A ) ) -> b C_ A )
13 1 isf34lem1 
 |-  ( ( A e. V /\ b C_ A ) -> ( F ` b ) = ( A \ b ) )
14 12 13 syldan 
 |-  ( ( A e. V /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( F ` b ) = ( A \ b ) )
15 elpwi 
 |-  ( a e. ~P A -> a C_ A )
16 15 ad2antrl 
 |-  ( ( A e. V /\ ( a e. ~P A /\ b e. ~P A ) ) -> a C_ A )
17 1 isf34lem1 
 |-  ( ( A e. V /\ a C_ A ) -> ( F ` a ) = ( A \ a ) )
18 16 17 syldan 
 |-  ( ( A e. V /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( F ` a ) = ( A \ a ) )
19 14 18 psseq12d 
 |-  ( ( A e. V /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( ( F ` b ) C. ( F ` a ) <-> ( A \ b ) C. ( A \ a ) ) )
20 difss 
 |-  ( A \ a ) C_ A
21 pssdifcom1 
 |-  ( ( b C_ A /\ ( A \ a ) C_ A ) -> ( ( A \ b ) C. ( A \ a ) <-> ( A \ ( A \ a ) ) C. b ) )
22 12 20 21 sylancl 
 |-  ( ( A e. V /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( ( A \ b ) C. ( A \ a ) <-> ( A \ ( A \ a ) ) C. b ) )
23 dfss4 
 |-  ( a C_ A <-> ( A \ ( A \ a ) ) = a )
24 16 23 sylib 
 |-  ( ( A e. V /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( A \ ( A \ a ) ) = a )
25 24 psseq1d 
 |-  ( ( A e. V /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( ( A \ ( A \ a ) ) C. b <-> a C. b ) )
26 19 22 25 3bitrrd 
 |-  ( ( A e. V /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( a C. b <-> ( F ` b ) C. ( F ` a ) ) )
27 vex 
 |-  b e. _V
28 27 brrpss 
 |-  ( a [C.] b <-> a C. b )
29 fvex 
 |-  ( F ` a ) e. _V
30 29 brrpss 
 |-  ( ( F ` b ) [C.] ( F ` a ) <-> ( F ` b ) C. ( F ` a ) )
31 26 28 30 3bitr4g 
 |-  ( ( A e. V /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( a [C.] b <-> ( F ` b ) [C.] ( F ` a ) ) )
32 relrpss 
 |-  Rel [C.]
33 32 relbrcnv 
 |-  ( ( F ` a ) `' [C.] ( F ` b ) <-> ( F ` b ) [C.] ( F ` a ) )
34 31 33 bitr4di 
 |-  ( ( A e. V /\ ( a e. ~P A /\ b e. ~P A ) ) -> ( a [C.] b <-> ( F ` a ) `' [C.] ( F ` b ) ) )
35 34 ralrimivva 
 |-  ( A e. V -> A. a e. ~P A A. b e. ~P A ( a [C.] b <-> ( F ` a ) `' [C.] ( F ` b ) ) )
36 df-isom 
 |-  ( F Isom [C.] , `' [C.] ( ~P A , ~P A ) <-> ( F : ~P A -1-1-onto-> ~P A /\ A. a e. ~P A A. b e. ~P A ( a [C.] b <-> ( F ` a ) `' [C.] ( F ` b ) ) ) )
37 10 35 36 sylanbrc 
 |-  ( A e. V -> F Isom [C.] , `' [C.] ( ~P A , ~P A ) )