Metamath Proof Explorer

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 MGalConn W )
mgcf1o.a 
|- A = ( Base ` V )
mgcf1o.b 
|- B = ( Base ` W )
mgcf1o.1 
|- .<_ = ( le ` V )
mgcf1o.2 
|- .c_ = ( le ` W )
mgcf1o.v 
|- ( ph -> V e. Poset )
mgcf1o.w 
|- ( ph -> W e. Poset )
mgcf1o.f 
|- ( ph -> F H G )
mgcf1olem2.1 
|- ( ph -> Y e. B )
Assertion mgcf1olem2 
|- ( ph -> ( G ` ( F ` ( G ` Y ) ) ) = ( G ` Y ) )

Proof

Step Hyp Ref Expression
1 mgcf1o.h 
 |-  H = ( V MGalConn W )
2 mgcf1o.a 
 |-  A = ( Base ` V )
3 mgcf1o.b 
 |-  B = ( Base ` W )
4 mgcf1o.1 
 |-  .<_ = ( le ` V )
5 mgcf1o.2 
 |-  .c_ = ( le ` W )
6 mgcf1o.v 
 |-  ( ph -> V e. Poset )
7 mgcf1o.w 
 |-  ( ph -> W e. Poset )
8 mgcf1o.f 
 |-  ( ph -> F H G )
9 mgcf1olem2.1 
 |-  ( ph -> Y e. B )
10 posprs 
 |-  ( V e. Poset -> V e. Proset )
11 6 10 syl 
 |-  ( ph -> V e. Proset )
12 posprs 
 |-  ( W e. Poset -> W e. Proset )
13 7 12 syl 
 |-  ( ph -> W e. Proset )
14 2 3 4 5 1 11 13 dfmgc2 
 |-  ( 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 ) ) ) ) ) ) )
15 8 14 mpbid 
 |-  ( 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 ) ) ) ) ) )
16 15 simplrd 
 |-  ( ph -> G : B --> A )
17 15 simplld 
 |-  ( ph -> F : A --> B )
18 16 9 ffvelrnd 
 |-  ( ph -> ( G ` Y ) e. A )
19 17 18 ffvelrnd 
 |-  ( ph -> ( F ` ( G ` Y ) ) e. B )
20 16 19 ffvelrnd 
 |-  ( ph -> ( G ` ( F ` ( G ` Y ) ) ) e. A )
21 2 3 4 5 1 11 13 8 9 mgccole2 
 |-  ( ph -> ( F ` ( G ` Y ) ) .c_ Y )
22 2 3 4 5 1 11 13 8 19 9 21 mgcmnt2 
 |-  ( ph -> ( G ` ( F ` ( G ` Y ) ) ) .<_ ( G ` Y ) )
23 2 3 4 5 1 11 13 8 18 mgccole1 
 |-  ( ph -> ( G ` Y ) .<_ ( G ` ( F ` ( G ` Y ) ) ) )
24 2 4 posasymb 
 |-  ( ( V e. Poset /\ ( G ` ( F ` ( G ` Y ) ) ) e. A /\ ( G ` Y ) e. A ) -> ( ( ( G ` ( F ` ( G ` Y ) ) ) .<_ ( G ` Y ) /\ ( G ` Y ) .<_ ( G ` ( F ` ( G ` Y ) ) ) ) <-> ( G ` ( F ` ( G ` Y ) ) ) = ( G ` Y ) ) )
25 24 biimpa 
 |-  ( ( ( V e. Poset /\ ( G ` ( F ` ( G ` Y ) ) ) e. A /\ ( G ` Y ) e. A ) /\ ( ( G ` ( F ` ( G ` Y ) ) ) .<_ ( G ` Y ) /\ ( G ` Y ) .<_ ( G ` ( F ` ( G ` Y ) ) ) ) ) -> ( G ` ( F ` ( G ` Y ) ) ) = ( G ` Y ) )
26 6 20 18 22 23 25 syl32anc 
 |-  ( ph -> ( G ` ( F ` ( G ` Y ) ) ) = ( G ` Y ) )