Theorem mgcmnt2d

Description: Galois connection implies monotonicity of the right adjoint. (Contributed by Thierry Arnoux, 21-Jul-2024)

	Ref	Expression
Hypotheses	mgcmntd.1	No typesetting found for |- H = ( V MGalConn W ) with typecode |-
	mgcmntd.2	$$⊢\phi \to V\in \mathrm{Proset}$$
	mgcmntd.3	$$⊢\phi \to W\in \mathrm{Proset}$$
	mgcmntd.4	$$⊢\phi \to FHG$$
Assertion	mgcmnt2d	Could not format assertion : No typesetting found for |- ( ph -> G e. ( W Monot V ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		mgcmntd.1	Could not format H = ( V MGalConn W ) : No typesetting found for |- H = ( V MGalConn W ) with typecode |-
2		mgcmntd.2	$$⊢\phi \to V\in \mathrm{Proset}$$
3		mgcmntd.3	$$⊢\phi \to W\in \mathrm{Proset}$$
4		mgcmntd.4	$$⊢\phi \to FHG$$
5		eqid	$$⊢{\mathrm{Base}}_V={\mathrm{Base}}_V$$
6		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
7		eqid	$$⊢{\le }_V={\le }_V$$
8		eqid	$$⊢{\le }_W={\le }_W$$
9	5 6 7 8 1 2 3 4	mgcf2	$$⊢\phi \to G:{\mathrm{Base}}_W⟶{\mathrm{Base}}_V$$
10	5 6 7 8 1 2 3	dfmgc2	$$⊢\phi \to \left(FHG\leftrightarrow \left(\left(F:{\mathrm{Base}}_V⟶{\mathrm{Base}}_W\wedge G:{\mathrm{Base}}_W⟶{\mathrm{Base}}_V\right)\wedge \left(\left(\forall x\in {\mathrm{Base}}_V\forall y\in {\mathrm{Base}}_V\left(x{\le }_{V}y\to F\left(x\right){\le }_{W}F\left(y\right)\right)\wedge \forall u\in {\mathrm{Base}}_W\forall v\in {\mathrm{Base}}_W\left(u{\le }_{W}v\to G\left(u\right){\le }_{V}G\left(v\right)\right)\right)\wedge \left(\forall u\in {\mathrm{Base}}_{W}F\left(G\left(u\right)\right){\le }_{W}u\wedge \forall x\in {\mathrm{Base}}_{V}x{\le }_{V}G\left(F\left(x\right)\right)\right)\right)\right)\right)$$
11	4 10	mpbid	$$⊢\phi \to \left(\left(F:{\mathrm{Base}}_V⟶{\mathrm{Base}}_W\wedge G:{\mathrm{Base}}_W⟶{\mathrm{Base}}_V\right)\wedge \left(\left(\forall x\in {\mathrm{Base}}_V\forall y\in {\mathrm{Base}}_V\left(x{\le }_{V}y\to F\left(x\right){\le }_{W}F\left(y\right)\right)\wedge \forall u\in {\mathrm{Base}}_W\forall v\in {\mathrm{Base}}_W\left(u{\le }_{W}v\to G\left(u\right){\le }_{V}G\left(v\right)\right)\right)\wedge \left(\forall u\in {\mathrm{Base}}_{W}F\left(G\left(u\right)\right){\le }_{W}u\wedge \forall x\in {\mathrm{Base}}_{V}x{\le }_{V}G\left(F\left(x\right)\right)\right)\right)\right)$$
12	11	simprld	$$⊢\phi \to \left(\forall x\in {\mathrm{Base}}_V\forall y\in {\mathrm{Base}}_V\left(x{\le }_{V}y\to F\left(x\right){\le }_{W}F\left(y\right)\right)\wedge \forall u\in {\mathrm{Base}}_W\forall v\in {\mathrm{Base}}_W\left(u{\le }_{W}v\to G\left(u\right){\le }_{V}G\left(v\right)\right)\right)$$
13	12	simprd	$$⊢\phi \to \forall u\in {\mathrm{Base}}_W\forall v\in {\mathrm{Base}}_W\left(u{\le }_{W}v\to G\left(u\right){\le }_{V}G\left(v\right)\right)$$
14	6 5 8 7	ismnt	Could not format ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) with typecode |-
15	14	biimpar	Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
16	3 2 9 13 15	syl22anc	Could not format ( ph -> G e. ( W Monot V ) ) : No typesetting found for |- ( ph -> G e. ( W Monot V ) ) with typecode |-