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