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 ) )