Theorem mgccole1

Description: An inequality for the kernel operator G o. F . (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	$$⊢H=V\mathrm{MGalConn}W$$
	mgcval.2	$$⊢\phi \to V\in \mathrm{Proset}$$
	mgcval.3	$$⊢\phi \to W\in \mathrm{Proset}$$
	mgccole.1	$$⊢\phi \to FHG$$
	mgccole1.2	$$⊢\phi \to X\in A$$
Assertion	mgccole1	$$⊢\phi \to X\underset{\dot{}}{\le }G\left(F\left(X\right)\right)$$

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	$$⊢H=V\mathrm{MGalConn}W$$
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		mgccole1.2	$$⊢\phi \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	$$⊢\phi \to F:A⟶B$$
13	12 9	ffvelcdmd	$$⊢\phi \to F\left(X\right)\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\left(x\right)=F\left(X\right)$$
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 \left(x\underset{\dot{}}{\le }G\left(y\right)\leftrightarrow X\underset{\dot{}}{\le }G\left(y\right)\right)$$
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	$$⊢\left(\phi \wedge y=F\left(X\right)\right)\to y=F\left(X\right)$$
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	$$⊢\left(\phi \wedge y=F\left(X\right)\right)\to G\left(y\right)=G\left(F\left(X\right)\right)$$
26	25	breq2d	$$⊢\left(\phi \wedge y=F\left(X\right)\right)\to \left(X\underset{\dot{}}{\le }G\left(y\right)\leftrightarrow X\underset{\dot{}}{\le }G\left(F\left(X\right)\right)\right)$$
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	$$⊢\phi \to X\underset{\dot{}}{\le }G\left(F\left(X\right)\right)$$