Metamath Proof Explorer

Theorem mgcmnt2d

Description: Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024)

Ref Expression
Hypotheses mgcmntd.1 ⊢ H = V MGalConn W
mgcmntd.2 ⊢ φ → V ∈ Proset
mgcmntd.3 ⊢ φ → W ∈ Proset
mgcmntd.4 ⊢ φ → F H G
Assertion mgcmnt2d ⊢ φ → G ∈ W Monot V

Proof

Step Hyp Ref Expression
1 mgcmntd.1 ⊢ H = V MGalConn W
2 mgcmntd.2 ⊢ φ → V ∈ Proset
3 mgcmntd.3 ⊢ φ → W ∈ Proset
4 mgcmntd.4 ⊢ φ → F H G
5 eqid ⊢ Base V = Base V
6 eqid ⊢ Base W = Base W
7 eqid ⊢ ≤ V = ≤ V
8 eqid ⊢ ≤ W = ≤ W
9 5 6 7 8 1 2 3 4 mgcf2 ⊢ φ → G : Base W ⟶ Base V
10 5 6 7 8 1 2 3 dfmgc2 ⊢ φ → F H G ↔ F : Base V ⟶ Base W ∧ G : Base W ⟶ Base V ∧ ∀ x ∈ Base V ∀ y ∈ Base V x ≤ V y → F ⁡ x ≤ W F ⁡ y ∧ ∀ u ∈ Base W ∀ v ∈ Base W u ≤ W v → G ⁡ u ≤ V G ⁡ v ∧ ∀ u ∈ Base W F ⁡ G ⁡ u ≤ W u ∧ ∀ x ∈ Base V x ≤ V G ⁡ F ⁡ x
11 4 10 mpbid ⊢ φ → F : Base V ⟶ Base W ∧ G : Base W ⟶ Base V ∧ ∀ x ∈ Base V ∀ y ∈ Base V x ≤ V y → F ⁡ x ≤ W F ⁡ y ∧ ∀ u ∈ Base W ∀ v ∈ Base W u ≤ W v → G ⁡ u ≤ V G ⁡ v ∧ ∀ u ∈ Base W F ⁡ G ⁡ u ≤ W u ∧ ∀ x ∈ Base V x ≤ V G ⁡ F ⁡ x
12 11 simprld ⊢ φ → ∀ x ∈ Base V ∀ y ∈ Base V x ≤ V y → F ⁡ x ≤ W F ⁡ y ∧ ∀ u ∈ Base W ∀ v ∈ Base W u ≤ W v → G ⁡ u ≤ V G ⁡ v
13 12 simprd ⊢ φ → ∀ u ∈ Base W ∀ v ∈ Base W u ≤ W v → G ⁡ u ≤ V G ⁡ v
14 6 5 8 7 ismnt ⊢ W ∈ Proset ∧ V ∈ Proset → G ∈ W Monot V ↔ G : Base W ⟶ Base V ∧ ∀ u ∈ Base W ∀ v ∈ Base W u ≤ W v → G ⁡ u ≤ V G ⁡ v
15 14 biimpar ⊢ W ∈ Proset ∧ V ∈ Proset ∧ G : Base W ⟶ Base V ∧ ∀ u ∈ Base W ∀ v ∈ Base W u ≤ W v → G ⁡ u ≤ V G ⁡ v → G ∈ W Monot V
16 3 2 9 13 15 syl22anc ⊢ φ → G ∈ W Monot V