Metamath Proof Explorer


Theorem mgcmnt1

Description: The lower adjoint F 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 ( 𝜑𝐹 𝐻 𝐺 )
mgcmnt1.1 ( 𝜑𝑋𝐴 )
mgcmnt1.2 ( 𝜑𝑌𝐴 )
mgcmnt1.3 ( 𝜑𝑋 𝑌 )
Assertion mgcmnt1 ( 𝜑 → ( 𝐹𝑋 ) ( 𝐹𝑌 ) )

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 mgcmnt1.1 ( 𝜑𝑋𝐴 )
10 mgcmnt1.2 ( 𝜑𝑌𝐴 )
11 mgcmnt1.3 ( 𝜑𝑋 𝑌 )
12 1 2 3 4 5 6 7 mgcval ( 𝜑 → ( 𝐹 𝐻 𝐺 ↔ ( ( 𝐹 : 𝐴𝐵𝐺 : 𝐵𝐴 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) ) ) )
13 8 12 mpbid ( 𝜑 → ( ( 𝐹 : 𝐴𝐵𝐺 : 𝐵𝐴 ) ∧ ∀ 𝑥𝐴𝑦𝐵 ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) ) )
14 13 simplrd ( 𝜑𝐺 : 𝐵𝐴 )
15 13 simplld ( 𝜑𝐹 : 𝐴𝐵 )
16 15 10 ffvelrnd ( 𝜑 → ( 𝐹𝑌 ) ∈ 𝐵 )
17 14 16 ffvelrnd ( 𝜑 → ( 𝐺 ‘ ( 𝐹𝑌 ) ) ∈ 𝐴 )
18 1 2 3 4 5 6 7 8 10 mgccole1 ( 𝜑𝑌 ( 𝐺 ‘ ( 𝐹𝑌 ) ) )
19 1 3 prstr ( ( 𝑉 ∈ Proset ∧ ( 𝑋𝐴𝑌𝐴 ∧ ( 𝐺 ‘ ( 𝐹𝑌 ) ) ∈ 𝐴 ) ∧ ( 𝑋 𝑌𝑌 ( 𝐺 ‘ ( 𝐹𝑌 ) ) ) ) → 𝑋 ( 𝐺 ‘ ( 𝐹𝑌 ) ) )
20 6 9 10 17 11 18 19 syl132anc ( 𝜑𝑋 ( 𝐺 ‘ ( 𝐹𝑌 ) ) )
21 13 simprd ( 𝜑 → ∀ 𝑥𝐴𝑦𝐵 ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) )
22 fveq2 ( 𝑥 = 𝑋 → ( 𝐹𝑥 ) = ( 𝐹𝑋 ) )
23 22 breq1d ( 𝑥 = 𝑋 → ( ( 𝐹𝑥 ) 𝑦 ↔ ( 𝐹𝑋 ) 𝑦 ) )
24 breq1 ( 𝑥 = 𝑋 → ( 𝑥 ( 𝐺𝑦 ) ↔ 𝑋 ( 𝐺𝑦 ) ) )
25 23 24 bibi12d ( 𝑥 = 𝑋 → ( ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) ↔ ( ( 𝐹𝑋 ) 𝑦𝑋 ( 𝐺𝑦 ) ) ) )
26 25 adantl ( ( 𝜑𝑥 = 𝑋 ) → ( ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) ↔ ( ( 𝐹𝑋 ) 𝑦𝑋 ( 𝐺𝑦 ) ) ) )
27 26 ralbidv ( ( 𝜑𝑥 = 𝑋 ) → ( ∀ 𝑦𝐵 ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) ↔ ∀ 𝑦𝐵 ( ( 𝐹𝑋 ) 𝑦𝑋 ( 𝐺𝑦 ) ) ) )
28 9 27 rspcdv ( 𝜑 → ( ∀ 𝑥𝐴𝑦𝐵 ( ( 𝐹𝑥 ) 𝑦𝑥 ( 𝐺𝑦 ) ) → ∀ 𝑦𝐵 ( ( 𝐹𝑋 ) 𝑦𝑋 ( 𝐺𝑦 ) ) ) )
29 21 28 mpd ( 𝜑 → ∀ 𝑦𝐵 ( ( 𝐹𝑋 ) 𝑦𝑋 ( 𝐺𝑦 ) ) )
30 simpr ( ( 𝜑𝑦 = ( 𝐹𝑌 ) ) → 𝑦 = ( 𝐹𝑌 ) )
31 30 breq2d ( ( 𝜑𝑦 = ( 𝐹𝑌 ) ) → ( ( 𝐹𝑋 ) 𝑦 ↔ ( 𝐹𝑋 ) ( 𝐹𝑌 ) ) )
32 30 fveq2d ( ( 𝜑𝑦 = ( 𝐹𝑌 ) ) → ( 𝐺𝑦 ) = ( 𝐺 ‘ ( 𝐹𝑌 ) ) )
33 32 breq2d ( ( 𝜑𝑦 = ( 𝐹𝑌 ) ) → ( 𝑋 ( 𝐺𝑦 ) ↔ 𝑋 ( 𝐺 ‘ ( 𝐹𝑌 ) ) ) )
34 31 33 bibi12d ( ( 𝜑𝑦 = ( 𝐹𝑌 ) ) → ( ( ( 𝐹𝑋 ) 𝑦𝑋 ( 𝐺𝑦 ) ) ↔ ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ↔ 𝑋 ( 𝐺 ‘ ( 𝐹𝑌 ) ) ) ) )
35 16 34 rspcdv ( 𝜑 → ( ∀ 𝑦𝐵 ( ( 𝐹𝑋 ) 𝑦𝑋 ( 𝐺𝑦 ) ) → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ↔ 𝑋 ( 𝐺 ‘ ( 𝐹𝑌 ) ) ) ) )
36 29 35 mpd ( 𝜑 → ( ( 𝐹𝑋 ) ( 𝐹𝑌 ) ↔ 𝑋 ( 𝐺 ‘ ( 𝐹𝑌 ) ) ) )
37 20 36 mpbird ( 𝜑 → ( 𝐹𝑋 ) ( 𝐹𝑌 ) )