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 ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
mgccnv.2 ⊢ 𝑀 = ( ( ODual ‘ 𝑊 ) MGalConn ( ODual ‘ 𝑉 ) )
Assertion mgccnv ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → ( 𝐹 𝐻 𝐺 ↔ 𝐺 𝑀 𝐹 ) )

Proof

Step Hyp Ref Expression
1 mgccnv.1 ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
2 mgccnv.2 ⊢ 𝑀 = ( ( ODual ‘ 𝑊 ) MGalConn ( ODual ‘ 𝑉 ) )
3 ancom ⊢ ( ( 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ∧ 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ) ↔ ( 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ∧ 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ) )
4 3 a1i ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → ( ( 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ∧ 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ) ↔ ( 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ∧ 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ) ) )
5 ralcom ⊢ ( ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 ↔ 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ( ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 ↔ 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) ) )
6 bicom ⊢ ( ( ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 ↔ 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 ) )
7 fvex ⊢ ( 𝐺 ‘ 𝑦 ) ∈ V
8 vex ⊢ 𝑥 ∈ V
9 7 8 brcnv ⊢ ( ( 𝐺 ‘ 𝑦 ) ◡ ( le ‘ 𝑉 ) 𝑥 ↔ 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) )
10 9 bicomi ⊢ ( 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝑦 ) ◡ ( le ‘ 𝑉 ) 𝑥 )
11 10 a1i ⊢ ( ( ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) → ( 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝑦 ) ◡ ( le ‘ 𝑉 ) 𝑥 ) )
12 vex ⊢ 𝑦 ∈ V
13 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
14 12 13 brcnv ⊢ ( 𝑦 ◡ ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 )
15 14 bicomi ⊢ ( ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 ↔ 𝑦 ◡ ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) )
16 15 a1i ⊢ ( ( ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 ↔ 𝑦 ◡ ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) )
17 11 16 bibi12d ⊢ ( ( ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) → ( ( 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 ) ↔ ( ( 𝐺 ‘ 𝑦 ) ◡ ( le ‘ 𝑉 ) 𝑥 ↔ 𝑦 ◡ ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ) )
18 6 17 syl5bb ⊢ ( ( ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) ∧ 𝑥 ∈ ( Base ‘ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 ↔ 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( 𝐺 ‘ 𝑦 ) ◡ ( le ‘ 𝑉 ) 𝑥 ↔ 𝑦 ◡ ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ) )
19 18 ralbidva ⊢ ( ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ( ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 ↔ 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ( ( 𝐺 ‘ 𝑦 ) ◡ ( le ‘ 𝑉 ) 𝑥 ↔ 𝑦 ◡ ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ) )
20 19 ralbidva ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ( ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 ↔ 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ( ( 𝐺 ‘ 𝑦 ) ◡ ( le ‘ 𝑉 ) 𝑥 ↔ 𝑦 ◡ ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ) )
21 5 20 syl5bb ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 ↔ 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ( ( 𝐺 ‘ 𝑦 ) ◡ ( le ‘ 𝑉 ) 𝑥 ↔ 𝑦 ◡ ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ) )
22 4 21 anbi12d ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → ( ( ( 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ∧ 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 ↔ 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( ( 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ∧ 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ( ( 𝐺 ‘ 𝑦 ) ◡ ( le ‘ 𝑉 ) 𝑥 ↔ 𝑦 ◡ ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ) ) )
23 eqid ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ 𝑉 )
24 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
25 eqid ⊢ ( le ‘ 𝑉 ) = ( le ‘ 𝑉 )
26 eqid ⊢ ( le ‘ 𝑊 ) = ( le ‘ 𝑊 )
27 simpl ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → 𝑉 ∈ Proset )
28 simpr ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → 𝑊 ∈ Proset )
29 23 24 25 26 1 27 28 mgcval ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ∧ 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ) ∧ ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ( ( 𝐹 ‘ 𝑥 ) ( le ‘ 𝑊 ) 𝑦 ↔ 𝑥 ( le ‘ 𝑉 ) ( 𝐺 ‘ 𝑦 ) ) ) ) )
30 eqid ⊢ ( ODual ‘ 𝑊 ) = ( ODual ‘ 𝑊 )
31 30 24 odubas ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( ODual ‘ 𝑊 ) )
32 eqid ⊢ ( ODual ‘ 𝑉 ) = ( ODual ‘ 𝑉 )
33 32 23 odubas ⊢ ( Base ‘ 𝑉 ) = ( Base ‘ ( ODual ‘ 𝑉 ) )
34 30 26 oduleval ⊢ ◡ ( le ‘ 𝑊 ) = ( le ‘ ( ODual ‘ 𝑊 ) )
35 32 25 oduleval ⊢ ◡ ( le ‘ 𝑉 ) = ( le ‘ ( ODual ‘ 𝑉 ) )
36 30 oduprs ⊢ ( 𝑊 ∈ Proset → ( ODual ‘ 𝑊 ) ∈ Proset )
37 28 36 syl ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → ( ODual ‘ 𝑊 ) ∈ Proset )
38 32 oduprs ⊢ ( 𝑉 ∈ Proset → ( ODual ‘ 𝑉 ) ∈ Proset )
39 27 38 syl ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → ( ODual ‘ 𝑉 ) ∈ Proset )
40 31 33 34 35 2 37 39 mgcval ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → ( 𝐺 𝑀 𝐹 ↔ ( ( 𝐺 : ( Base ‘ 𝑊 ) ⟶ ( Base ‘ 𝑉 ) ∧ 𝐹 : ( Base ‘ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ) ∧ ∀ 𝑦 ∈ ( Base ‘ 𝑊 ) ∀ 𝑥 ∈ ( Base ‘ 𝑉 ) ( ( 𝐺 ‘ 𝑦 ) ◡ ( le ‘ 𝑉 ) 𝑥 ↔ 𝑦 ◡ ( le ‘ 𝑊 ) ( 𝐹 ‘ 𝑥 ) ) ) ) )
41 22 29 40 3bitr4d ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑊 ∈ Proset ) → ( 𝐹 𝐻 𝐺 ↔ 𝐺 𝑀 𝐹 ) )