Theorem mgcf1olem2

Description: Property of a Galois connection, lemma for mgcf1o . (Contributed by Thierry Arnoux, 26-Jul-2024)

	Ref	Expression
Hypotheses	mgcf1o.h	$$⊢H=V\mathrm{MGalConn}W$$
	mgcf1o.a	$$⊢A={\mathrm{Base}}_V$$
	mgcf1o.b	$$⊢B={\mathrm{Base}}_W$$
	mgcf1o.1	$$⊢\underset{\dot{}}{\le }={\le }_V$$
	mgcf1o.2	No typesetting found for |- .c_ = ( le ` W ) with typecode |-
	mgcf1o.v	$$⊢\phi \to V\in \mathrm{Poset}$$
	mgcf1o.w	$$⊢\phi \to W\in \mathrm{Poset}$$
	mgcf1o.f	$$⊢\phi \to FHG$$
	mgcf1olem2.1	$$⊢\phi \to Y\in B$$
Assertion	mgcf1olem2	$$⊢\phi \to G\left(F\left(G\left(Y\right)\right)\right)=G\left(Y\right)$$

Proof

Step	Hyp	Ref	Expression
1		mgcf1o.h	$$⊢H=V\mathrm{MGalConn}W$$
2		mgcf1o.a	$$⊢A={\mathrm{Base}}_V$$
3		mgcf1o.b	$$⊢B={\mathrm{Base}}_W$$
4		mgcf1o.1	$$⊢\underset{\dot{}}{\le }={\le }_V$$
5		mgcf1o.2	Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
6		mgcf1o.v	$$⊢\phi \to V\in \mathrm{Poset}$$
7		mgcf1o.w	$$⊢\phi \to W\in \mathrm{Poset}$$
8		mgcf1o.f	$$⊢\phi \to FHG$$
9		mgcf1olem2.1	$$⊢\phi \to Y\in B$$
10		posprs	$$⊢V\in \mathrm{Poset}\to V\in \mathrm{Proset}$$
11	6 10	syl	$$⊢\phi \to V\in \mathrm{Proset}$$
12		posprs	$$⊢W\in \mathrm{Poset}\to W\in \mathrm{Proset}$$
13	7 12	syl	$$⊢\phi \to W\in \mathrm{Proset}$$
14	2 3 4 5 1 11 13	dfmgc2	Could not format ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) ) with typecode |-
15	8 14	mpbid	Could not format ( ph -> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) : No typesetting found for |- ( ph -> ( ( F : A --> B /\ G : B --> A ) /\ ( ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) /\ A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) ) /\ ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) ) ) ) with typecode |-
16	15	simplrd	$$⊢\phi \to G:B⟶A$$
17	15	simplld	$$⊢\phi \to F:A⟶B$$
18	16 9	ffvelcdmd	$$⊢\phi \to G\left(Y\right)\in A$$
19	17 18	ffvelcdmd	$$⊢\phi \to F\left(G\left(Y\right)\right)\in B$$
20	16 19	ffvelcdmd	$$⊢\phi \to G\left(F\left(G\left(Y\right)\right)\right)\in A$$
21	2 3 4 5 1 11 13 8 9	mgccole2	Could not format ( ph -> ( F ` ( G ` Y ) ) .c_ Y ) : No typesetting found for |- ( ph -> ( F ` ( G ` Y ) ) .c_ Y ) with typecode |-
22	2 3 4 5 1 11 13 8 19 9 21	mgcmnt2	$$⊢\phi \to G\left(F\left(G\left(Y\right)\right)\right)\underset{\dot{}}{\le }G\left(Y\right)$$
23	2 3 4 5 1 11 13 8 18	mgccole1	$$⊢\phi \to G\left(Y\right)\underset{\dot{}}{\le }G\left(F\left(G\left(Y\right)\right)\right)$$
24	2 4	posasymb	$$⊢\left(V\in \mathrm{Poset}\wedge G\left(F\left(G\left(Y\right)\right)\right)\in A\wedge G\left(Y\right)\in A\right)\to \left(\left(G\left(F\left(G\left(Y\right)\right)\right)\underset{\dot{}}{\le }G\left(Y\right)\wedge G\left(Y\right)\underset{\dot{}}{\le }G\left(F\left(G\left(Y\right)\right)\right)\right)\leftrightarrow G\left(F\left(G\left(Y\right)\right)\right)=G\left(Y\right)\right)$$
25	24	biimpa	$$⊢\left(\left(V\in \mathrm{Poset}\wedge G\left(F\left(G\left(Y\right)\right)\right)\in A\wedge G\left(Y\right)\in A\right)\wedge \left(G\left(F\left(G\left(Y\right)\right)\right)\underset{\dot{}}{\le }G\left(Y\right)\wedge G\left(Y\right)\underset{\dot{}}{\le }G\left(F\left(G\left(Y\right)\right)\right)\right)\right)\to G\left(F\left(G\left(Y\right)\right)\right)=G\left(Y\right)$$
26	6 20 18 22 23 25	syl32anc	$$⊢\phi \to G\left(F\left(G\left(Y\right)\right)\right)=G\left(Y\right)$$