mgccole2

Description: Inequality for the closure operator ( F o. G ) of the Galois connection H . (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$
	mgccole2.1	$⊢ φ \to Y \in B$
Assertion	mgccole2	Could not format assertion : No typesetting found for \|- ( ph -> ( F ` ( G ` Y ) ) .c_ 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		mgccole2.1	$⊢ φ \to Y \in B$
10	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 \|-
11	8 10	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 \|-
12	11	simplrd	$⊢ φ \to G : B ⟶ A$
13	12 9	ffvelcdmd	$⊢ φ \to G (Y) \in A$
14	1 3	prsref	$⊢ (V \in Proset \land G (Y) \in A) \to G (Y) \underset{˙}{\leq} G (Y)$
15	6 13 14	syl2anc	$⊢ φ \to G (Y) \underset{˙}{\leq} G (Y)$
16	11	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 \|-
17		fveq2	$⊢ x = G (Y) \to F (x) = F (G (Y))$
18	17	breq1d	Could not format ( x = ( G ` Y ) -> ( ( F ` x ) .c_ y <-> ( F ` ( G ` Y ) ) .c_ y ) ) : No typesetting found for \|- ( x = ( G ` Y ) -> ( ( F ` x ) .c_ y <-> ( F ` ( G ` Y ) ) .c_ y ) ) with typecode \|-
19		breq1	$⊢ x = G (Y) \to (x \underset{˙}{\leq} G (y) \leftrightarrow G (Y) \underset{˙}{\leq} G (y))$
20	18 19	bibi12d	Could not format ( x = ( G ` Y ) -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) ) ) : No typesetting found for \|- ( x = ( G ` Y ) -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) ) ) with typecode \|-
21	20	adantl	Could not format ( ( ph /\ x = ( G ` Y ) ) -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) ) ) : No typesetting found for \|- ( ( ph /\ x = ( G ` Y ) ) -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) ) ) with typecode \|-
22	21	ralbidv	Could not format ( ( ph /\ x = ( G ` Y ) ) -> ( A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> A. y e. B ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) ) ) : No typesetting found for \|- ( ( ph /\ x = ( G ` Y ) ) -> ( A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> A. y e. B ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) ) ) with typecode \|-
23	13 22	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 ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( 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 ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) ) ) with typecode \|-
24	16 23	mpd	Could not format ( ph -> A. y e. B ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) ) : No typesetting found for \|- ( ph -> A. y e. B ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) ) with typecode \|-
25		simpr	$⊢ (φ \land y = Y) \to y = Y$
26	25	breq2d	Could not format ( ( ph /\ y = Y ) -> ( ( F ` ( G ` Y ) ) .c_ y <-> ( F ` ( G ` Y ) ) .c_ Y ) ) : No typesetting found for \|- ( ( ph /\ y = Y ) -> ( ( F ` ( G ` Y ) ) .c_ y <-> ( F ` ( G ` Y ) ) .c_ Y ) ) with typecode \|-
27		fveq2	$⊢ y = Y \to G (y) = G (Y)$
28	27	adantl	$⊢ (φ \land y = Y) \to G (y) = G (Y)$
29	28	breq2d	$⊢ (φ \land y = Y) \to (G (Y) \underset{˙}{\leq} G (y) \leftrightarrow G (Y) \underset{˙}{\leq} G (Y))$
30	26 29	bibi12d	Could not format ( ( ph /\ y = Y ) -> ( ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) <-> ( ( F ` ( G ` Y ) ) .c_ Y <-> ( G ` Y ) .<_ ( G ` Y ) ) ) ) : No typesetting found for \|- ( ( ph /\ y = Y ) -> ( ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) <-> ( ( F ` ( G ` Y ) ) .c_ Y <-> ( G ` Y ) .<_ ( G ` Y ) ) ) ) with typecode \|-
31	9 30	rspcdv	Could not format ( ph -> ( A. y e. B ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) -> ( ( F ` ( G ` Y ) ) .c_ Y <-> ( G ` Y ) .<_ ( G ` Y ) ) ) ) : No typesetting found for \|- ( ph -> ( A. y e. B ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) -> ( ( F ` ( G ` Y ) ) .c_ Y <-> ( G ` Y ) .<_ ( G ` Y ) ) ) ) with typecode \|-
32	24 31	mpd	Could not format ( ph -> ( ( F ` ( G ` Y ) ) .c_ Y <-> ( G ` Y ) .<_ ( G ` Y ) ) ) : No typesetting found for \|- ( ph -> ( ( F ` ( G ` Y ) ) .c_ Y <-> ( G ` Y ) .<_ ( G ` Y ) ) ) with typecode \|-
33	15 32	mpbird	Could not format ( ph -> ( F ` ( G ` Y ) ) .c_ Y ) : No typesetting found for \|- ( ph -> ( F ` ( G ` Y ) ) .c_ Y ) with typecode \|-

Metamath Proof Explorer

Theorem mgccole2

Proof