mgccole1

Description: An inequality for the kernel operator G o. F . (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$
	mgccole1.2	$⊢ φ \to X \in A$
Assertion	mgccole1	$⊢ φ \to X \underset{˙}{\leq} G (F (X))$

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		mgccole1.2	$⊢ φ \to X \in A$
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	simplld	$⊢ φ \to F : A ⟶ B$
13	12 9	ffvelcdmd	$⊢ φ \to F (X) \in B$
14	2 4	prsref	Could not format ( ( W e. Proset /\ ( F ` X ) e. B ) -> ( F ` X ) .c_ ( F ` X ) ) : No typesetting found for \|- ( ( W e. Proset /\ ( F ` X ) e. B ) -> ( F ` X ) .c_ ( F ` X ) ) with typecode \|-
15	7 13 14	syl2anc	Could not format ( ph -> ( F ` X ) .c_ ( F ` X ) ) : No typesetting found for \|- ( ph -> ( F ` X ) .c_ ( F ` X ) ) with typecode \|-
16		fveq2	$⊢ x = X \to F (x) = F (X)$
17	16	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 \|-
18		breq1	$⊢ x = X \to (x \underset{˙}{\leq} G (y) \leftrightarrow X \underset{˙}{\leq} G (y))$
19	17 18	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 \|-
20	19	ralbidv	Could not format ( 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 \|- ( 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 \|-
21	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 \|-
22	20 21 9	rspcdva	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 \|-
23		simpr	$⊢ (φ \land y = F (X)) \to y = F (X)$
24	23	breq2d	Could not format ( ( ph /\ y = ( F ` X ) ) -> ( ( F ` X ) .c_ y <-> ( F ` X ) .c_ ( F ` X ) ) ) : No typesetting found for \|- ( ( ph /\ y = ( F ` X ) ) -> ( ( F ` X ) .c_ y <-> ( F ` X ) .c_ ( F ` X ) ) ) with typecode \|-
25	23	fveq2d	$⊢ (φ \land y = F (X)) \to G (y) = G (F (X))$
26	25	breq2d	$⊢ (φ \land y = F (X)) \to (X \underset{˙}{\leq} G (y) \leftrightarrow X \underset{˙}{\leq} G (F (X)))$
27	24 26	bibi12d	Could not format ( ( ph /\ y = ( F ` X ) ) -> ( ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) <-> ( ( F ` X ) .c_ ( F ` X ) <-> X .<_ ( G ` ( F ` X ) ) ) ) ) : No typesetting found for \|- ( ( ph /\ y = ( F ` X ) ) -> ( ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) <-> ( ( F ` X ) .c_ ( F ` X ) <-> X .<_ ( G ` ( F ` X ) ) ) ) ) with typecode \|-
28	13 27	rspcdv	Could not format ( ph -> ( A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) -> ( ( F ` X ) .c_ ( F ` X ) <-> X .<_ ( G ` ( F ` X ) ) ) ) ) : No typesetting found for \|- ( ph -> ( A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) -> ( ( F ` X ) .c_ ( F ` X ) <-> X .<_ ( G ` ( F ` X ) ) ) ) ) with typecode \|-
29	22 28	mpd	Could not format ( ph -> ( ( F ` X ) .c_ ( F ` X ) <-> X .<_ ( G ` ( F ` X ) ) ) ) : No typesetting found for \|- ( ph -> ( ( F ` X ) .c_ ( F ` X ) <-> X .<_ ( G ` ( F ` X ) ) ) ) with typecode \|-
30	15 29	mpbid	$⊢ φ \to X \underset{˙}{\leq} G (F (X))$

Metamath Proof Explorer

Theorem mgccole1

Proof