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 = {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$
	mgcmnt1.1	$⊢ φ \to X \in A$
	mgcmnt1.2	$⊢ φ \to Y \in A$
	mgcmnt1.3	$⊢ φ \to X \underset{˙}{\leq} 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 = {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		mgcmnt1.1	$⊢ φ \to X \in A$
10		mgcmnt1.2	$⊢ φ \to Y \in A$
11		mgcmnt1.3	$⊢ φ \to X \underset{˙}{\leq} 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	$⊢ φ \to G : B ⟶ A$
15	13	simplld	$⊢ φ \to F : A ⟶ B$
16	15 10	ffvelcdmd	$⊢ φ \to F (Y) \in B$
17	14 16	ffvelcdmd	$⊢ φ \to G (F (Y)) \in A$
18	1 2 3 4 5 6 7 8 10	mgccole1	$⊢ φ \to Y \underset{˙}{\leq} G (F (Y))$
19	1 3	prstr	$⊢ (V \in Proset \land (X \in A \land Y \in A \land G (F (Y)) \in A) \land (X \underset{˙}{\leq} Y \land Y \underset{˙}{\leq} G (F (Y)))) \to X \underset{˙}{\leq} G (F (Y))$
20	6 9 10 17 11 18 19	syl132anc	$⊢ φ \to X \underset{˙}{\leq} G (F (Y))$
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 (x) = F (X)$
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 (x \underset{˙}{\leq} G (y) \leftrightarrow X \underset{˙}{\leq} G (y))$
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	$⊢ (φ \land y = F (Y)) \to y = F (Y)$
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	$⊢ (φ \land y = F (Y)) \to G (y) = G (F (Y))$
33	32	breq2d	$⊢ (φ \land y = F (Y)) \to (X \underset{˙}{\leq} G (y) \leftrightarrow X \underset{˙}{\leq} G (F (Y)))$
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 \|-

Metamath Proof Explorer

Theorem mgcmnt1

Proof