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