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 = {Base}_{V}$
	mgcoval.2	$⊢ B = {Base}_{W}$
	mgcoval.3	$⊢ \underset{˙}{\leq} = \leq_{V}$
	mgcoval.4	No typesetting found for \|- .c_ = ( le ` W ) with typecode \|-
	mgcval.1	$⊢ H = V MGalConn W$
	mgcval.2	$⊢ φ \to V \in Proset$
	mgcval.3	$⊢ φ \to W \in Proset$
	mgccole.1	$⊢ φ \to F H G$
	mgcmnt2.1	$⊢ φ \to X \in B$
	mgcmnt2.2	$⊢ φ \to Y \in B$
	mgcmnt2.3	No typesetting found for \|- ( ph -> X .c_ Y ) with typecode \|-
Assertion	mgcmnt2	$⊢ φ \to G (X) \underset{˙}{\leq} G (Y)$

Proof

Step	Hyp	Ref	Expression
1		mgcoval.1	$⊢ A = {Base}_{V}$
2		mgcoval.2	$⊢ B = {Base}_{W}$
3		mgcoval.3	$⊢ \underset{˙}{\leq} = \leq_{V}$
4		mgcoval.4	Could not format .c_ = ( le ` W ) : No typesetting found for \|- .c_ = ( le ` W ) with typecode \|-
5		mgcval.1	$⊢ H = V MGalConn W$
6		mgcval.2	$⊢ φ \to V \in Proset$
7		mgcval.3	$⊢ φ \to W \in Proset$
8		mgccole.1	$⊢ φ \to F H G$
9		mgcmnt2.1	$⊢ φ \to X \in B$
10		mgcmnt2.2	$⊢ φ \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	$⊢ φ \to F : A ⟶ B$
15	13	simplrd	$⊢ φ \to G : B ⟶ A$
16	15 9	ffvelcdmd	$⊢ φ \to G (X) \in A$
17	14 16	ffvelcdmd	$⊢ φ \to F (G (X)) \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 (y) = G (Y)$
23	22	breq2d	$⊢ y = Y \to (G (X) \underset{˙}{\leq} G (y) \leftrightarrow G (X) \underset{˙}{\leq} G (Y))$
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 (X) \to F (x) = F (G (X))$
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 (X) \to (x \underset{˙}{\leq} G (y) \leftrightarrow G (X) \underset{˙}{\leq} G (y))$
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	$⊢ φ \to G (X) \underset{˙}{\leq} G (Y)$

Metamath Proof Explorer

Theorem mgcmnt2

Proof