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 ⊢ 𝐴 = ( Base ‘ 𝑉 )
mgcoval.2 ⊢ 𝐵 = ( Base ‘ 𝑊 )
mgcoval.3 ⊢ ≤ = ( le ‘ 𝑉 )
mgcoval.4 ⊢ ≲ = ( le ‘ 𝑊 )
mgcval.1 ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
mgcval.2 ⊢ ( 𝜑 → 𝑉 ∈ Proset )
mgcval.3 ⊢ ( 𝜑 → 𝑊 ∈ Proset )
mgccole.1 ⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
mgcmntco.1 ⊢ 𝐶 = ( Base ‘ 𝑋 )
mgcmntco.2 ⊢ < = ( le ‘ 𝑋 )
mgcmntco.3 ⊢ ( 𝜑 → 𝑋 ∈ Proset )
mgcmntco.4 ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑉 Monot 𝑋 ) )
mgcmntco.5 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝑊 Monot 𝑋 ) )
Assertion mgcmntco ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) )

Proof

Step Hyp Ref Expression
1 mgcoval.1 ⊢ 𝐴 = ( Base ‘ 𝑉 )
2 mgcoval.2 ⊢ 𝐵 = ( Base ‘ 𝑊 )
3 mgcoval.3 ⊢ ≤ = ( le ‘ 𝑉 )
4 mgcoval.4 ⊢ ≲ = ( le ‘ 𝑊 )
5 mgcval.1 ⊢ 𝐻 = ( 𝑉 MGalConn 𝑊 )
6 mgcval.2 ⊢ ( 𝜑 → 𝑉 ∈ Proset )
7 mgcval.3 ⊢ ( 𝜑 → 𝑊 ∈ Proset )
8 mgccole.1 ⊢ ( 𝜑 → 𝐹 𝐻 𝐺 )
9 mgcmntco.1 ⊢ 𝐶 = ( Base ‘ 𝑋 )
10 mgcmntco.2 ⊢ < = ( le ‘ 𝑋 )
11 mgcmntco.3 ⊢ ( 𝜑 → 𝑋 ∈ Proset )
12 mgcmntco.4 ⊢ ( 𝜑 → 𝐾 ∈ ( 𝑉 Monot 𝑋 ) )
13 mgcmntco.5 ⊢ ( 𝜑 → 𝐿 ∈ ( 𝑊 Monot 𝑋 ) )
14 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑋 ∈ Proset )
15 1 9 mntf ⊢ ( ( 𝑉 ∈ Proset ∧ 𝑋 ∈ Proset ∧ 𝐾 ∈ ( 𝑉 Monot 𝑋 ) ) → 𝐾 : 𝐴 ⟶ 𝐶 )
16 6 11 12 15 syl3anc ⊢ ( 𝜑 → 𝐾 : 𝐴 ⟶ 𝐶 )
17 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝐾 : 𝐴 ⟶ 𝐶 )
18 1 2 3 4 5 6 7 8 mgcf2 ⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐴 )
19 18 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 𝐺 : 𝐵 ⟶ 𝐴 )
20 19 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 )
21 17 20 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ 𝐶 )
22 2 9 mntf ⊢ ( ( 𝑊 ∈ Proset ∧ 𝑋 ∈ Proset ∧ 𝐿 ∈ ( 𝑊 Monot 𝑋 ) ) → 𝐿 : 𝐵 ⟶ 𝐶 )
23 7 11 13 22 syl3anc ⊢ ( 𝜑 → 𝐿 : 𝐵 ⟶ 𝐶 )
24 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝐿 : 𝐵 ⟶ 𝐶 )
25 1 2 3 4 5 6 7 8 mgcf1 ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
27 26 20 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ 𝐵 )
28 24 27 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐿 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ∈ 𝐶 )
29 23 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → 𝐿 : 𝐵 ⟶ 𝐶 )
30 29 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐿 ‘ 𝑦 ) ∈ 𝐶 )
31 18 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝐴 )
32 fveq2 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑦 ) → ( 𝐾 ‘ 𝑥 ) = ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) )
33 2fveq3 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑦 ) → ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) = ( 𝐿 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
34 32 33 breq12d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑦 ) → ( ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) )
35 34 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑥 = ( 𝐺 ‘ 𝑦 ) ) → ( ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) )
36 31 35 rspcdv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ) )
37 36 imp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
38 37 an32s ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) )
39 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑊 ∈ Proset )
40 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝐿 ∈ ( 𝑊 Monot 𝑋 ) )
41 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
42 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝑉 ∈ Proset )
43 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → 𝐹 𝐻 𝐺 )
44 1 2 3 4 5 42 39 43 41 mgccole2 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ≲ 𝑦 )
45 2 9 4 10 39 14 40 27 41 44 ismntd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐿 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) < ( 𝐿 ‘ 𝑦 ) )
46 9 10 prstr ⊢ ( ( 𝑋 ∈ Proset ∧ ( ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) ∈ 𝐶 ∧ ( 𝐿 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ∈ 𝐶 ∧ ( 𝐿 ‘ 𝑦 ) ∈ 𝐶 ) ∧ ( ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) ∧ ( 𝐿 ‘ ( 𝐹 ‘ ( 𝐺 ‘ 𝑦 ) ) ) < ( 𝐿 ‘ 𝑦 ) ) ) → ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) )
47 14 21 28 30 38 45 46 syl132anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ 𝑦 ∈ 𝐵 ) → ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) )
48 47 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) )
49 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑋 ∈ Proset )
50 16 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐾 : 𝐴 ⟶ 𝐶 )
51 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝐴 )
52 50 51 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐾 ‘ 𝑥 ) ∈ 𝐶 )
53 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐺 : 𝐵 ⟶ 𝐴 )
54 25 adantr ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 )
55 54 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
56 53 55 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐴 )
57 50 56 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐾 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐶 )
58 23 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐿 : 𝐵 ⟶ 𝐶 )
59 58 55 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐶 )
60 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑉 ∈ Proset )
61 12 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐾 ∈ ( 𝑉 Monot 𝑋 ) )
62 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑊 ∈ Proset )
63 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝐹 𝐻 𝐺 )
64 1 2 3 4 5 60 62 63 51 mgccole1 ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) )
65 1 9 3 10 60 49 61 51 56 64 ismntd ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐾 ‘ 𝑥 ) < ( 𝐾 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
66 25 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝐵 )
67 2fveq3 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) = ( 𝐾 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
68 fveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝐿 ‘ 𝑦 ) = ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) )
69 67 68 breq12d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ↔ ( 𝐾 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
70 69 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 = ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ↔ ( 𝐾 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
71 66 70 rspcdv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) → ( 𝐾 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) )
72 71 imp ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) → ( 𝐾 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) )
73 72 an32s ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐾 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) )
74 9 10 prstr ⊢ ( ( 𝑋 ∈ Proset ∧ ( ( 𝐾 ‘ 𝑥 ) ∈ 𝐶 ∧ ( 𝐾 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∈ 𝐶 ∧ ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ∈ 𝐶 ) ∧ ( ( 𝐾 ‘ 𝑥 ) < ( 𝐾 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ∧ ( 𝐾 ‘ ( 𝐺 ‘ ( 𝐹 ‘ 𝑥 ) ) ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ) ) → ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) )
75 49 52 57 59 65 73 74 syl132anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) )
76 75 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) )
77 48 76 impbida ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 ( 𝐾 ‘ 𝑥 ) < ( 𝐿 ‘ ( 𝐹 ‘ 𝑥 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝐾 ‘ ( 𝐺 ‘ 𝑦 ) ) < ( 𝐿 ‘ 𝑦 ) ) )