Metamath Proof Explorer

Theorem dfmgc2

Description: Alternate definition of the monotone Galois connection. (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 )
Assertion 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 ) ) ) ) ) ) )

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 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 ) ) ) ) )
9 8 simprbda 
 |-  ( ( ph /\ F H G ) -> ( F : A --> B /\ G : B --> A ) )
10 6 ad4antr 
 |-  ( ( ( ( ( ph /\ F H G ) /\ x e. A ) /\ y e. A ) /\ x .<_ y ) -> V e. Proset )
11 7 ad4antr 
 |-  ( ( ( ( ( ph /\ F H G ) /\ x e. A ) /\ y e. A ) /\ x .<_ y ) -> W e. Proset )
12 simp-4r 
 |-  ( ( ( ( ( ph /\ F H G ) /\ x e. A ) /\ y e. A ) /\ x .<_ y ) -> F H G )
13 simpllr 
 |-  ( ( ( ( ( ph /\ F H G ) /\ x e. A ) /\ y e. A ) /\ x .<_ y ) -> x e. A )
14 simplr 
 |-  ( ( ( ( ( ph /\ F H G ) /\ x e. A ) /\ y e. A ) /\ x .<_ y ) -> y e. A )
15 simpr 
 |-  ( ( ( ( ( ph /\ F H G ) /\ x e. A ) /\ y e. A ) /\ x .<_ y ) -> x .<_ y )
16 1 2 3 4 5 10 11 12 13 14 15 mgcmnt1 
 |-  ( ( ( ( ( ph /\ F H G ) /\ x e. A ) /\ y e. A ) /\ x .<_ y ) -> ( F ` x ) .c_ ( F ` y ) )
17 16 ex 
 |-  ( ( ( ( ph /\ F H G ) /\ x e. A ) /\ y e. A ) -> ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) )
18 17 anasss 
 |-  ( ( ( ph /\ F H G ) /\ ( x e. A /\ y e. A ) ) -> ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) )
19 18 ralrimivva 
 |-  ( ( ph /\ F H G ) -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) )
20 6 ad4antr 
 |-  ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> V e. Proset )
21 7 ad4antr 
 |-  ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> W e. Proset )
22 simp-4r 
 |-  ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> F H G )
23 simpllr 
 |-  ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> u e. B )
24 simplr 
 |-  ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> v e. B )
25 simpr 
 |-  ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> u .c_ v )
26 1 2 3 4 5 20 21 22 23 24 25 mgcmnt2 
 |-  ( ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) /\ u .c_ v ) -> ( G ` u ) .<_ ( G ` v ) )
27 26 ex 
 |-  ( ( ( ( ph /\ F H G ) /\ u e. B ) /\ v e. B ) -> ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) )
28 27 anasss 
 |-  ( ( ( ph /\ F H G ) /\ ( u e. B /\ v e. B ) ) -> ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) )
29 28 ralrimivva 
 |-  ( ( ph /\ F H G ) -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) )
30 19 29 jca 
 |-  ( ( ph /\ F H G ) -> ( 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 ) ) ) )
31 6 ad2antrr 
 |-  ( ( ( ph /\ F H G ) /\ u e. B ) -> V e. Proset )
32 7 ad2antrr 
 |-  ( ( ( ph /\ F H G ) /\ u e. B ) -> W e. Proset )
33 simplr 
 |-  ( ( ( ph /\ F H G ) /\ u e. B ) -> F H G )
34 simpr 
 |-  ( ( ( ph /\ F H G ) /\ u e. B ) -> u e. B )
35 1 2 3 4 5 31 32 33 34 mgccole2 
 |-  ( ( ( ph /\ F H G ) /\ u e. B ) -> ( F ` ( G ` u ) ) .c_ u )
36 35 ralrimiva 
 |-  ( ( ph /\ F H G ) -> A. u e. B ( F ` ( G ` u ) ) .c_ u )
37 6 ad2antrr 
 |-  ( ( ( ph /\ F H G ) /\ x e. A ) -> V e. Proset )
38 7 ad2antrr 
 |-  ( ( ( ph /\ F H G ) /\ x e. A ) -> W e. Proset )
39 simplr 
 |-  ( ( ( ph /\ F H G ) /\ x e. A ) -> F H G )
40 simpr 
 |-  ( ( ( ph /\ F H G ) /\ x e. A ) -> x e. A )
41 1 2 3 4 5 37 38 39 40 mgccole1 
 |-  ( ( ( ph /\ F H G ) /\ x e. A ) -> x .<_ ( G ` ( F ` x ) ) )
42 41 ralrimiva 
 |-  ( ( ph /\ F H G ) -> A. x e. A x .<_ ( G ` ( F ` x ) ) )
43 36 42 jca 
 |-  ( ( ph /\ F H G ) -> ( A. u e. B ( F ` ( G ` u ) ) .c_ u /\ A. x e. A x .<_ ( G ` ( F ` x ) ) ) )
44 30 43 jca 
 |-  ( ( ph /\ F H G ) -> ( ( 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 ) ) ) ) )
45 9 44 jca 
 |-  ( ( 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 ) ) ) ) ) )
46 6 ad4antr 
 |-  ( ( ( ( ( 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 ) ) ) -> V e. Proset )
47 7 ad4antr 
 |-  ( ( ( ( ( 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 ) ) ) -> W e. Proset )
48 simp-4r 
 |-  ( ( ( ( ( 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 ) ) ) -> ( F : A --> B /\ G : B --> A ) )
49 48 simpld 
 |-  ( ( ( ( ( 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 ) ) ) -> F : A --> B )
50 48 simprd 
 |-  ( ( ( ( ( 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 ) ) ) -> G : B --> A )
51 simpllr 
 |-  ( ( ( ( ( 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 ) ) ) -> ( 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 ) ) ) )
52 51 simpld 
 |-  ( ( ( ( ( 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 ) ) ) -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) )
53 breq1 
 |-  ( x = m -> ( x .<_ y <-> m .<_ y ) )
54 fveq2 
 |-  ( x = m -> ( F ` x ) = ( F ` m ) )
55 54 breq1d 
 |-  ( x = m -> ( ( F ` x ) .c_ ( F ` y ) <-> ( F ` m ) .c_ ( F ` y ) ) )
56 53 55 imbi12d 
 |-  ( x = m -> ( ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) <-> ( m .<_ y -> ( F ` m ) .c_ ( F ` y ) ) ) )
57 breq2 
 |-  ( y = n -> ( m .<_ y <-> m .<_ n ) )
58 fveq2 
 |-  ( y = n -> ( F ` y ) = ( F ` n ) )
59 58 breq2d 
 |-  ( y = n -> ( ( F ` m ) .c_ ( F ` y ) <-> ( F ` m ) .c_ ( F ` n ) ) )
60 57 59 imbi12d 
 |-  ( y = n -> ( ( m .<_ y -> ( F ` m ) .c_ ( F ` y ) ) <-> ( m .<_ n -> ( F ` m ) .c_ ( F ` n ) ) ) )
61 56 60 cbvral2vw 
 |-  ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) <-> A. m e. A A. n e. A ( m .<_ n -> ( F ` m ) .c_ ( F ` n ) ) )
62 52 61 sylib 
 |-  ( ( ( ( ( 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 ) ) ) -> A. m e. A A. n e. A ( m .<_ n -> ( F ` m ) .c_ ( F ` n ) ) )
63 51 simprd 
 |-  ( ( ( ( ( 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 ) ) ) -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) )
64 breq1 
 |-  ( u = i -> ( u .c_ v <-> i .c_ v ) )
65 fveq2 
 |-  ( u = i -> ( G ` u ) = ( G ` i ) )
66 65 breq1d 
 |-  ( u = i -> ( ( G ` u ) .<_ ( G ` v ) <-> ( G ` i ) .<_ ( G ` v ) ) )
67 64 66 imbi12d 
 |-  ( u = i -> ( ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) <-> ( i .c_ v -> ( G ` i ) .<_ ( G ` v ) ) ) )
68 breq2 
 |-  ( v = j -> ( i .c_ v <-> i .c_ j ) )
69 fveq2 
 |-  ( v = j -> ( G ` v ) = ( G ` j ) )
70 69 breq2d 
 |-  ( v = j -> ( ( G ` i ) .<_ ( G ` v ) <-> ( G ` i ) .<_ ( G ` j ) ) )
71 68 70 imbi12d 
 |-  ( v = j -> ( ( i .c_ v -> ( G ` i ) .<_ ( G ` v ) ) <-> ( i .c_ j -> ( G ` i ) .<_ ( G ` j ) ) ) )
72 67 71 cbvral2vw 
 |-  ( A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) <-> A. i e. B A. j e. B ( i .c_ j -> ( G ` i ) .<_ ( G ` j ) ) )
73 63 72 sylib 
 |-  ( ( ( ( ( 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 ) ) ) -> A. i e. B A. j e. B ( i .c_ j -> ( G ` i ) .<_ ( G ` j ) ) )
74 id 
 |-  ( x = m -> x = m )
75 2fveq3 
 |-  ( x = m -> ( G ` ( F ` x ) ) = ( G ` ( F ` m ) ) )
76 74 75 breq12d 
 |-  ( x = m -> ( x .<_ ( G ` ( F ` x ) ) <-> m .<_ ( G ` ( F ` m ) ) ) )
77 simplr 
 |-  ( ( ( ( ( ( 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 ) ) ) /\ m e. A ) -> A. x e. A x .<_ ( G ` ( F ` x ) ) )
78 simpr 
 |-  ( ( ( ( ( ( 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 ) ) ) /\ m e. A ) -> m e. A )
79 76 77 78 rspcdva 
 |-  ( ( ( ( ( ( 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 ) ) ) /\ m e. A ) -> m .<_ ( G ` ( F ` m ) ) )
80 2fveq3 
 |-  ( u = i -> ( F ` ( G ` u ) ) = ( F ` ( G ` i ) ) )
81 id 
 |-  ( u = i -> u = i )
82 80 81 breq12d 
 |-  ( u = i -> ( ( F ` ( G ` u ) ) .c_ u <-> ( F ` ( G ` i ) ) .c_ i ) )
83 simpllr 
 |-  ( ( ( ( ( ( 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 ) ) ) /\ i e. B ) -> A. u e. B ( F ` ( G ` u ) ) .c_ u )
84 simpr 
 |-  ( ( ( ( ( ( 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 ) ) ) /\ i e. B ) -> i e. B )
85 82 83 84 rspcdva 
 |-  ( ( ( ( ( ( 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 ) ) ) /\ i e. B ) -> ( F ` ( G ` i ) ) .c_ i )
86 1 2 3 4 5 46 47 49 50 62 73 79 85 dfmgc2lem 
 |-  ( ( ( ( ( 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 ) ) ) -> F H G )
87 86 anasss 
 |-  ( ( ( ( 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 ) ) ) ) -> F H G )
88 87 anasss 
 |-  ( ( ( 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 ) ) ) ) ) -> F H G )
89 88 anasss 
 |-  ( ( 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 ) ) ) ) ) ) -> F H G )
90 45 89 impbida 
 |-  ( 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 ) ) ) ) ) ) )