Metamath Proof Explorer

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 = ( Base ` V )
mgcoval.2 
|- B = ( Base ` W )
mgcoval.3 
|- .<_ = ( le ` V )
mgcoval.4 
|- .c_ = ( le ` W )
mgcval.1 
|- H = ( V MGalConn W )
mgcval.2 
|- ( ph -> V e. Proset )
mgcval.3 
|- ( ph -> W e. Proset )
mgccole.1 
|- ( ph -> F H G )
mgccole2.1 
|- ( ph -> Y e. B )
Assertion mgccole2 
|- ( ph -> ( F ` ( G ` Y ) ) .c_ Y )

Proof

Step Hyp Ref Expression
1 mgcoval.1 
 |-  A = ( Base ` V )
2 mgcoval.2 
 |-  B = ( Base ` W )
3 mgcoval.3 
 |-  .<_ = ( le ` V )
4 mgcoval.4 
 |-  .c_ = ( le ` W )
5 mgcval.1 
 |-  H = ( V MGalConn W )
6 mgcval.2 
 |-  ( ph -> V e. Proset )
7 mgcval.3 
 |-  ( ph -> W e. Proset )
8 mgccole.1 
 |-  ( ph -> F H G )
9 mgccole2.1 
 |-  ( ph -> Y e. B )
10 1 2 3 4 5 6 7 mgcval 
 |-  ( 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 ) ) ) ) )
11 8 10 mpbid 
 |-  ( ph -> ( ( F : A --> B /\ G : B --> A ) /\ A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) ) )
12 11 simplrd 
 |-  ( ph -> G : B --> A )
13 12 9 ffvelrnd 
 |-  ( ph -> ( G ` Y ) e. A )
14 1 3 prsref 
 |-  ( ( V e. Proset /\ ( G ` Y ) e. A ) -> ( G ` Y ) .<_ ( G ` Y ) )
15 6 13 14 syl2anc 
 |-  ( ph -> ( G ` Y ) .<_ ( G ` Y ) )
16 11 simprd 
 |-  ( ph -> A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) )
17 fveq2 
 |-  ( x = ( G ` Y ) -> ( F ` x ) = ( F ` ( G ` Y ) ) )
18 17 breq1d 
 |-  ( x = ( G ` Y ) -> ( ( F ` x ) .c_ y <-> ( F ` ( G ` Y ) ) .c_ y ) )
19 breq1 
 |-  ( x = ( G ` Y ) -> ( x .<_ ( G ` y ) <-> ( G ` Y ) .<_ ( G ` y ) ) )
20 18 19 bibi12d 
 |-  ( x = ( G ` Y ) -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) ) )
21 20 adantl 
 |-  ( ( ph /\ x = ( G ` Y ) ) -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) ) )
22 21 ralbidv 
 |-  ( ( 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 ) ) ) )
23 13 22 rspcdv 
 |-  ( 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 ) ) ) )
24 16 23 mpd 
 |-  ( ph -> A. y e. B ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) )
25 simpr 
 |-  ( ( ph /\ y = Y ) -> y = Y )
26 25 breq2d 
 |-  ( ( ph /\ y = Y ) -> ( ( F ` ( G ` Y ) ) .c_ y <-> ( F ` ( G ` Y ) ) .c_ Y ) )
27 fveq2 
 |-  ( y = Y -> ( G ` y ) = ( G ` Y ) )
28 27 adantl 
 |-  ( ( ph /\ y = Y ) -> ( G ` y ) = ( G ` Y ) )
29 28 breq2d 
 |-  ( ( ph /\ y = Y ) -> ( ( G ` Y ) .<_ ( G ` y ) <-> ( G ` Y ) .<_ ( G ` Y ) ) )
30 26 29 bibi12d 
 |-  ( ( ph /\ y = Y ) -> ( ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) <-> ( ( F ` ( G ` Y ) ) .c_ Y <-> ( G ` Y ) .<_ ( G ` Y ) ) ) )
31 9 30 rspcdv 
 |-  ( ph -> ( A. y e. B ( ( F ` ( G ` Y ) ) .c_ y <-> ( G ` Y ) .<_ ( G ` y ) ) -> ( ( F ` ( G ` Y ) ) .c_ Y <-> ( G ` Y ) .<_ ( G ` Y ) ) ) )
32 24 31 mpd 
 |-  ( ph -> ( ( F ` ( G ` Y ) ) .c_ Y <-> ( G ` Y ) .<_ ( G ` Y ) ) )
33 15 32 mpbird 
 |-  ( ph -> ( F ` ( G ` Y ) ) .c_ Y )