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 ⊢ H = V MGalConn W
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 ⊢ φ → K ∈ V Monot X
mgcmntco.5 ⊢ φ → L ∈ W Monot X
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 ⊢ H = V MGalConn W
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 ⊢ φ → K ∈ V Monot X
13 mgcmntco.5 ⊢ φ → L ∈ W Monot X
14 11 ad2antrr ⊢ φ ∧ ∀ x ∈ A K ⁡ x < ˙ L ⁡ F ⁡ x ∧ y ∈ B → X ∈ Proset
15 1 9 mntf ⊢ V ∈ Proset ∧ X ∈ Proset ∧ K ∈ V Monot X → K : A ⟶ C
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 ffvelcdmda ⊢ φ ∧ ∀ x ∈ A K ⁡ x < ˙ L ⁡ F ⁡ x ∧ y ∈ B → G ⁡ y ∈ A
21 17 20 ffvelcdmd ⊢ φ ∧ ∀ x ∈ A K ⁡ x < ˙ L ⁡ F ⁡ x ∧ y ∈ B → K ⁡ G ⁡ y ∈ C
22 2 9 mntf ⊢ W ∈ Proset ∧ X ∈ Proset ∧ L ∈ W Monot X → L : B ⟶ C
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 ffvelcdmd ⊢ φ ∧ ∀ x ∈ A K ⁡ x < ˙ L ⁡ F ⁡ x ∧ y ∈ B → F ⁡ G ⁡ y ∈ B
28 24 27 ffvelcdmd ⊢ φ ∧ ∀ 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 ffvelcdmda ⊢ φ ∧ ∀ x ∈ A K ⁡ x < ˙ L ⁡ F ⁡ x ∧ y ∈ B → L ⁡ y ∈ C
31 18 ffvelcdmda ⊢ φ ∧ 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 ⊢ φ ∧ ∀ x ∈ A K ⁡ x < ˙ L ⁡ F ⁡ x ∧ y ∈ B → L ∈ W Monot X
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 ffvelcdmd ⊢ φ ∧ ∀ 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 ffvelcdmda ⊢ φ ∧ ∀ y ∈ B K ⁡ G ⁡ y < ˙ L ⁡ y ∧ x ∈ A → F ⁡ x ∈ B
56 53 55 ffvelcdmd ⊢ φ ∧ ∀ y ∈ B K ⁡ G ⁡ y < ˙ L ⁡ y ∧ x ∈ A → G ⁡ F ⁡ x ∈ A
57 50 56 ffvelcdmd ⊢ φ ∧ ∀ 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 ffvelcdmd ⊢ φ ∧ ∀ 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 ⊢ φ ∧ ∀ y ∈ B K ⁡ G ⁡ y < ˙ L ⁡ y ∧ x ∈ A → K ∈ V Monot X
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 ffvelcdmda ⊢ φ ∧ 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