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

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 
|- ( ph -> V e. Proset )
mgcmntd.3 
|- ( ph -> W e. Proset )
mgcmntd.4 
|- ( ph -> F H G )
Assertion mgcmnt1d 
|- ( ph -> F e. ( V Monot W ) )

Proof

Step Hyp Ref Expression
1 mgcmntd.1 
 |-  H = ( V MGalConn W )
2 mgcmntd.2 
 |-  ( ph -> V e. Proset )
3 mgcmntd.3 
 |-  ( ph -> W e. Proset )
4 mgcmntd.4 
 |-  ( ph -> F H G )
5 eqid 
 |-  ( Base ` V ) = ( Base ` V )
6 eqid 
 |-  ( Base ` W ) = ( Base ` W )
7 eqid 
 |-  ( le ` V ) = ( le ` V )
8 eqid 
 |-  ( le ` W ) = ( le ` W )
9 5 6 7 8 1 2 3 4 mgcf1 
 |-  ( ph -> F : ( Base ` V ) --> ( Base ` W ) )
10 5 6 7 8 1 2 3 dfmgc2 
 |-  ( ph -> ( F H G <-> ( ( F : ( Base ` V ) --> ( Base ` W ) /\ G : ( Base ` W ) --> ( Base ` V ) ) /\ ( ( A. x e. ( Base ` V ) A. y e. ( Base ` V ) ( x ( le ` V ) y -> ( F ` x ) ( le ` W ) ( F ` y ) ) /\ A. u e. ( Base ` W ) A. v e. ( Base ` W ) ( u ( le ` W ) v -> ( G ` u ) ( le ` V ) ( G ` v ) ) ) /\ ( A. u e. ( Base ` W ) ( F ` ( G ` u ) ) ( le ` W ) u /\ A. x e. ( Base ` V ) x ( le ` V ) ( G ` ( F ` x ) ) ) ) ) ) )
11 4 10 mpbid 
 |-  ( ph -> ( ( F : ( Base ` V ) --> ( Base ` W ) /\ G : ( Base ` W ) --> ( Base ` V ) ) /\ ( ( A. x e. ( Base ` V ) A. y e. ( Base ` V ) ( x ( le ` V ) y -> ( F ` x ) ( le ` W ) ( F ` y ) ) /\ A. u e. ( Base ` W ) A. v e. ( Base ` W ) ( u ( le ` W ) v -> ( G ` u ) ( le ` V ) ( G ` v ) ) ) /\ ( A. u e. ( Base ` W ) ( F ` ( G ` u ) ) ( le ` W ) u /\ A. x e. ( Base ` V ) x ( le ` V ) ( G ` ( F ` x ) ) ) ) ) )
12 11 simprld 
 |-  ( ph -> ( A. x e. ( Base ` V ) A. y e. ( Base ` V ) ( x ( le ` V ) y -> ( F ` x ) ( le ` W ) ( F ` y ) ) /\ A. u e. ( Base ` W ) A. v e. ( Base ` W ) ( u ( le ` W ) v -> ( G ` u ) ( le ` V ) ( G ` v ) ) ) )
13 12 simpld 
 |-  ( ph -> A. x e. ( Base ` V ) A. y e. ( Base ` V ) ( x ( le ` V ) y -> ( F ` x ) ( le ` W ) ( F ` y ) ) )
14 5 6 7 8 ismnt 
 |-  ( ( V e. Proset /\ W e. Proset ) -> ( F e. ( V Monot W ) <-> ( F : ( Base ` V ) --> ( Base ` W ) /\ A. x e. ( Base ` V ) A. y e. ( Base ` V ) ( x ( le ` V ) y -> ( F ` x ) ( le ` W ) ( F ` y ) ) ) ) )
15 14 biimpar 
 |-  ( ( ( V e. Proset /\ W e. Proset ) /\ ( F : ( Base ` V ) --> ( Base ` W ) /\ A. x e. ( Base ` V ) A. y e. ( Base ` V ) ( x ( le ` V ) y -> ( F ` x ) ( le ` W ) ( F ` y ) ) ) ) -> F e. ( V Monot W ) )
16 2 3 9 13 15 syl22anc 
 |-  ( ph -> F e. ( V Monot W ) )