Metamath Proof Explorer

Theorem mgcmnt2d

Description: Galois connection implies monotonicity of the right 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	mgcmnt2d	\|- ( ph -> G e. ( W Monot V ) )

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	mgcf2	\|- ( ph -> G : ( Base ` W ) --> ( Base ` V ) )
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	simprd	\|- ( ph -> A. u e. ( Base ` W ) A. v e. ( Base ` W ) ( u ( le ` W ) v -> ( G ` u ) ( le ` V ) ( G ` v ) ) )
14	6 5 8 7	ismnt	\|- ( ( W e. Proset /\ V e. Proset ) -> ( G e. ( W Monot V ) <-> ( G : ( Base ` W ) --> ( Base ` V ) /\ A. u e. ( Base ` W ) A. v e. ( Base ` W ) ( u ( le ` W ) v -> ( G ` u ) ( le ` V ) ( G ` v ) ) ) ) )
15	14	biimpar	\|- ( ( ( W e. Proset /\ V e. Proset ) /\ ( G : ( Base ` W ) --> ( Base ` V ) /\ A. u e. ( Base ` W ) A. v e. ( Base ` W ) ( u ( le ` W ) v -> ( G ` u ) ( le ` V ) ( G ` v ) ) ) ) -> G e. ( W Monot V ) )
16	3 2 9 13 15	syl22anc	\|- ( ph -> G e. ( W Monot V ) )