Theorem mgcf1olem1

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$$
	mgcf1olem1.1	$$⊢\phi \to X\in A$$
Assertion	mgcf1olem1	$$⊢\phi \to F\left(G\left(F\left(X\right)\right)\right)=F\left(X\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		mgcf1olem1.1	$$⊢\phi \to X\in A$$
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	simplld	$$⊢\phi \to F:A⟶B$$
17	15	simplrd	$$⊢\phi \to G:B⟶A$$
18	16 9	ffvelcdmd	$$⊢\phi \to F\left(X\right)\in B$$
19	17 18	ffvelcdmd	$$⊢\phi \to G\left(F\left(X\right)\right)\in A$$
20	16 19	ffvelcdmd	$$⊢\phi \to F\left(G\left(F\left(X\right)\right)\right)\in B$$
21	2 3 4 5 1 11 13 8 18	mgccole2	Could not format ( ph -> ( F ` ( G ` ( F ` X ) ) ) .c_ ( F ` X ) ) : No typesetting found for |- ( ph -> ( F ` ( G ` ( F ` X ) ) ) .c_ ( F ` X ) ) with typecode |-
22	2 3 4 5 1 11 13 8 9	mgccole1	$$⊢\phi \to X\underset{\dot{}}{\le }G\left(F\left(X\right)\right)$$
23	2 3 4 5 1 11 13 8 9 19 22	mgcmnt1	Could not format ( ph -> ( F ` X ) .c_ ( F ` ( G ` ( F ` X ) ) ) ) : No typesetting found for |- ( ph -> ( F ` X ) .c_ ( F ` ( G ` ( F ` X ) ) ) ) with typecode |-
24	3 5	posasymb	Could not format ( ( W e. Poset /\ ( F ` ( G ` ( F ` X ) ) ) e. B /\ ( F ` X ) e. B ) -> ( ( ( F ` ( G ` ( F ` X ) ) ) .c_ ( F ` X ) /\ ( F ` X ) .c_ ( F ` ( G ` ( F ` X ) ) ) ) <-> ( F ` ( G ` ( F ` X ) ) ) = ( F ` X ) ) ) : No typesetting found for |- ( ( W e. Poset /\ ( F ` ( G ` ( F ` X ) ) ) e. B /\ ( F ` X ) e. B ) -> ( ( ( F ` ( G ` ( F ` X ) ) ) .c_ ( F ` X ) /\ ( F ` X ) .c_ ( F ` ( G ` ( F ` X ) ) ) ) <-> ( F ` ( G ` ( F ` X ) ) ) = ( F ` X ) ) ) with typecode |-
25	24	biimpa	Could not format ( ( ( W e. Poset /\ ( F ` ( G ` ( F ` X ) ) ) e. B /\ ( F ` X ) e. B ) /\ ( ( F ` ( G ` ( F ` X ) ) ) .c_ ( F ` X ) /\ ( F ` X ) .c_ ( F ` ( G ` ( F ` X ) ) ) ) ) -> ( F ` ( G ` ( F ` X ) ) ) = ( F ` X ) ) : No typesetting found for |- ( ( ( W e. Poset /\ ( F ` ( G ` ( F ` X ) ) ) e. B /\ ( F ` X ) e. B ) /\ ( ( F ` ( G ` ( F ` X ) ) ) .c_ ( F ` X ) /\ ( F ` X ) .c_ ( F ` ( G ` ( F ` X ) ) ) ) ) -> ( F ` ( G ` ( F ` X ) ) ) = ( F ` X ) ) with typecode |-
26	7 20 18 21 23 25	syl32anc	$$⊢\phi \to F\left(G\left(F\left(X\right)\right)\right)=F\left(X\right)$$