Theorem mgcmnt1d

Description: Galois connection implies monotonicity of the left 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	mgcmnt1d	Could not format assertion : No typesetting found for |- ( ph -> F e. ( V Monot W ) ) 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	mgcf1	$$⊢\phi \to F:{\mathrm{Base}}_V⟶{\mathrm{Base}}_W$$
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	simpld	$$⊢\phi \to \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)$$
14	5 6 7 8	ismnt	Could not format ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) with typecode |-
15	14	biimpar	Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
16	2 3 9 13 15	syl22anc	Could not format ( ph -> F e. ( V Monot W ) ) : No typesetting found for |- ( ph -> F e. ( V Monot W ) ) with typecode |-