This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 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 )
mgcf1olem1.1 
|- ( ph -> X e. A )
Assertion mgcf1olem1 
|- ( ph -> ( F ` ( G ` ( F ` X ) ) ) = ( F ` X ) )

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 mgcf1olem1.1 
 |-  ( ph -> X e. A )
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 simplld 
 |-  ( ph -> F : A --> B )
17 15 simplrd 
 |-  ( ph -> G : B --> A )
18 16 9 ffvelcdmd 
 |-  ( ph -> ( F ` X ) e. B )
19 17 18 ffvelcdmd 
 |-  ( ph -> ( G ` ( F ` X ) ) e. A )
20 16 19 ffvelcdmd 
 |-  ( ph -> ( F ` ( G ` ( F ` X ) ) ) e. B )
21 2 3 4 5 1 11 13 8 18 mgccole2 
 |-  ( ph -> ( F ` ( G ` ( F ` X ) ) ) .c_ ( F ` X ) )
22 2 3 4 5 1 11 13 8 9 mgccole1 
 |-  ( ph -> X .<_ ( G ` ( F ` X ) ) )
23 2 3 4 5 1 11 13 8 9 19 22 mgcmnt1 
 |-  ( ph -> ( F ` X ) .c_ ( F ` ( G ` ( F ` X ) ) ) )
24 3 5 posasymb 
 |-  ( ( 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 ) ) )
25 24 biimpa 
 |-  ( ( ( 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 ) )
26 7 20 18 21 23 25 syl32anc 
 |-  ( ph -> ( F ` ( G ` ( F ` X ) ) ) = ( F ` X ) )