Metamath Proof Explorer


Theorem mgccole1

Description: An inequality for the kernel operator G o. F . (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 )
mgccole1.2
|- ( ph -> X e. A )
Assertion mgccole1
|- ( ph -> X .<_ ( G ` ( F ` X ) ) )

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 mgccole1.2
 |-  ( ph -> X e. A )
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 simplld
 |-  ( ph -> F : A --> B )
13 12 9 ffvelrnd
 |-  ( ph -> ( F ` X ) e. B )
14 2 4 prsref
 |-  ( ( W e. Proset /\ ( F ` X ) e. B ) -> ( F ` X ) .c_ ( F ` X ) )
15 7 13 14 syl2anc
 |-  ( ph -> ( F ` X ) .c_ ( F ` X ) )
16 fveq2
 |-  ( x = X -> ( F ` x ) = ( F ` X ) )
17 16 breq1d
 |-  ( x = X -> ( ( F ` x ) .c_ y <-> ( F ` X ) .c_ y ) )
18 breq1
 |-  ( x = X -> ( x .<_ ( G ` y ) <-> X .<_ ( G ` y ) ) )
19 17 18 bibi12d
 |-  ( x = X -> ( ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) )
20 19 ralbidv
 |-  ( x = X -> ( A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) <-> A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) ) )
21 11 simprd
 |-  ( ph -> A. x e. A A. y e. B ( ( F ` x ) .c_ y <-> x .<_ ( G ` y ) ) )
22 20 21 9 rspcdva
 |-  ( ph -> A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) )
23 simpr
 |-  ( ( ph /\ y = ( F ` X ) ) -> y = ( F ` X ) )
24 23 breq2d
 |-  ( ( ph /\ y = ( F ` X ) ) -> ( ( F ` X ) .c_ y <-> ( F ` X ) .c_ ( F ` X ) ) )
25 23 fveq2d
 |-  ( ( ph /\ y = ( F ` X ) ) -> ( G ` y ) = ( G ` ( F ` X ) ) )
26 25 breq2d
 |-  ( ( ph /\ y = ( F ` X ) ) -> ( X .<_ ( G ` y ) <-> X .<_ ( G ` ( F ` X ) ) ) )
27 24 26 bibi12d
 |-  ( ( ph /\ y = ( F ` X ) ) -> ( ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) <-> ( ( F ` X ) .c_ ( F ` X ) <-> X .<_ ( G ` ( F ` X ) ) ) ) )
28 13 27 rspcdv
 |-  ( ph -> ( A. y e. B ( ( F ` X ) .c_ y <-> X .<_ ( G ` y ) ) -> ( ( F ` X ) .c_ ( F ` X ) <-> X .<_ ( G ` ( F ` X ) ) ) ) )
29 22 28 mpd
 |-  ( ph -> ( ( F ` X ) .c_ ( F ` X ) <-> X .<_ ( G ` ( F ` X ) ) ) )
30 15 29 mpbid
 |-  ( ph -> X .<_ ( G ` ( F ` X ) ) )