Metamath Proof Explorer

Theorem pmltpclem2

Description: Lemma for pmltpc . (Contributed by Mario Carneiro, 1-Jul-2014)

Ref Expression
Hypotheses pmltpc.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ℝ ↑pm ℝ ) )
pmltpc.2 ⊢ ( 𝜑 → 𝐴 ⊆ dom 𝐹 )
pmltpc.3 ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
pmltpc.4 ⊢ ( 𝜑 → 𝑉 ∈ 𝐴 )
pmltpc.5 ⊢ ( 𝜑 → 𝑊 ∈ 𝐴 )
pmltpc.6 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
pmltpc.7 ⊢ ( 𝜑 → 𝑈 ≤ 𝑉 )
pmltpc.8 ⊢ ( 𝜑 → 𝑊 ≤ 𝑋 )
pmltpc.9 ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑉 ) )
pmltpc.10 ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝑋 ) ≤ ( 𝐹 ‘ 𝑊 ) )
Assertion pmltpclem2 ( 𝜑 → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pmltpc.1 ⊢ ( 𝜑 → 𝐹 ∈ ( ℝ ↑pm ℝ ) )
2 pmltpc.2 ⊢ ( 𝜑 → 𝐴 ⊆ dom 𝐹 )
3 pmltpc.3 ⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
4 pmltpc.4 ⊢ ( 𝜑 → 𝑉 ∈ 𝐴 )
5 pmltpc.5 ⊢ ( 𝜑 → 𝑊 ∈ 𝐴 )
6 pmltpc.6 ⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
7 pmltpc.7 ⊢ ( 𝜑 → 𝑈 ≤ 𝑉 )
8 pmltpc.8 ⊢ ( 𝜑 → 𝑊 ≤ 𝑋 )
9 pmltpc.9 ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑉 ) )
10 pmltpc.10 ⊢ ( 𝜑 → ¬ ( 𝐹 ‘ 𝑋 ) ≤ ( 𝐹 ‘ 𝑊 ) )
11 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑊 < 𝑈 ) → 𝑊 ∈ 𝐴 )
12 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑊 < 𝑈 ) → 𝑈 ∈ 𝐴 )
13 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑊 < 𝑈 ) → 𝑉 ∈ 𝐴 )
14 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑊 < 𝑈 ) → 𝑊 < 𝑈 )
15 reex ⊢ ℝ ∈ V
16 15 15 elpm2 ⊢ ( 𝐹 ∈ ( ℝ ↑pm ℝ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℝ ∧ dom 𝐹 ⊆ ℝ ) )
17 1 16 sylib ⊢ ( 𝜑 → ( 𝐹 : dom 𝐹 ⟶ ℝ ∧ dom 𝐹 ⊆ ℝ ) )
18 17 simprd ⊢ ( 𝜑 → dom 𝐹 ⊆ ℝ )
19 2 3 sseldd ⊢ ( 𝜑 → 𝑈 ∈ dom 𝐹 )
20 18 19 sseldd ⊢ ( 𝜑 → 𝑈 ∈ ℝ )
21 2 4 sseldd ⊢ ( 𝜑 → 𝑉 ∈ dom 𝐹 )
22 18 21 sseldd ⊢ ( 𝜑 → 𝑉 ∈ ℝ )
23 17 simpld ⊢ ( 𝜑 → 𝐹 : dom 𝐹 ⟶ ℝ )
24 23 21 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑉 ) ∈ ℝ )
25 23 19 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑈 ) ∈ ℝ )
26 24 25 ltnled ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑈 ) ↔ ¬ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑉 ) ) )
27 9 26 mpbird ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑈 ) )
28 24 27 gtned ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑈 ) ≠ ( 𝐹 ‘ 𝑉 ) )
29 fveq2 ⊢ ( 𝑉 = 𝑈 → ( 𝐹 ‘ 𝑉 ) = ( 𝐹 ‘ 𝑈 ) )
30 29 eqcomd ⊢ ( 𝑉 = 𝑈 → ( 𝐹 ‘ 𝑈 ) = ( 𝐹 ‘ 𝑉 ) )
31 30 necon3i ⊢ ( ( 𝐹 ‘ 𝑈 ) ≠ ( 𝐹 ‘ 𝑉 ) → 𝑉 ≠ 𝑈 )
32 28 31 syl ⊢ ( 𝜑 → 𝑉 ≠ 𝑈 )
33 20 22 7 32 leneltd ⊢ ( 𝜑 → 𝑈 < 𝑉 )
34 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑊 < 𝑈 ) → 𝑈 < 𝑉 )
35 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑊 < 𝑈 ) → ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) )
36 27 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑊 < 𝑈 ) → ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑈 ) )
37 35 36 jca ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑊 < 𝑈 ) → ( ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ∧ ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑈 ) ) )
38 37 orcd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑊 < 𝑈 ) → ( ( ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ∧ ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑈 ) ) ∨ ( ( 𝐹 ‘ 𝑈 ) < ( 𝐹 ‘ 𝑊 ) ∧ ( 𝐹 ‘ 𝑈 ) < ( 𝐹 ‘ 𝑉 ) ) ) )
39 11 12 13 14 34 38 pmltpclem1 ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑊 < 𝑈 ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )
40 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → 𝑈 ∈ 𝐴 )
41 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → 𝑊 ∈ 𝐴 )
42 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → 𝑋 ∈ 𝐴 )
43 20 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → 𝑈 ∈ ℝ )
44 2 5 sseldd ⊢ ( 𝜑 → 𝑊 ∈ dom 𝐹 )
45 18 44 sseldd ⊢ ( 𝜑 → 𝑊 ∈ ℝ )
46 45 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → 𝑊 ∈ ℝ )
47 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → 𝑈 ≤ 𝑊 )
48 23 44 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑊 ) ∈ ℝ )
49 48 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → ( 𝐹 ‘ 𝑊 ) ∈ ℝ )
50 simplr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) )
51 49 50 gtned ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → ( 𝐹 ‘ 𝑈 ) ≠ ( 𝐹 ‘ 𝑊 ) )
52 fveq2 ⊢ ( 𝑊 = 𝑈 → ( 𝐹 ‘ 𝑊 ) = ( 𝐹 ‘ 𝑈 ) )
53 52 eqcomd ⊢ ( 𝑊 = 𝑈 → ( 𝐹 ‘ 𝑈 ) = ( 𝐹 ‘ 𝑊 ) )
54 53 necon3i ⊢ ( ( 𝐹 ‘ 𝑈 ) ≠ ( 𝐹 ‘ 𝑊 ) → 𝑊 ≠ 𝑈 )
55 51 54 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → 𝑊 ≠ 𝑈 )
56 43 46 47 55 leneltd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → 𝑈 < 𝑊 )
57 2 6 sseldd ⊢ ( 𝜑 → 𝑋 ∈ dom 𝐹 )
58 18 57 sseldd ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
59 23 57 ffvelcdmd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ∈ ℝ )
60 48 59 ltnled ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑋 ) ↔ ¬ ( 𝐹 ‘ 𝑋 ) ≤ ( 𝐹 ‘ 𝑊 ) ) )
61 10 60 mpbird ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑋 ) )
62 48 61 gtned ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑊 ) )
63 fveq2 ⊢ ( 𝑋 = 𝑊 → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑊 ) )
64 63 necon3i ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑊 ) → 𝑋 ≠ 𝑊 )
65 62 64 syl ⊢ ( 𝜑 → 𝑋 ≠ 𝑊 )
66 45 58 8 65 leneltd ⊢ ( 𝜑 → 𝑊 < 𝑋 )
67 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → 𝑊 < 𝑋 )
68 61 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑋 ) )
69 50 68 jca ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → ( ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑋 ) ) )
70 69 olcd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → ( ( ( 𝐹 ‘ 𝑈 ) < ( 𝐹 ‘ 𝑊 ) ∧ ( 𝐹 ‘ 𝑋 ) < ( 𝐹 ‘ 𝑊 ) ) ∨ ( ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑋 ) ) ) )
71 40 41 42 56 67 70 pmltpclem1 ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) ∧ 𝑈 ≤ 𝑊 ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )
72 45 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) → 𝑊 ∈ ℝ )
73 20 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) → 𝑈 ∈ ℝ )
74 39 71 72 73 ltlecasei ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑈 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )
75 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑉 < 𝑋 ) → 𝑈 ∈ 𝐴 )
76 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑉 < 𝑋 ) → 𝑉 ∈ 𝐴 )
77 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑉 < 𝑋 ) → 𝑋 ∈ 𝐴 )
78 33 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑉 < 𝑋 ) → 𝑈 < 𝑉 )
79 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑉 < 𝑋 ) → 𝑉 < 𝑋 )
80 27 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑉 < 𝑋 ) → ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑈 ) )
81 24 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) → ( 𝐹 ‘ 𝑉 ) ∈ ℝ )
82 25 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) → ( 𝐹 ‘ 𝑈 ) ∈ ℝ )
83 59 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) → ( 𝐹 ‘ 𝑋 ) ∈ ℝ )
84 27 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) → ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑈 ) )
85 48 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) → ( 𝐹 ‘ 𝑊 ) ∈ ℝ )
86 simpr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) → ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) )
87 61 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) → ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑋 ) )
88 82 85 83 86 87 lelttrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) → ( 𝐹 ‘ 𝑈 ) < ( 𝐹 ‘ 𝑋 ) )
89 81 82 83 84 88 lttrd ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) → ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑋 ) )
90 89 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑉 < 𝑋 ) → ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑋 ) )
91 80 90 jca ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑉 < 𝑋 ) → ( ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑈 ) ∧ ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑋 ) ) )
92 91 olcd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑉 < 𝑋 ) → ( ( ( 𝐹 ‘ 𝑈 ) < ( 𝐹 ‘ 𝑉 ) ∧ ( 𝐹 ‘ 𝑋 ) < ( 𝐹 ‘ 𝑉 ) ) ∨ ( ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑈 ) ∧ ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑋 ) ) ) )
93 75 76 77 78 79 92 pmltpclem1 ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑉 < 𝑋 ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )
94 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → 𝑊 ∈ 𝐴 )
95 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → 𝑋 ∈ 𝐴 )
96 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → 𝑉 ∈ 𝐴 )
97 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → 𝑊 < 𝑋 )
98 58 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → 𝑋 ∈ ℝ )
99 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → 𝑉 ∈ ℝ )
100 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → 𝑋 ≤ 𝑉 )
101 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → ( 𝐹 ‘ 𝑉 ) ∈ ℝ )
102 89 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑋 ) )
103 101 102 gtned ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑉 ) )
104 fveq2 ⊢ ( 𝑉 = 𝑋 → ( 𝐹 ‘ 𝑉 ) = ( 𝐹 ‘ 𝑋 ) )
105 104 eqcomd ⊢ ( 𝑉 = 𝑋 → ( 𝐹 ‘ 𝑋 ) = ( 𝐹 ‘ 𝑉 ) )
106 105 necon3i ⊢ ( ( 𝐹 ‘ 𝑋 ) ≠ ( 𝐹 ‘ 𝑉 ) → 𝑉 ≠ 𝑋 )
107 103 106 syl ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → 𝑉 ≠ 𝑋 )
108 98 99 100 107 leneltd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → 𝑋 < 𝑉 )
109 61 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑋 ) )
110 109 102 jca ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → ( ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑋 ) ) )
111 110 orcd ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → ( ( ( 𝐹 ‘ 𝑊 ) < ( 𝐹 ‘ 𝑋 ) ∧ ( 𝐹 ‘ 𝑉 ) < ( 𝐹 ‘ 𝑋 ) ) ∨ ( ( 𝐹 ‘ 𝑋 ) < ( 𝐹 ‘ 𝑊 ) ∧ ( 𝐹 ‘ 𝑋 ) < ( 𝐹 ‘ 𝑉 ) ) ) )
112 94 95 96 97 108 111 pmltpclem1 ⊢ ( ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) ∧ 𝑋 ≤ 𝑉 ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )
113 22 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) → 𝑉 ∈ ℝ )
114 58 adantr ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) → 𝑋 ∈ ℝ )
115 93 112 113 114 ltlecasei ⊢ ( ( 𝜑 ∧ ( 𝐹 ‘ 𝑈 ) ≤ ( 𝐹 ‘ 𝑊 ) ) → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )
116 74 115 48 25 ltlecasei ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝐴 ∃ 𝑏 ∈ 𝐴 ∃ 𝑐 ∈ 𝐴 ( 𝑎 < 𝑏 ∧ 𝑏 < 𝑐 ∧ ( ( ( 𝐹 ‘ 𝑎 ) < ( 𝐹 ‘ 𝑏 ) ∧ ( 𝐹 ‘ 𝑐 ) < ( 𝐹 ‘ 𝑏 ) ) ∨ ( ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑎 ) ∧ ( 𝐹 ‘ 𝑏 ) < ( 𝐹 ‘ 𝑐 ) ) ) ) )