This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- 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 )
mgcmnt1.1 
|- ( ph -> X e. A )
mgcmnt1.2 
|- ( ph -> Y e. A )
mgcmnt1.3 
|- ( ph -> X .<_ Y )
Assertion mgcmnt1 
|- ( ph -> ( F ` X ) .c_ ( F ` 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 mgcmnt1.1 
 |-  ( ph -> X e. A )
10 mgcmnt1.2 
 |-  ( ph -> Y e. A )
11 mgcmnt1.3 
 |-  ( ph -> X .<_ 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 simplrd 
 |-  ( ph -> G : B --> A )
15 13 simplld 
 |-  ( ph -> F : A --> B )
16 15 10 ffvelcdmd 
 |-  ( ph -> ( F ` Y ) e. B )
17 14 16 ffvelcdmd 
 |-  ( ph -> ( G ` ( F ` Y ) ) e. A )
18 1 2 3 4 5 6 7 8 10 mgccole1 
 |-  ( ph -> Y .<_ ( G ` ( F ` Y ) ) )
19 1 3 prstr 
 |-  ( ( V e. Proset /\ ( X e. A /\ Y e. A /\ ( G ` ( F ` Y ) ) e. A ) /\ ( X .<_ Y /\ Y .<_ ( G ` ( F ` Y ) ) ) ) -> X .<_ ( G ` ( F ` Y ) ) )
20 6 9 10 17 11 18 19 syl132anc 
 |-  ( ph -> X .<_ ( G ` ( F ` Y ) ) )
21 13 simprd 
 |-  ( ph -> A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) )
22 fveq2 
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
23 22 breq1d 
 |-  ( x = X -> ( ( F ` x ) .c_ y <-> ( F ` X ) .c_ y ) )
24 breq1 
 |-  ( x = X -> ( x .<_ ( G ` y ) <-> X .<_ ( G ` y ) ) )
25 23 24 bibi12d 
 |-  ( x = X -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) )
26 25 adantl 
 |-  ( ( ph /\ x = X ) -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) )
27 26 ralbidv 
 |-  ( ( ph /\ x = X ) -> ( A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) )
28 9 27 rspcdv 
 |-  ( ph -> ( A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) -> A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) )
29 21 28 mpd 
 |-  ( ph -> A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) )
30 simpr 
 |-  ( ( ph /\ y = ( F ` Y ) ) -> y = ( F ` Y ) )
31 30 breq2d 
 |-  ( ( ph /\ y = ( F ` Y ) ) -> ( ( F ` X ) .c_ y <-> ( F ` X ) .c_ ( F ` Y ) ) )
32 30 fveq2d 
 |-  ( ( ph /\ y = ( F ` Y ) ) -> ( G ` y ) = ( G ` ( F ` Y ) ) )
33 32 breq2d 
 |-  ( ( ph /\ y = ( F ` Y ) ) -> ( X .<_ ( G ` y ) <-> X .<_ ( G ` ( F ` Y ) ) ) )
34 31 33 bibi12d 
 |-  ( ( ph /\ y = ( F ` Y ) ) -> ( ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) <-> ( ( F ` X ) .c_ ( F ` Y ) <-> X .<_ ( G ` ( F ` Y ) ) ) ) )
35 16 34 rspcdv 
 |-  ( ph -> ( A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) -> ( ( F ` X ) .c_ ( F ` Y ) <-> X .<_ ( G ` ( F ` Y ) ) ) ) )
36 29 35 mpd 
 |-  ( ph -> ( ( F ` X ) .c_ ( F ` Y ) <-> X .<_ ( G ` ( F ` Y ) ) ) )
37 20 36 mpbird 
 |-  ( ph -> ( F ` X ) .c_ ( F ` Y ) )