Theorem mgcmnt2

Description: The upper adjoint G of a Galois connection is monotonically increasing. (Contributed by Thierry Arnoux, 26-Apr-2024)

	Ref	Expression
Hypotheses	mgcoval.1	$$⊢A={\mathrm{Base}}_V$$
	mgcoval.2	$$⊢B={\mathrm{Base}}_W$$
	mgcoval.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
	mgcoval.4	No typesetting found for |- .c_ = ( le ` W ) with typecode |-
	mgcval.1	No typesetting found for |- H = ( V MGalConn W ) with typecode |-
	mgcval.2	$$⊢\phi \to V\in \mathrm{Proset}$$
	mgcval.3	$$⊢\phi \to W\in \mathrm{Proset}$$
	mgccole.1	$$⊢\phi \to FHG$$
	mgcmnt2.1	$$⊢\phi \to X\in B$$
	mgcmnt2.2	$$⊢\phi \to Y\in B$$
	mgcmnt2.3	No typesetting found for |- ( ph -> X .c_ Y ) with typecode |-
Assertion	mgcmnt2	$$⊢\phi \to G\left(X\right)\underset{\dot{}}{\le }G\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		mgcoval.1	$$⊢A={\mathrm{Base}}_V$$
2		mgcoval.2	$$⊢B={\mathrm{Base}}_W$$
3		mgcoval.3	$$⊢\underset{\dot{}}{\le }={\le }_V$$
4		mgcoval.4	Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
5		mgcval.1	Could not format H = ( V MGalConn W ) : No typesetting found for |- H = ( V MGalConn W ) with typecode |-
6		mgcval.2	$$⊢\phi \to V\in \mathrm{Proset}$$
7		mgcval.3	$$⊢\phi \to W\in \mathrm{Proset}$$
8		mgccole.1	$$⊢\phi \to FHG$$
9		mgcmnt2.1	$$⊢\phi \to X\in B$$
10		mgcmnt2.2	$$⊢\phi \to Y\in B$$
11		mgcmnt2.3	Could not format ( ph -> X .c_ Y ) : No typesetting found for |- ( ph -> X .c_ Y ) with typecode |-
12	1 2 3 4 5 6 7	mgcval	Could not format ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) ) : No typesetting found for |- ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) ) with typecode |-
13	8 12	mpbid	Could not format ( ph -> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( ph -> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) ) with typecode |-
14	13	simplld	$$⊢\phi \to F:A⟶B$$
15	13	simplrd	$$⊢\phi \to G:B⟶A$$
16	15 9	ffvelrnd	$$⊢\phi \to G\left(X\right)\in A$$
17	14 16	ffvelrnd	$$⊢\phi \to F\left(G\left(X\right)\right)\in B$$
18	1 2 3 4 5 6 7 8 9	mgccole2	Could not format ( ph -> ( F ` ( G ` X ) ) .c_ X ) : No typesetting found for |- ( ph -> ( F ` ( G ` X ) ) .c_ X ) with typecode |-
19	2 4	prstr	Could not format ( ( W e. Proset /\ ( ( F ` ( G ` X ) ) e. B /\ X e. B /\ Y e. B ) /\ ( ( F ` ( G ` X ) ) .c_ X /\ X .c_ Y ) ) -> ( F ` ( G ` X ) ) .c_ Y ) : No typesetting found for |- ( ( W e. Proset /\ ( ( F ` ( G ` X ) ) e. B /\ X e. B /\ Y e. B ) /\ ( ( F ` ( G ` X ) ) .c_ X /\ X .c_ Y ) ) -> ( F ` ( G ` X ) ) .c_ Y ) with typecode |-
20	7 17 9 10 18 11 19	syl132anc	Could not format ( ph -> ( F ` ( G ` X ) ) .c_ Y ) : No typesetting found for |- ( ph -> ( F ` ( G ` X ) ) .c_ Y ) with typecode |-
21		breq2	Could not format ( y = Y -> ( ( F ` ( G ` X ) ) .c_ y <-> ( F ` ( G ` X ) ) .c_ Y ) ) : No typesetting found for |- ( y = Y -> ( ( F ` ( G ` X ) ) .c_ y <-> ( F ` ( G ` X ) ) .c_ Y ) ) with typecode |-
22		fveq2	$$⊢y=Y\to G\left(y\right)=G\left(Y\right)$$
23	22	breq2d	$$⊢y=Y\to \left(G\left(X\right)\underset{\dot{}}{\le }G\left(y\right)\leftrightarrow G\left(X\right)\underset{\dot{}}{\le }G\left(Y\right)\right)$$
24	21 23	bibi12d	Could not format ( y = Y -> ( ( ( F ` ( G ` X ) ) .c_ y <-> ( G ` X ) .<_ ( G ` y ) ) <-> ( ( F ` ( G ` X ) ) .c_ Y <-> ( G ` X ) .<_ ( G ` Y ) ) ) ) : No typesetting found for |- ( y = Y -> ( ( ( F ` ( G ` X ) ) .c_ y <-> ( G ` X ) .<_ ( G ` y ) ) <-> ( ( F ` ( G ` X ) ) .c_ Y <-> ( G ` X ) .<_ ( G ` Y ) ) ) ) with typecode |-
25		fveq2	$$⊢x=G\left(X\right)\to F\left(x\right)=F\left(G\left(X\right)\right)$$
26	25	breq1d	Could not format ( x = ( G ` X ) -> ( ( F ` x ) .c_ y <-> ( F ` ( G ` X ) ) .c_ y ) ) : No typesetting found for |- ( x = ( G ` X ) -> ( ( F ` x ) .c_ y <-> ( F ` ( G ` X ) ) .c_ y ) ) with typecode |-
27		breq1	$$⊢x=G\left(X\right)\to \left(x\underset{\dot{}}{\le }G\left(y\right)\leftrightarrow G\left(X\right)\underset{\dot{}}{\le }G\left(y\right)\right)$$
28	26 27	bibi12d	Could not format ( x = ( G ` X ) -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` ( G ` X ) ) .c_ y <-> ( G ` X ) .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( x = ( G ` X ) -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` ( G ` X ) ) .c_ y <-> ( G ` X ) .<_ ( G ` y ) ) ) ) with typecode |-
29	28	ralbidv	Could not format ( x = ( G ` X ) -> ( A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> A. y e. B ( ( F ` ( G ` X ) ) .c_ y <-> ( G ` X ) .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( x = ( G ` X ) -> ( A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> A. y e. B ( ( F ` ( G ` X ) ) .c_ y <-> ( G ` X ) .<_ ( G ` y ) ) ) ) with typecode |-
30	13	simprd	Could not format ( ph -> A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) : No typesetting found for |- ( ph -> A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) with typecode |-
31	29 30 16	rspcdva	Could not format ( ph -> A. y e. B ( ( F ` ( G ` X ) ) .c_ y <-> ( G ` X ) .<_ ( G ` y ) ) ) : No typesetting found for |- ( ph -> A. y e. B ( ( F ` ( G ` X ) ) .c_ y <-> ( G ` X ) .<_ ( G ` y ) ) ) with typecode |-
32	24 31 10	rspcdva	Could not format ( ph -> ( ( F ` ( G ` X ) ) .c_ Y <-> ( G ` X ) .<_ ( G ` Y ) ) ) : No typesetting found for |- ( ph -> ( ( F ` ( G ` X ) ) .c_ Y <-> ( G ` X ) .<_ ( G ` Y ) ) ) with typecode |-
33	20 32	mpbid	$$⊢\phi \to G\left(X\right)\underset{\dot{}}{\le }G\left(Y\right)$$