Metamath Proof Explorer

Theorem isocnv3

Description: Complementation law for isomorphism. (Contributed by Mario Carneiro, 9-Sep-2015)

Ref Expression
Hypotheses isocnv3.1 
|- C = ( ( A X. A ) \ R )
isocnv3.2 
|- D = ( ( B X. B ) \ S )
Assertion isocnv3 
|- ( H Isom R , S ( A , B ) <-> H Isom C , D ( A , B ) )

Proof

Step Hyp Ref Expression
1 isocnv3.1 
 |-  C = ( ( A X. A ) \ R )
2 isocnv3.2 
 |-  D = ( ( B X. B ) \ S )
3 notbi 
 |-  ( ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> ( -. x R y <-> -. ( H ` x ) S ( H ` y ) ) )
4 brxp 
 |-  ( x ( A X. A ) y <-> ( x e. A /\ y e. A ) )
5 1 breqi 
 |-  ( x C y <-> x ( ( A X. A ) \ R ) y )
6 brdif 
 |-  ( x ( ( A X. A ) \ R ) y <-> ( x ( A X. A ) y /\ -. x R y ) )
7 5 6 bitri 
 |-  ( x C y <-> ( x ( A X. A ) y /\ -. x R y ) )
8 7 baib 
 |-  ( x ( A X. A ) y -> ( x C y <-> -. x R y ) )
9 4 8 sylbir 
 |-  ( ( x e. A /\ y e. A ) -> ( x C y <-> -. x R y ) )
10 9 adantl 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. A /\ y e. A ) ) -> ( x C y <-> -. x R y ) )
11 f1of 
 |-  ( H : A -1-1-onto-> B -> H : A --> B )
12 ffvelrn 
 |-  ( ( H : A --> B /\ x e. A ) -> ( H ` x ) e. B )
13 ffvelrn 
 |-  ( ( H : A --> B /\ y e. A ) -> ( H ` y ) e. B )
14 12 13 anim12dan 
 |-  ( ( H : A --> B /\ ( x e. A /\ y e. A ) ) -> ( ( H ` x ) e. B /\ ( H ` y ) e. B ) )
15 brxp 
 |-  ( ( H ` x ) ( B X. B ) ( H ` y ) <-> ( ( H ` x ) e. B /\ ( H ` y ) e. B ) )
16 14 15 sylibr 
 |-  ( ( H : A --> B /\ ( x e. A /\ y e. A ) ) -> ( H ` x ) ( B X. B ) ( H ` y ) )
17 11 16 sylan 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. A /\ y e. A ) ) -> ( H ` x ) ( B X. B ) ( H ` y ) )
18 2 breqi 
 |-  ( ( H ` x ) D ( H ` y ) <-> ( H ` x ) ( ( B X. B ) \ S ) ( H ` y ) )
19 brdif 
 |-  ( ( H ` x ) ( ( B X. B ) \ S ) ( H ` y ) <-> ( ( H ` x ) ( B X. B ) ( H ` y ) /\ -. ( H ` x ) S ( H ` y ) ) )
20 18 19 bitri 
 |-  ( ( H ` x ) D ( H ` y ) <-> ( ( H ` x ) ( B X. B ) ( H ` y ) /\ -. ( H ` x ) S ( H ` y ) ) )
21 20 baib 
 |-  ( ( H ` x ) ( B X. B ) ( H ` y ) -> ( ( H ` x ) D ( H ` y ) <-> -. ( H ` x ) S ( H ` y ) ) )
22 17 21 syl 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. A /\ y e. A ) ) -> ( ( H ` x ) D ( H ` y ) <-> -. ( H ` x ) S ( H ` y ) ) )
23 10 22 bibi12d 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. A /\ y e. A ) ) -> ( ( x C y <-> ( H ` x ) D ( H ` y ) ) <-> ( -. x R y <-> -. ( H ` x ) S ( H ` y ) ) ) )
24 3 23 bitr4id 
 |-  ( ( H : A -1-1-onto-> B /\ ( x e. A /\ y e. A ) ) -> ( ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> ( x C y <-> ( H ` x ) D ( H ` y ) ) ) )
25 24 2ralbidva 
 |-  ( H : A -1-1-onto-> B -> ( A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) <-> A. x e. A A. y e. A ( x C y <-> ( H ` x ) D ( H ` y ) ) ) )
26 25 pm5.32i 
 |-  ( ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x C y <-> ( H ` x ) D ( H ` y ) ) ) )
27 df-isom 
 |-  ( H Isom R , S ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x R y <-> ( H ` x ) S ( H ` y ) ) ) )
28 df-isom 
 |-  ( H Isom C , D ( A , B ) <-> ( H : A -1-1-onto-> B /\ A. x e. A A. y e. A ( x C y <-> ( H ` x ) D ( H ` y ) ) ) )
29 26 27 28 3bitr4i 
 |-  ( H Isom R , S ( A , B ) <-> H Isom C , D ( A , B ) )