Theorem 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={\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$$
	mgccole2.1	$$⊢\phi \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={\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		mgccole2.1	$$⊢\phi \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	$$⊢\phi \to G:B⟶A$$
13	12 9	ffvelcdmd	$$⊢\phi \to G\left(Y\right)\in A$$
14	1 3	prsref	$$⊢\left(V\in \mathrm{Proset}\wedge G\left(Y\right)\in A\right)\to G\left(Y\right)\underset{\dot{}}{\le }G\left(Y\right)$$
15	6 13 14	syl2anc	$$⊢\phi \to G\left(Y\right)\underset{\dot{}}{\le }G\left(Y\right)$$
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\left(Y\right)\to F\left(x\right)=F\left(G\left(Y\right)\right)$$
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\left(Y\right)\to \left(x\underset{\dot{}}{\le }G\left(y\right)\leftrightarrow G\left(Y\right)\underset{\dot{}}{\le }G\left(y\right)\right)$$
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	$$⊢\left(\phi \wedge y=Y\right)\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\left(y\right)=G\left(Y\right)$$
28	27	adantl	$$⊢\left(\phi \wedge y=Y\right)\to G\left(y\right)=G\left(Y\right)$$
29	28	breq2d	$$⊢\left(\phi \wedge y=Y\right)\to \left(G\left(Y\right)\underset{\dot{}}{\le }G\left(y\right)\leftrightarrow G\left(Y\right)\underset{\dot{}}{\le }G\left(Y\right)\right)$$
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 |-