Metamath Proof Explorer

Theorem mgcmntco

Description: A Galois connection like statement, for two functions with same range. (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 )
mgcmntco.1 
|- C = ( Base ` X )
mgcmntco.2 
|- .< = ( le ` X )
mgcmntco.3 
|- ( ph -> X e. Proset )
mgcmntco.4 
|- ( ph -> K e. ( V Monot X ) )
mgcmntco.5 
|- ( ph -> L e. ( W Monot X ) )
Assertion mgcmntco 
|- ( ph -> ( A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) <-> A. y e. B ( K ` ( G ` y ) ) .< ( L ` 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 mgcmntco.1 
 |-  C = ( Base ` X )
10 mgcmntco.2 
 |-  .< = ( le ` X )
11 mgcmntco.3 
 |-  ( ph -> X e. Proset )
12 mgcmntco.4 
 |-  ( ph -> K e. ( V Monot X ) )
13 mgcmntco.5 
 |-  ( ph -> L e. ( W Monot X ) )
14 11 ad2antrr 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> X e. Proset )
15 1 9 mntf 
 |-  ( ( V e. Proset /\ X e. Proset /\ K e. ( V Monot X ) ) -> K : A --> C )
16 6 11 12 15 syl3anc 
 |-  ( ph -> K : A --> C )
17 16 ad2antrr 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> K : A --> C )
18 1 2 3 4 5 6 7 8 mgcf2 
 |-  ( ph -> G : B --> A )
19 18 adantr 
 |-  ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) -> G : B --> A )
20 19 ffvelrnda 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> ( G ` y ) e. A )
21 17 20 ffvelrnd 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> ( K ` ( G ` y ) ) e. C )
22 2 9 mntf 
 |-  ( ( W e. Proset /\ X e. Proset /\ L e. ( W Monot X ) ) -> L : B --> C )
23 7 11 13 22 syl3anc 
 |-  ( ph -> L : B --> C )
24 23 ad2antrr 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> L : B --> C )
25 1 2 3 4 5 6 7 8 mgcf1 
 |-  ( ph -> F : A --> B )
26 25 ad2antrr 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> F : A --> B )
27 26 20 ffvelrnd 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> ( F ` ( G ` y ) ) e. B )
28 24 27 ffvelrnd 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> ( L ` ( F ` ( G ` y ) ) ) e. C )
29 23 adantr 
 |-  ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) -> L : B --> C )
30 29 ffvelrnda 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> ( L ` y ) e. C )
31 18 ffvelrnda 
 |-  ( ( ph /\ y e. B ) -> ( G ` y ) e. A )
32 fveq2 
 |-  ( x = ( G ` y ) -> ( K ` x ) = ( K ` ( G ` y ) ) )
33 2fveq3 
 |-  ( x = ( G ` y ) -> ( L ` ( F ` x ) ) = ( L ` ( F ` ( G ` y ) ) ) )
34 32 33 breq12d 
 |-  ( x = ( G ` y ) -> ( ( K ` x ) .< ( L ` ( F ` x ) ) <-> ( K ` ( G ` y ) ) .< ( L ` ( F ` ( G ` y ) ) ) ) )
35 34 adantl 
 |-  ( ( ( ph /\ y e. B ) /\ x = ( G ` y ) ) -> ( ( K ` x ) .< ( L ` ( F ` x ) ) <-> ( K ` ( G ` y ) ) .< ( L ` ( F ` ( G ` y ) ) ) ) )
36 31 35 rspcdv 
 |-  ( ( ph /\ y e. B ) -> ( A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) -> ( K ` ( G ` y ) ) .< ( L ` ( F ` ( G ` y ) ) ) ) )
37 36 imp 
 |-  ( ( ( ph /\ y e. B ) /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) -> ( K ` ( G ` y ) ) .< ( L ` ( F ` ( G ` y ) ) ) )
38 37 an32s 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> ( K ` ( G ` y ) ) .< ( L ` ( F ` ( G ` y ) ) ) )
39 7 ad2antrr 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> W e. Proset )
40 13 ad2antrr 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> L e. ( W Monot X ) )
41 simpr 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> y e. B )
42 6 ad2antrr 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> V e. Proset )
43 8 ad2antrr 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> F H G )
44 1 2 3 4 5 42 39 43 41 mgccole2 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> ( F ` ( G ` y ) ) .c_ y )
45 2 9 4 10 39 14 40 27 41 44 ismntd 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> ( L ` ( F ` ( G ` y ) ) ) .< ( L ` y ) )
46 9 10 prstr 
 |-  ( ( X e. Proset /\ ( ( K ` ( G ` y ) ) e. C /\ ( L ` ( F ` ( G ` y ) ) ) e. C /\ ( L ` y ) e. C ) /\ ( ( K ` ( G ` y ) ) .< ( L ` ( F ` ( G ` y ) ) ) /\ ( L ` ( F ` ( G ` y ) ) ) .< ( L ` y ) ) ) -> ( K ` ( G ` y ) ) .< ( L ` y ) )
47 14 21 28 30 38 45 46 syl132anc 
 |-  ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> ( K ` ( G ` y ) ) .< ( L ` y ) )
48 47 ralrimiva 
 |-  ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) -> A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) )
49 11 ad2antrr 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> X e. Proset )
50 16 ad2antrr 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> K : A --> C )
51 simpr 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> x e. A )
52 50 51 ffvelrnd 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> ( K ` x ) e. C )
53 18 ad2antrr 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> G : B --> A )
54 25 adantr 
 |-  ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) -> F : A --> B )
55 54 ffvelrnda 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> ( F ` x ) e. B )
56 53 55 ffvelrnd 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> ( G ` ( F ` x ) ) e. A )
57 50 56 ffvelrnd 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> ( K ` ( G ` ( F ` x ) ) ) e. C )
58 23 ad2antrr 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> L : B --> C )
59 58 55 ffvelrnd 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> ( L ` ( F ` x ) ) e. C )
60 6 ad2antrr 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> V e. Proset )
61 12 ad2antrr 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> K e. ( V Monot X ) )
62 7 ad2antrr 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> W e. Proset )
63 8 ad2antrr 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> F H G )
64 1 2 3 4 5 60 62 63 51 mgccole1 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> x .<_ ( G ` ( F ` x ) ) )
65 1 9 3 10 60 49 61 51 56 64 ismntd 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> ( K ` x ) .< ( K ` ( G ` ( F ` x ) ) ) )
66 25 ffvelrnda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. B )
67 2fveq3 
 |-  ( y = ( F ` x ) -> ( K ` ( G ` y ) ) = ( K ` ( G ` ( F ` x ) ) ) )
68 fveq2 
 |-  ( y = ( F ` x ) -> ( L ` y ) = ( L ` ( F ` x ) ) )
69 67 68 breq12d 
 |-  ( y = ( F ` x ) -> ( ( K ` ( G ` y ) ) .< ( L ` y ) <-> ( K ` ( G ` ( F ` x ) ) ) .< ( L ` ( F ` x ) ) ) )
70 69 adantl 
 |-  ( ( ( ph /\ x e. A ) /\ y = ( F ` x ) ) -> ( ( K ` ( G ` y ) ) .< ( L ` y ) <-> ( K ` ( G ` ( F ` x ) ) ) .< ( L ` ( F ` x ) ) ) )
71 66 70 rspcdv 
 |-  ( ( ph /\ x e. A ) -> ( A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) -> ( K ` ( G ` ( F ` x ) ) ) .< ( L ` ( F ` x ) ) ) )
72 71 imp 
 |-  ( ( ( ph /\ x e. A ) /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) -> ( K ` ( G ` ( F ` x ) ) ) .< ( L ` ( F ` x ) ) )
73 72 an32s 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> ( K ` ( G ` ( F ` x ) ) ) .< ( L ` ( F ` x ) ) )
74 9 10 prstr 
 |-  ( ( X e. Proset /\ ( ( K ` x ) e. C /\ ( K ` ( G ` ( F ` x ) ) ) e. C /\ ( L ` ( F ` x ) ) e. C ) /\ ( ( K ` x ) .< ( K ` ( G ` ( F ` x ) ) ) /\ ( K ` ( G ` ( F ` x ) ) ) .< ( L ` ( F ` x ) ) ) ) -> ( K ` x ) .< ( L ` ( F ` x ) ) )
75 49 52 57 59 65 73 74 syl132anc 
 |-  ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> ( K ` x ) .< ( L ` ( F ` x ) ) )
76 75 ralrimiva 
 |-  ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) -> A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) )
77 48 76 impbida 
 |-  ( ph -> ( A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) <-> A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) )