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 ˙ = V
mgcoval.4 No typesetting found for |- .c_ = ( le ` W ) with typecode |-
mgcval.1 No typesetting found for |- H = ( V MGalConn W ) with typecode |-
mgcval.2 φ V Proset
mgcval.3 φ W Proset
mgccole.1 φ F H G
mgcmntco.1 C = Base X
mgcmntco.2 < ˙ = X
mgcmntco.3 φ X Proset
mgcmntco.4 No typesetting found for |- ( ph -> K e. ( V Monot X ) ) with typecode |-
mgcmntco.5 No typesetting found for |- ( ph -> L e. ( W Monot X ) ) with typecode |-
Assertion mgcmntco φ x A K x < ˙ L F x y 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 ˙ = V
4 mgcoval.4 Could not format .c_ = ( le ` W ) : No typesetting found for |- .c_ = ( le ` W ) with typecode |-
5 mgcval.1 Could not format H = ( V MGalConn W ) : No typesetting found for |- H = ( V MGalConn W ) with typecode |-
6 mgcval.2 φ V Proset
7 mgcval.3 φ W Proset
8 mgccole.1 φ F H G
9 mgcmntco.1 C = Base X
10 mgcmntco.2 < ˙ = X
11 mgcmntco.3 φ X Proset
12 mgcmntco.4 Could not format ( ph -> K e. ( V Monot X ) ) : No typesetting found for |- ( ph -> K e. ( V Monot X ) ) with typecode |-
13 mgcmntco.5 Could not format ( ph -> L e. ( W Monot X ) ) : No typesetting found for |- ( ph -> L e. ( W Monot X ) ) with typecode |-
14 11 ad2antrr φ x A K x < ˙ L F x y B X Proset
15 1 9 mntf Could not format ( ( V e. Proset /\ X e. Proset /\ K e. ( V Monot X ) ) -> K : A --> C ) : No typesetting found for |- ( ( V e. Proset /\ X e. Proset /\ K e. ( V Monot X ) ) -> K : A --> C ) with typecode |-
16 6 11 12 15 syl3anc φ K : A C
17 16 ad2antrr φ x A K x < ˙ L F x y B K : A C
18 1 2 3 4 5 6 7 8 mgcf2 φ G : B A
19 18 adantr φ x A K x < ˙ L F x G : B A
20 19 ffvelrnda φ x A K x < ˙ L F x y B G y A
21 17 20 ffvelrnd φ x A K x < ˙ L F x y B K G y C
22 2 9 mntf Could not format ( ( W e. Proset /\ X e. Proset /\ L e. ( W Monot X ) ) -> L : B --> C ) : No typesetting found for |- ( ( W e. Proset /\ X e. Proset /\ L e. ( W Monot X ) ) -> L : B --> C ) with typecode |-
23 7 11 13 22 syl3anc φ L : B C
24 23 ad2antrr φ x A K x < ˙ L F x y B L : B C
25 1 2 3 4 5 6 7 8 mgcf1 φ F : A B
26 25 ad2antrr φ x A K x < ˙ L F x y B F : A B
27 26 20 ffvelrnd φ x A K x < ˙ L F x y B F G y B
28 24 27 ffvelrnd φ x A K x < ˙ L F x y B L F G y C
29 23 adantr φ x A K x < ˙ L F x L : B C
30 29 ffvelrnda φ x A K x < ˙ L F x y B L y C
31 18 ffvelrnda φ y B G y 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 φ y B x = G y K x < ˙ L F x K G y < ˙ L F G y
36 31 35 rspcdv φ y B x A K x < ˙ L F x K G y < ˙ L F G y
37 36 imp φ y B x A K x < ˙ L F x K G y < ˙ L F G y
38 37 an32s φ x A K x < ˙ L F x y B K G y < ˙ L F G y
39 7 ad2antrr φ x A K x < ˙ L F x y B W Proset
40 13 ad2antrr Could not format ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> L e. ( W Monot X ) ) : No typesetting found for |- ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> L e. ( W Monot X ) ) with typecode |-
41 simpr φ x A K x < ˙ L F x y B y B
42 6 ad2antrr φ x A K x < ˙ L F x y B V Proset
43 8 ad2antrr φ x A K x < ˙ L F x y B F H G
44 1 2 3 4 5 42 39 43 41 mgccole2 Could not format ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> ( F ` ( G ` y ) ) .c_ y ) : No typesetting found for |- ( ( ( ph /\ A. x e. A ( K ` x ) .< ( L ` ( F ` x ) ) ) /\ y e. B ) -> ( F ` ( G ` y ) ) .c_ y ) with typecode |-
45 2 9 4 10 39 14 40 27 41 44 ismntd φ x A K x < ˙ L F x y B L F G y < ˙ L y
46 9 10 prstr X Proset K G y C L F G y C L y 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 φ x A K x < ˙ L F x y B K G y < ˙ L y
48 47 ralrimiva φ x A K x < ˙ L F x y B K G y < ˙ L y
49 11 ad2antrr φ y B K G y < ˙ L y x A X Proset
50 16 ad2antrr φ y B K G y < ˙ L y x A K : A C
51 simpr φ y B K G y < ˙ L y x A x A
52 50 51 ffvelrnd φ y B K G y < ˙ L y x A K x C
53 18 ad2antrr φ y B K G y < ˙ L y x A G : B A
54 25 adantr φ y B K G y < ˙ L y F : A B
55 54 ffvelrnda φ y B K G y < ˙ L y x A F x B
56 53 55 ffvelrnd φ y B K G y < ˙ L y x A G F x A
57 50 56 ffvelrnd φ y B K G y < ˙ L y x A K G F x C
58 23 ad2antrr φ y B K G y < ˙ L y x A L : B C
59 58 55 ffvelrnd φ y B K G y < ˙ L y x A L F x C
60 6 ad2antrr φ y B K G y < ˙ L y x A V Proset
61 12 ad2antrr Could not format ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> K e. ( V Monot X ) ) : No typesetting found for |- ( ( ( ph /\ A. y e. B ( K ` ( G ` y ) ) .< ( L ` y ) ) /\ x e. A ) -> K e. ( V Monot X ) ) with typecode |-
62 7 ad2antrr φ y B K G y < ˙ L y x A W Proset
63 8 ad2antrr φ y B K G y < ˙ L y x A F H G
64 1 2 3 4 5 60 62 63 51 mgccole1 φ y B K G y < ˙ L y x A x ˙ G F x
65 1 9 3 10 60 49 61 51 56 64 ismntd φ y B K G y < ˙ L y x A K x < ˙ K G F x
66 25 ffvelrnda φ x A F x 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 φ x A y = F x K G y < ˙ L y K G F x < ˙ L F x
71 66 70 rspcdv φ x A y B K G y < ˙ L y K G F x < ˙ L F x
72 71 imp φ x A y B K G y < ˙ L y K G F x < ˙ L F x
73 72 an32s φ y B K G y < ˙ L y x A K G F x < ˙ L F x
74 9 10 prstr X Proset K x C K G F x C L F x 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 φ y B K G y < ˙ L y x A K x < ˙ L F x
76 75 ralrimiva φ y B K G y < ˙ L y x A K x < ˙ L F x
77 48 76 impbida φ x A K x < ˙ L F x y B K G y < ˙ L y