Theorem mgcmnt1

Description: The lower adjoint F 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$$
	mgcmnt1.1	$$⊢\phi \to X\in A$$
	mgcmnt1.2	$$⊢\phi \to Y\in A$$
	mgcmnt1.3	$$⊢\phi \to X\underset{\dot{}}{\le }Y$$
Assertion	mgcmnt1	Could not format assertion : No typesetting found for |- ( ph -> ( F ` X ) .c_ ( F ` Y ) ) with typecode |-

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		mgcmnt1.1	$$⊢\phi \to X\in A$$
10		mgcmnt1.2	$$⊢\phi \to Y\in A$$
11		mgcmnt1.3	$$⊢\phi \to X\underset{\dot{}}{\le }Y$$
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	simplrd	$$⊢\phi \to G:B⟶A$$
15	13	simplld	$$⊢\phi \to F:A⟶B$$
16	15 10	ffvelcdmd	$$⊢\phi \to F\left(Y\right)\in B$$
17	14 16	ffvelcdmd	$$⊢\phi \to G\left(F\left(Y\right)\right)\in A$$
18	1 2 3 4 5 6 7 8 10	mgccole1	$$⊢\phi \to Y\underset{\dot{}}{\le }G\left(F\left(Y\right)\right)$$
19	1 3	prstr	$$⊢\left(V\in \mathrm{Proset}\wedge \left(X\in A\wedge Y\in A\wedge G\left(F\left(Y\right)\right)\in A\right)\wedge \left(X\underset{\dot{}}{\le }Y\wedge Y\underset{\dot{}}{\le }G\left(F\left(Y\right)\right)\right)\right)\to X\underset{\dot{}}{\le }G\left(F\left(Y\right)\right)$$
20	6 9 10 17 11 18 19	syl132anc	$$⊢\phi \to X\underset{\dot{}}{\le }G\left(F\left(Y\right)\right)$$
21	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 |-
22		fveq2	$$⊢x=X\to F\left(x\right)=F\left(X\right)$$
23	22	breq1d	Could not format ( x = X -> ( ( F ` x ) .c_ y <-> ( F ` X ) .c_ y ) ) : No typesetting found for |- ( x = X -> ( ( F ` x ) .c_ y <-> ( F ` X ) .c_ y ) ) with typecode |-
24		breq1	$$⊢x=X\to \left(x\underset{\dot{}}{\le }G\left(y\right)\leftrightarrow X\underset{\dot{}}{\le }G\left(y\right)\right)$$
25	23 24	bibi12d	Could not format ( x = X -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( x = X -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) ) with typecode |-
26	25	adantl	Could not format ( ( ph /\ x = X ) -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( ( ph /\ x = X ) -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) ) with typecode |-
27	26	ralbidv	Could not format ( ( ph /\ x = X ) -> ( A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) ) : No typesetting found for |- ( ( ph /\ x = X ) -> ( A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) ) with typecode |-
28	9 27	rspcdv	Could not format ( ph -> ( A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) -> 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 ) ) -> A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) ) with typecode |-
29	21 28	mpd	Could not format ( ph -> A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) : No typesetting found for |- ( ph -> A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) with typecode |-
30		simpr	$$⊢\left(\phi \wedge y=F\left(Y\right)\right)\to y=F\left(Y\right)$$
31	30	breq2d	Could not format ( ( ph /\ y = ( F ` Y ) ) -> ( ( F ` X ) .c_ y <-> ( F ` X ) .c_ ( F ` Y ) ) ) : No typesetting found for |- ( ( ph /\ y = ( F ` Y ) ) -> ( ( F ` X ) .c_ y <-> ( F ` X ) .c_ ( F ` Y ) ) ) with typecode |-
32	30	fveq2d	$$⊢\left(\phi \wedge y=F\left(Y\right)\right)\to G\left(y\right)=G\left(F\left(Y\right)\right)$$
33	32	breq2d	$$⊢\left(\phi \wedge y=F\left(Y\right)\right)\to \left(X\underset{\dot{}}{\le }G\left(y\right)\leftrightarrow X\underset{\dot{}}{\le }G\left(F\left(Y\right)\right)\right)$$
34	31 33	bibi12d	Could not format ( ( ph /\ y = ( F ` Y ) ) -> ( ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) <-> ( ( F ` X ) .c_ ( F ` Y ) <-> X .<_ ( G ` ( F ` Y ) ) ) ) ) : No typesetting found for |- ( ( ph /\ y = ( F ` Y ) ) -> ( ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) <-> ( ( F ` X ) .c_ ( F ` Y ) <-> X .<_ ( G ` ( F ` Y ) ) ) ) ) with typecode |-
35	16 34	rspcdv	Could not format ( ph -> ( A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) -> ( ( F ` X ) .c_ ( F ` Y ) <-> X .<_ ( G ` ( F ` Y ) ) ) ) ) : No typesetting found for |- ( ph -> ( A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) -> ( ( F ` X ) .c_ ( F ` Y ) <-> X .<_ ( G ` ( F ` Y ) ) ) ) ) with typecode |-
36	29 35	mpd	Could not format ( ph -> ( ( F ` X ) .c_ ( F ` Y ) <-> X .<_ ( G ` ( F ` Y ) ) ) ) : No typesetting found for |- ( ph -> ( ( F ` X ) .c_ ( F ` Y ) <-> X .<_ ( G ` ( F ` Y ) ) ) ) with typecode |-
37	20 36	mpbird	Could not format ( ph -> ( F ` X ) .c_ ( F ` Y ) ) : No typesetting found for |- ( ph -> ( F ` X ) .c_ ( F ` Y ) ) with typecode |-