Metamath Proof Explorer

Theorem mgcmnt2

Description: The upper adjoint G of a Galois connection is monotonically increasing. (Contributed by Thierry Arnoux, 26-Apr-2024)

Ref Expression
Hypotheses mgcoval.1 ⊢ 𝐴 = ( Base ‘ 𝑉 )
mgcoval.2 ⊢ 𝐵 = ( Base ‘ 𝑊 )
mgcoval.3 ⊢ ≤ = ( le ‘ 𝑉 )
mgcoval.4 ⊢ ≲ = ( le ‘ 𝑊 )
mgcval.1 ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
mgcval.2 ⊢ ( 𝜑 → 𝑉 ∈ Proset )
mgcval.3 ⊢ ( 𝜑 → 𝑊 ∈ Proset )
mgccole.1 ⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
mgcmnt2.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
mgcmnt2.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
mgcmnt2.3 ⊢ ( 𝜑 → 𝑋 ≲ 𝑌 )
Assertion mgcmnt2 ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≤ ( 𝐺 ‘ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 mgcoval.1 ⊢ 𝐴 = ( Base ‘ 𝑉 )
2 mgcoval.2 ⊢ 𝐵 = ( Base ‘ 𝑊 )
3 mgcoval.3 ⊢ ≤ = ( le ‘ 𝑉 )
4 mgcoval.4 ⊢ ≲ = ( le ‘ 𝑊 )
5 mgcval.1 ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
6 mgcval.2 ⊢ ( 𝜑 → 𝑉 ∈ Proset )
7 mgcval.3 ⊢ ( 𝜑 → 𝑊 ∈ Proset )
8 mgccole.1 ⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
9 mgcmnt2.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
10 mgcmnt2.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝐵 )
11 mgcmnt2.3 ⊢ ( 𝜑 → 𝑋 ≲ 𝑌 )
12 1 2 3 4 5 6 7 mgcval ⊢ ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) ) )
13 8 12 mpbid ⊢ ( 𝜑 → ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐺 : 𝐵 ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ) )
14 13 simplld ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
15 13 simplrd ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
16 15 9 ffvelrnd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ∈ 𝐴 )
17 14 16 ffvelrnd ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐵 )
18 1 2 3 4 5 6 7 8 9 mgccole2 ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ≲ 𝑋 )
19 2 4 prstr ⊢ ( ( 𝑊 ∈ Proset ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ≲ 𝑋 ∧ 𝑋 ≲ 𝑌 ) ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ≲ 𝑌 )
20 7 17 9 10 18 11 19 syl132anc ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ≲ 𝑌 )
21 breq2 ⊢ ( 𝑦 = 𝑌 → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ≲ 𝑦 ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ≲ 𝑌 ) )
22 fveq2 ⊢ ( 𝑦 = 𝑌 → ( 𝐺 ‘ 𝑦 ) = ( 𝐺 ‘ 𝑌 ) )
23 22 breq2d ⊢ ( 𝑦 = 𝑌 → ( ( 𝐺 ‘ 𝑋 ) ≤ ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝑋 ) ≤ ( 𝐺 ‘ 𝑌 ) ) )
24 21 23 bibi12d ⊢ ( 𝑦 = 𝑌 → ( ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ≲ 𝑦 ↔ ( 𝐺 ‘ 𝑋 ) ≤ ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ≲ 𝑌 ↔ ( 𝐺 ‘ 𝑋 ) ≤ ( 𝐺 ‘ 𝑌 ) ) ) )
25 fveq2 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑋 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) )
26 25 breq1d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑋 ) → ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ≲ 𝑦 ) )
27 breq1 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑋 ) → ( 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝑋 ) ≤ ( 𝐺 ‘ 𝑦 ) ) )
28 26 27 bibi12d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑋 ) → ( ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ↔ ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ≲ 𝑦 ↔ ( 𝐺 ‘ 𝑋 ) ≤ ( 𝐺 ‘ 𝑦 ) ) ) )
29 28 ralbidv ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑋 ) → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ≲ 𝑦 ↔ ( 𝐺 ‘ 𝑋 ) ≤ ( 𝐺 ‘ 𝑦 ) ) ) )
30 13 simprd ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑥 ) ≲ 𝑦 ↔ 𝑥 ≤ ( 𝐺 ‘ 𝑦 ) ) )
31 29 30 16 rspcdva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ≲ 𝑦 ↔ ( 𝐺 ‘ 𝑋 ) ≤ ( 𝐺 ‘ 𝑦 ) ) )
32 24 31 10 rspcdva ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝐺 ‘ 𝑋 ) ) ≲ 𝑌 ↔ ( 𝐺 ‘ 𝑋 ) ≤ ( 𝐺 ‘ 𝑌 ) ) )
33 20 32 mpbid ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) ≤ ( 𝐺 ‘ 𝑌 ) )