Metamath Proof Explorer

Theorem mgccnv

Description: The inverse Galois connection is the Galois connection of the dual orders. (Contributed by Thierry Arnoux, 26-Apr-2024)

Ref Expression
Hypotheses mgccnv.1 
|- H = ( V MGalConn W )
mgccnv.2 
|- M = ( ( ODual ` W ) MGalConn ( ODual ` V ) )
Assertion mgccnv 
|- ( ( V e. Proset /\ W e. Proset ) -> ( F H G <-> G M F ) )

Proof

Step Hyp Ref Expression
1 mgccnv.1 
 |-  H = ( V MGalConn W )
2 mgccnv.2 
 |-  M = ( ( ODual ` W ) MGalConn ( ODual ` V ) )
3 ancom 
 |-  ( ( F : ( Base ` V ) --> ( Base ` W ) /\ G : ( Base ` W ) --> ( Base ` V ) ) <-> ( G : ( Base ` W ) --> ( Base ` V ) /\ F : ( Base ` V ) --> ( Base ` W ) ) )
4 3 a1i 
 |-  ( ( V e. Proset /\ W e. Proset ) -> ( ( F : ( Base ` V ) --> ( Base ` W ) /\ G : ( Base ` W ) --> ( Base ` V ) ) <-> ( G : ( Base ` W ) --> ( Base ` V ) /\ F : ( Base ` V ) --> ( Base ` W ) ) ) )
5 ralcom 
 |-  ( A. x e. ( Base ` V ) A. y e. ( Base ` W ) ( ( F ` x ) ( le ` W ) y <-> x ( le ` V ) ( G ` y ) ) <-> A. y e. ( Base ` W ) A. x e. ( Base ` V ) ( ( F ` x ) ( le ` W ) y <-> x ( le ` V ) ( G ` y ) ) )
6 bicom 
 |-  ( ( ( F ` x ) ( le ` W ) y <-> x ( le ` V ) ( G ` y ) ) <-> ( x ( le ` V ) ( G ` y ) <-> ( F ` x ) ( le ` W ) y ) )
7 fvex 
 |-  ( G ` y ) e. _V
8 vex 
 |-  x e. _V
9 7 8 brcnv 
 |-  ( ( G ` y ) `' ( le ` V ) x <-> x ( le ` V ) ( G ` y ) )
10 9 bicomi 
 |-  ( x ( le ` V ) ( G ` y ) <-> ( G ` y ) `' ( le ` V ) x )
11 10 a1i 
 |-  ( ( ( ( V e. Proset /\ W e. Proset ) /\ y e. ( Base ` W ) ) /\ x e. ( Base ` V ) ) -> ( x ( le ` V ) ( G ` y ) <-> ( G ` y ) `' ( le ` V ) x ) )
12 vex 
 |-  y e. _V
13 fvex 
 |-  ( F ` x ) e. _V
14 12 13 brcnv 
 |-  ( y `' ( le ` W ) ( F ` x ) <-> ( F ` x ) ( le ` W ) y )
15 14 bicomi 
 |-  ( ( F ` x ) ( le ` W ) y <-> y `' ( le ` W ) ( F ` x ) )
16 15 a1i 
 |-  ( ( ( ( V e. Proset /\ W e. Proset ) /\ y e. ( Base ` W ) ) /\ x e. ( Base ` V ) ) -> ( ( F ` x ) ( le ` W ) y <-> y `' ( le ` W ) ( F ` x ) ) )
17 11 16 bibi12d 
 |-  ( ( ( ( V e. Proset /\ W e. Proset ) /\ y e. ( Base ` W ) ) /\ x e. ( Base ` V ) ) -> ( ( x ( le ` V ) ( G ` y ) <-> ( F ` x ) ( le ` W ) y ) <-> ( ( G ` y ) `' ( le ` V ) x <-> y `' ( le ` W ) ( F ` x ) ) ) )
18 6 17 syl5bb 
 |-  ( ( ( ( V e. Proset /\ W e. Proset ) /\ y e. ( Base ` W ) ) /\ x e. ( Base ` V ) ) -> ( ( ( F ` x ) ( le ` W ) y <-> x ( le ` V ) ( G ` y ) ) <-> ( ( G ` y ) `' ( le ` V ) x <-> y `' ( le ` W ) ( F ` x ) ) ) )
19 18 ralbidva 
 |-  ( ( ( V e. Proset /\ W e. Proset ) /\ y e. ( Base ` W ) ) -> ( A. x e. ( Base ` V ) ( ( F ` x ) ( le ` W ) y <-> x ( le ` V ) ( G ` y ) ) <-> A. x e. ( Base ` V ) ( ( G ` y ) `' ( le ` V ) x <-> y `' ( le ` W ) ( F ` x ) ) ) )
20 19 ralbidva 
 |-  ( ( V e. Proset /\ W e. Proset ) -> ( A. y e. ( Base ` W ) A. x e. ( Base ` V ) ( ( F ` x ) ( le ` W ) y <-> x ( le ` V ) ( G ` y ) ) <-> A. y e. ( Base ` W ) A. x e. ( Base ` V ) ( ( G ` y ) `' ( le ` V ) x <-> y `' ( le ` W ) ( F ` x ) ) ) )
21 5 20 syl5bb 
 |-  ( ( V e. Proset /\ W e. Proset ) -> ( A. x e. ( Base ` V ) A. y e. ( Base ` W ) ( ( F ` x ) ( le ` W ) y <-> x ( le ` V ) ( G ` y ) ) <-> A. y e. ( Base ` W ) A. x e. ( Base ` V ) ( ( G ` y ) `' ( le ` V ) x <-> y `' ( le ` W ) ( F ` x ) ) ) )
22 4 21 anbi12d 
 |-  ( ( V e. Proset /\ W e. Proset ) -> ( ( ( F : ( Base ` V ) --> ( Base ` W ) /\ G : ( Base ` W ) --> ( Base ` V ) ) /\ A. x e. ( Base ` V ) A. y e. ( Base ` W ) ( ( F ` x ) ( le ` W ) y <-> x ( le ` V ) ( G ` y ) ) ) <-> ( ( G : ( Base ` W ) --> ( Base ` V ) /\ F : ( Base ` V ) --> ( Base ` W ) ) /\ A. y e. ( Base ` W ) A. x e. ( Base ` V ) ( ( G ` y ) `' ( le ` V ) x <-> y `' ( le ` W ) ( F ` x ) ) ) ) )
23 eqid 
 |-  ( Base ` V ) = ( Base ` V )
24 eqid 
 |-  ( Base ` W ) = ( Base ` W )
25 eqid 
 |-  ( le ` V ) = ( le ` V )
26 eqid 
 |-  ( le ` W ) = ( le ` W )
27 simpl 
 |-  ( ( V e. Proset /\ W e. Proset ) -> V e. Proset )
28 simpr 
 |-  ( ( V e. Proset /\ W e. Proset ) -> W e. Proset )
29 23 24 25 26 1 27 28 mgcval 
 |-  ( ( V e. Proset /\ W e. Proset ) -> ( F H G <-> ( ( F : ( Base ` V ) --> ( Base ` W ) /\ G : ( Base ` W ) --> ( Base ` V ) ) /\ A. x e. ( Base ` V ) A. y e. ( Base ` W ) ( ( F ` x ) ( le ` W ) y <-> x ( le ` V ) ( G ` y ) ) ) ) )
30 eqid 
 |-  ( ODual ` W ) = ( ODual ` W )
31 30 24 odubas 
 |-  ( Base ` W ) = ( Base ` ( ODual ` W ) )
32 eqid 
 |-  ( ODual ` V ) = ( ODual ` V )
33 32 23 odubas 
 |-  ( Base ` V ) = ( Base ` ( ODual ` V ) )
34 30 26 oduleval 
 |-  `' ( le ` W ) = ( le ` ( ODual ` W ) )
35 32 25 oduleval 
 |-  `' ( le ` V ) = ( le ` ( ODual ` V ) )
36 30 oduprs 
 |-  ( W e. Proset -> ( ODual ` W ) e. Proset )
37 28 36 syl 
 |-  ( ( V e. Proset /\ W e. Proset ) -> ( ODual ` W ) e. Proset )
38 32 oduprs 
 |-  ( V e. Proset -> ( ODual ` V ) e. Proset )
39 27 38 syl 
 |-  ( ( V e. Proset /\ W e. Proset ) -> ( ODual ` V ) e. Proset )
40 31 33 34 35 2 37 39 mgcval 
 |-  ( ( V e. Proset /\ W e. Proset ) -> ( G M F <-> ( ( G : ( Base ` W ) --> ( Base ` V ) /\ F : ( Base ` V ) --> ( Base ` W ) ) /\ A. y e. ( Base ` W ) A. x e. ( Base ` V ) ( ( G ` y ) `' ( le ` V ) x <-> y `' ( le ` W ) ( F ` x ) ) ) ) )
41 22 29 40 3bitr4d 
 |-  ( ( V e. Proset /\ W e. Proset ) -> ( F H G <-> G M F ) )