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 No typesetting found for |- H = ( V MGalConn W ) with typecode |-
mgccnv.2 No typesetting found for |- M = ( ( ODual ` W ) MGalConn ( ODual ` V ) ) with typecode |-
Assertion mgccnv ⊢V∈Proset∧W∈Proset→FHG↔GMF

Proof

Step Hyp Ref Expression
1 mgccnv.1 Could not format H = ( V MGalConn W ) : No typesetting found for |- H = ( V MGalConn W ) with typecode |-
2 mgccnv.2 Could not format M = ( ( ODual ` W ) MGalConn ( ODual ` V ) ) : No typesetting found for |- M = ( ( ODual ` W ) MGalConn ( ODual ` V ) ) with typecode |-
3 ancom ⊢F:BaseV⟶BaseW∧G:BaseW⟶BaseV↔G:BaseW⟶BaseV∧F:BaseV⟶BaseW
4 3 a1i ⊢V∈Proset∧W∈Proset→F:BaseV⟶BaseW∧G:BaseW⟶BaseV↔G:BaseW⟶BaseV∧F:BaseV⟶BaseW
5 ralcom ⊢∀x∈BaseV∀y∈BaseWF⁡x≤Wy↔x≤VG⁡y↔∀y∈BaseW∀x∈BaseVF⁡x≤Wy↔x≤VG⁡y
6 bicom ⊢F⁡x≤Wy↔x≤VG⁡y↔x≤VG⁡y↔F⁡x≤Wy
7 fvex ⊢G⁡y∈V
8 vex ⊢x∈V
9 7 8 brcnv ⊢G⁡y≤V-1x↔x≤VG⁡y
10 9 bicomi ⊢x≤VG⁡y↔G⁡y≤V-1x
11 10 a1i ⊢V∈Proset∧W∈Proset∧y∈BaseW∧x∈BaseV→x≤VG⁡y↔G⁡y≤V-1x
12 vex ⊢y∈V
13 fvex ⊢F⁡x∈V
14 12 13 brcnv ⊢y≤W-1F⁡x↔F⁡x≤Wy
15 14 bicomi ⊢F⁡x≤Wy↔y≤W-1F⁡x
16 15 a1i ⊢V∈Proset∧W∈Proset∧y∈BaseW∧x∈BaseV→F⁡x≤Wy↔y≤W-1F⁡x
17 11 16 bibi12d ⊢V∈Proset∧W∈Proset∧y∈BaseW∧x∈BaseV→x≤VG⁡y↔F⁡x≤Wy↔G⁡y≤V-1x↔y≤W-1F⁡x
18 6 17 bitrid ⊢V∈Proset∧W∈Proset∧y∈BaseW∧x∈BaseV→F⁡x≤Wy↔x≤VG⁡y↔G⁡y≤V-1x↔y≤W-1F⁡x
19 18 ralbidva ⊢V∈Proset∧W∈Proset∧y∈BaseW→∀x∈BaseVF⁡x≤Wy↔x≤VG⁡y↔∀x∈BaseVG⁡y≤V-1x↔y≤W-1F⁡x
20 19 ralbidva ⊢V∈Proset∧W∈Proset→∀y∈BaseW∀x∈BaseVF⁡x≤Wy↔x≤VG⁡y↔∀y∈BaseW∀x∈BaseVG⁡y≤V-1x↔y≤W-1F⁡x
21 5 20 bitrid ⊢V∈Proset∧W∈Proset→∀x∈BaseV∀y∈BaseWF⁡x≤Wy↔x≤VG⁡y↔∀y∈BaseW∀x∈BaseVG⁡y≤V-1x↔y≤W-1F⁡x
22 4 21 anbi12d ⊢V∈Proset∧W∈Proset→F:BaseV⟶BaseW∧G:BaseW⟶BaseV∧∀x∈BaseV∀y∈BaseWF⁡x≤Wy↔x≤VG⁡y↔G:BaseW⟶BaseV∧F:BaseV⟶BaseW∧∀y∈BaseW∀x∈BaseVG⁡y≤V-1x↔y≤W-1F⁡x
23 eqid ⊢BaseV=BaseV
24 eqid ⊢BaseW=BaseW
25 eqid ⊢≤V=≤V
26 eqid ⊢≤W=≤W
27 simpl ⊢V∈Proset∧W∈Proset→V∈Proset
28 simpr ⊢V∈Proset∧W∈Proset→W∈Proset
29 23 24 25 26 1 27 28 mgcval ⊢V∈Proset∧W∈Proset→FHG↔F:BaseV⟶BaseW∧G:BaseW⟶BaseV∧∀x∈BaseV∀y∈BaseWF⁡x≤Wy↔x≤VG⁡y
30 eqid ⊢ODual⁡W=ODual⁡W
31 30 24 odubas ⊢BaseW=BaseODual⁡W
32 eqid ⊢ODual⁡V=ODual⁡V
33 32 23 odubas ⊢BaseV=BaseODual⁡V
34 30 26 oduleval ⊢≤W-1=≤ODual⁡W
35 32 25 oduleval ⊢≤V-1=≤ODual⁡V
36 30 oduprs ⊢W∈Proset→ODual⁡W∈Proset
37 28 36 syl ⊢V∈Proset∧W∈Proset→ODual⁡W∈Proset
38 32 oduprs ⊢V∈Proset→ODual⁡V∈Proset
39 27 38 syl ⊢V∈Proset∧W∈Proset→ODual⁡V∈Proset
40 31 33 34 35 2 37 39 mgcval ⊢V∈Proset∧W∈Proset→GMF↔G:BaseW⟶BaseV∧F:BaseV⟶BaseW∧∀y∈BaseW∀x∈BaseVG⁡y≤V-1x↔y≤W-1F⁡x
41 22 29 40 3bitr4d ⊢V∈Proset∧W∈Proset→FHG↔GMF