Metamath Proof Explorer

Theorem dfmgc2lem

Description: Lemma for dfmgc2, backwards direction. (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 )
dfmgc2lem.1 
|- ( ph -> F : A --> B )
dfmgc2lem.2 
|- ( ph -> G : B --> A )
dfmgc2lem.3 
|- ( ph -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) )
dfmgc2lem.4 
|- ( ph -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) )
dfmgc2lem.5 
|- ( ( ph /\ x e. A ) -> x .<_ ( G ` ( F ` x ) ) )
dfmgc2lem.6 
|- ( ( ph /\ u e. B ) -> ( F ` ( G ` u ) ) .c_ u )
Assertion dfmgc2lem 
|- ( ph -> F H G )

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 dfmgc2lem.1 
 |-  ( ph -> F : A --> B )
9 dfmgc2lem.2 
 |-  ( ph -> G : B --> A )
10 dfmgc2lem.3 
 |-  ( ph -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) )
11 dfmgc2lem.4 
 |-  ( ph -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) )
12 dfmgc2lem.5 
 |-  ( ( ph /\ x e. A ) -> x .<_ ( G ` ( F ` x ) ) )
13 dfmgc2lem.6 
 |-  ( ( ph /\ u e. B ) -> ( F ` ( G ` u ) ) .c_ u )
14 8 9 jca 
 |-  ( ph -> ( F : A --> B /\ G : B --> A ) )
15 6 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> V e. Proset )
16 simplr 
 |-  ( ( ( ph /\ z e. A ) /\ w e. B ) -> z e. A )
17 16 adantr 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> z e. A )
18 9 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> G : B --> A )
19 8 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> F : A --> B )
20 19 17 ffvelrnd 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( F ` z ) e. B )
21 18 20 ffvelrnd 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( G ` ( F ` z ) ) e. A )
22 9 ad2antrr 
 |-  ( ( ( ph /\ z e. A ) /\ w e. B ) -> G : B --> A )
23 simpr 
 |-  ( ( ( ph /\ z e. A ) /\ w e. B ) -> w e. B )
24 22 23 ffvelrnd 
 |-  ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( G ` w ) e. A )
25 24 adantr 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( G ` w ) e. A )
26 12 ralrimiva 
 |-  ( ph -> A. x e. A x .<_ ( G ` ( F ` x ) ) )
27 26 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> A. x e. A x .<_ ( G ` ( F ` x ) ) )
28 simpr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) /\ x = z ) -> x = z )
29 28 fveq2d 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) /\ x = z ) -> ( F ` x ) = ( F ` z ) )
30 29 fveq2d 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) /\ x = z ) -> ( G ` ( F ` x ) ) = ( G ` ( F ` z ) ) )
31 28 30 breq12d 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) /\ x = z ) -> ( x .<_ ( G ` ( F ` x ) ) <-> z .<_ ( G ` ( F ` z ) ) ) )
32 17 31 rspcdv 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( A. x e. A x .<_ ( G ` ( F ` x ) ) -> z .<_ ( G ` ( F ` z ) ) ) )
33 27 32 mpd 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> z .<_ ( G ` ( F ` z ) ) )
34 11 ad2antrr 
 |-  ( ( ( ph /\ z e. A ) /\ w e. B ) -> A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) )
35 breq1 
 |-  ( u = ( F ` z ) -> ( u .c_ v <-> ( F ` z ) .c_ v ) )
36 fveq2 
 |-  ( u = ( F ` z ) -> ( G ` u ) = ( G ` ( F ` z ) ) )
37 36 breq1d 
 |-  ( u = ( F ` z ) -> ( ( G ` u ) .<_ ( G ` v ) <-> ( G ` ( F ` z ) ) .<_ ( G ` v ) ) )
38 35 37 imbi12d 
 |-  ( u = ( F ` z ) -> ( ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) <-> ( ( F ` z ) .c_ v -> ( G ` ( F ` z ) ) .<_ ( G ` v ) ) ) )
39 breq2 
 |-  ( v = w -> ( ( F ` z ) .c_ v <-> ( F ` z ) .c_ w ) )
40 fveq2 
 |-  ( v = w -> ( G ` v ) = ( G ` w ) )
41 40 breq2d 
 |-  ( v = w -> ( ( G ` ( F ` z ) ) .<_ ( G ` v ) <-> ( G ` ( F ` z ) ) .<_ ( G ` w ) ) )
42 39 41 imbi12d 
 |-  ( v = w -> ( ( ( F ` z ) .c_ v -> ( G ` ( F ` z ) ) .<_ ( G ` v ) ) <-> ( ( F ` z ) .c_ w -> ( G ` ( F ` z ) ) .<_ ( G ` w ) ) ) )
43 8 ffvelrnda 
 |-  ( ( ph /\ z e. A ) -> ( F ` z ) e. B )
44 43 adantr 
 |-  ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( F ` z ) e. B )
45 eqidd 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ u = ( F ` z ) ) -> B = B )
46 38 42 44 45 23 rspc2vd 
 |-  ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( A. u e. B A. v e. B ( u .c_ v -> ( G ` u ) .<_ ( G ` v ) ) -> ( ( F ` z ) .c_ w -> ( G ` ( F ` z ) ) .<_ ( G ` w ) ) ) )
47 34 46 mpd 
 |-  ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( ( F ` z ) .c_ w -> ( G ` ( F ` z ) ) .<_ ( G ` w ) ) )
48 47 imp 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> ( G ` ( F ` z ) ) .<_ ( G ` w ) )
49 1 3 prstr 
 |-  ( ( V e. Proset /\ ( z e. A /\ ( G ` ( F ` z ) ) e. A /\ ( G ` w ) e. A ) /\ ( z .<_ ( G ` ( F ` z ) ) /\ ( G ` ( F ` z ) ) .<_ ( G ` w ) ) ) -> z .<_ ( G ` w ) )
50 15 17 21 25 33 48 49 syl132anc 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ ( F ` z ) .c_ w ) -> z .<_ ( G ` w ) )
51 7 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> W e. Proset )
52 43 ad2antrr 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( F ` z ) e. B )
53 8 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> F : A --> B )
54 24 adantr 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( G ` w ) e. A )
55 53 54 ffvelrnd 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( F ` ( G ` w ) ) e. B )
56 simplr 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> w e. B )
57 10 ad2antrr 
 |-  ( ( ( ph /\ z e. A ) /\ w e. B ) -> A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) )
58 breq1 
 |-  ( x = z -> ( x .<_ y <-> z .<_ y ) )
59 fveq2 
 |-  ( x = z -> ( F ` x ) = ( F ` z ) )
60 59 breq1d 
 |-  ( x = z -> ( ( F ` x ) .c_ ( F ` y ) <-> ( F ` z ) .c_ ( F ` y ) ) )
61 58 60 imbi12d 
 |-  ( x = z -> ( ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) <-> ( z .<_ y -> ( F ` z ) .c_ ( F ` y ) ) ) )
62 breq2 
 |-  ( y = ( G ` w ) -> ( z .<_ y <-> z .<_ ( G ` w ) ) )
63 fveq2 
 |-  ( y = ( G ` w ) -> ( F ` y ) = ( F ` ( G ` w ) ) )
64 63 breq2d 
 |-  ( y = ( G ` w ) -> ( ( F ` z ) .c_ ( F ` y ) <-> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) )
65 62 64 imbi12d 
 |-  ( y = ( G ` w ) -> ( ( z .<_ y -> ( F ` z ) .c_ ( F ` y ) ) <-> ( z .<_ ( G ` w ) -> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) ) )
66 eqidd 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ x = z ) -> A = A )
67 61 65 16 66 24 rspc2vd 
 |-  ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( A. x e. A A. y e. A ( x .<_ y -> ( F ` x ) .c_ ( F ` y ) ) -> ( z .<_ ( G ` w ) -> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) ) )
68 57 67 mpd 
 |-  ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( z .<_ ( G ` w ) -> ( F ` z ) .c_ ( F ` ( G ` w ) ) ) )
69 68 imp 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( F ` z ) .c_ ( F ` ( G ` w ) ) )
70 13 ralrimiva 
 |-  ( ph -> A. u e. B ( F ` ( G ` u ) ) .c_ u )
71 70 ad3antrrr 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> A. u e. B ( F ` ( G ` u ) ) .c_ u )
72 simpr 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) /\ u = w ) -> u = w )
73 72 fveq2d 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) /\ u = w ) -> ( G ` u ) = ( G ` w ) )
74 73 fveq2d 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) /\ u = w ) -> ( F ` ( G ` u ) ) = ( F ` ( G ` w ) ) )
75 74 72 breq12d 
 |-  ( ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) /\ u = w ) -> ( ( F ` ( G ` u ) ) .c_ u <-> ( F ` ( G ` w ) ) .c_ w ) )
76 56 75 rspcdv 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( A. u e. B ( F ` ( G ` u ) ) .c_ u -> ( F ` ( G ` w ) ) .c_ w ) )
77 71 76 mpd 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( F ` ( G ` w ) ) .c_ w )
78 2 4 prstr 
 |-  ( ( W e. Proset /\ ( ( F ` z ) e. B /\ ( F ` ( G ` w ) ) e. B /\ w e. B ) /\ ( ( F ` z ) .c_ ( F ` ( G ` w ) ) /\ ( F ` ( G ` w ) ) .c_ w ) ) -> ( F ` z ) .c_ w )
79 51 52 55 56 69 77 78 syl132anc 
 |-  ( ( ( ( ph /\ z e. A ) /\ w e. B ) /\ z .<_ ( G ` w ) ) -> ( F ` z ) .c_ w )
80 50 79 impbida 
 |-  ( ( ( ph /\ z e. A ) /\ w e. B ) -> ( ( F ` z ) .c_ w <-> z .<_ ( G ` w ) ) )
81 80 anasss 
 |-  ( ( ph /\ ( z e. A /\ w e. B ) ) -> ( ( F ` z ) .c_ w <-> z .<_ ( G ` w ) ) )
82 81 ralrimivva 
 |-  ( ph -> A. z e. A A. w e. B ( ( F ` z ) .c_ w <-> z .<_ ( G ` w ) ) )
83 1 2 3 4 5 6 7 mgcval 
 |-  ( ph -> ( F H G <-> ( ( F : A --> B /\ G : B --> A ) /\ A. z e. A A. w e. B ( ( F ` z ) .c_ w <-> z .<_ ( G ` w ) ) ) ) )
84 14 82 83 mpbir2and 
 |-  ( ph -> F H G )