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
|- A = ( Base ` V )
mgcoval.2
|- B = ( Base ` W )
mgcoval.3
|- .<_ = ( le ` V )
mgcoval.4
|- .c_ = ( le ` W )
mgcval.1
|- H = ( V MGalConn W )
mgcval.2
|- ( ph -> V e. Proset )
mgcval.3
|- ( ph -> W e. Proset )
mgccole.1
|- ( ph -> F H G )
mgcmnt2.1
|- ( ph -> X e. B )
mgcmnt2.2
|- ( ph -> Y e. B )
mgcmnt2.3
|- ( ph -> X .c_ Y )
Assertion mgcmnt2
|- ( ph -> ( G ` X ) .<_ ( G ` Y ) )

Proof

Step Hyp Ref Expression
1 mgcoval.1
 |-  A = ( Base ` V )
2 mgcoval.2
 |-  B = ( Base ` W )
3 mgcoval.3
 |-  .<_ = ( le ` V )
4 mgcoval.4
 |-  .c_ = ( le ` W )
5 mgcval.1
 |-  H = ( V MGalConn W )
6 mgcval.2
 |-  ( ph -> V e. Proset )
7 mgcval.3
 |-  ( ph -> W e. Proset )
8 mgccole.1
 |-  ( ph -> F H G )
9 mgcmnt2.1
 |-  ( ph -> X e. B )
10 mgcmnt2.2
 |-  ( ph -> Y e. B )
11 mgcmnt2.3
 |-  ( ph -> X .c_ Y )
12 1 2 3 4 5 6 7 mgcval
 |-  ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) )
13 8 12 mpbid
 |-  ( ph -> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) )
14 13 simplld
 |-  ( ph -> F : A --> B )
15 13 simplrd
 |-  ( ph -> G : B --> A )
16 15 9 ffvelrnd
 |-  ( ph -> ( G ` X ) e. A )
17 14 16 ffvelrnd
 |-  ( ph -> ( F ` ( G ` X ) ) e. B )
18 1 2 3 4 5 6 7 8 9 mgccole2
 |-  ( ph -> ( F ` ( G ` X ) ) .c_ X )
19 2 4 prstr
 |-  ( ( W e. Proset /\ ( ( F ` ( G ` X ) ) e. B /\ X e. B /\ Y e. B ) /\ ( ( F ` ( G ` X ) ) .c_ X /\ X .c_ Y ) ) -> ( F ` ( G ` X ) ) .c_ Y )
20 7 17 9 10 18 11 19 syl132anc
 |-  ( ph -> ( F ` ( G ` X ) ) .c_ Y )
21 breq2
 |-  ( y = Y -> ( ( F ` ( G ` X ) ) .c_ y <-> ( F ` ( G ` X ) ) .c_ Y ) )
22 fveq2
 |-  ( y = Y -> ( G ` y ) = ( G ` Y ) )
23 22 breq2d
 |-  ( y = Y -> ( ( G ` X ) .<_ ( G ` y ) <-> ( G ` X ) .<_ ( G ` Y ) ) )
24 21 23 bibi12d
 |-  ( y = Y -> ( ( ( F ` ( G ` X ) ) .c_ y <-> ( G ` X ) .<_ ( G ` y ) ) <-> ( ( F ` ( G ` X ) ) .c_ Y <-> ( G ` X ) .<_ ( G ` Y ) ) ) )
25 fveq2
 |-  ( x = ( G ` X ) -> ( F ` x ) = ( F ` ( G ` X ) ) )
26 25 breq1d
 |-  ( x = ( G ` X ) -> ( ( F ` x ) .c_ y <-> ( F ` ( G ` X ) ) .c_ y ) )
27 breq1
 |-  ( x = ( G ` X ) -> ( x .<_ ( G ` y ) <-> ( G ` X ) .<_ ( G ` y ) ) )
28 26 27 bibi12d
 |-  ( x = ( G ` X ) -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` ( G ` X ) ) .c_ y <-> ( G ` X ) .<_ ( G ` y ) ) ) )
29 28 ralbidv
 |-  ( x = ( G ` X ) -> ( A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> A. y e. B ( ( F ` ( G ` X ) ) .c_ y <-> ( G ` X ) .<_ ( G ` y ) ) ) )
30 13 simprd
 |-  ( ph -> A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) )
31 29 30 16 rspcdva
 |-  ( ph -> A. y e. B ( ( F ` ( G ` X ) ) .c_ y <-> ( G ` X ) .<_ ( G ` y ) ) )
32 24 31 10 rspcdva
 |-  ( ph -> ( ( F ` ( G ` X ) ) .c_ Y <-> ( G ` X ) .<_ ( G ` Y ) ) )
33 20 32 mpbid
 |-  ( ph -> ( G ` X ) .<_ ( G ` Y ) )