Metamath Proof Explorer

Theorem mgcmnt1d

Description: Galois connection implies monotonicity of the left 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 mgcmnt1d ⊢ φ → F ∈ V Monot W

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 mgcf1 ⊢ φ → F : Base V ⟶ Base W
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 simpld ⊢ φ → ∀ x ∈ Base V ∀ y ∈ Base V x ≤ V y → F ⁡ x ≤ W F ⁡ y
14 5 6 7 8 ismnt ⊢ V ∈ Proset ∧ W ∈ Proset → F ∈ V Monot W ↔ F : Base V ⟶ Base W ∧ ∀ x ∈ Base V ∀ y ∈ Base V x ≤ V y → F ⁡ x ≤ W F ⁡ y
15 14 biimpar ⊢ V ∈ Proset ∧ W ∈ Proset ∧ F : Base V ⟶ Base W ∧ ∀ x ∈ Base V ∀ y ∈ Base V x ≤ V y → F ⁡ x ≤ W F ⁡ y → F ∈ V Monot W
16 2 3 9 13 15 syl22anc ⊢ φ → F ∈ V Monot W