| Step | Hyp | Ref
| Expression |
| 1 | | uzublem.7 |
. . 3
⊢ 𝑋 = if(𝑊 ≤ 𝑌, 𝑌, 𝑊) |
| 2 | | uzublem.5 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ ℝ) |
| 3 | | uzublem.6 |
. . . . . 6
⊢ 𝑊 = sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < ) |
| 4 | 3 | a1i 11 |
. . . . 5
⊢ (𝜑 → 𝑊 = sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < )) |
| 5 | | uzublem.1 |
. . . . . 6
⊢
Ⅎ𝑗𝜑 |
| 6 | | ltso 11341 |
. . . . . . 7
⊢ < Or
ℝ |
| 7 | 6 | a1i 11 |
. . . . . 6
⊢ (𝜑 → < Or
ℝ) |
| 8 | | fzfid 14014 |
. . . . . 6
⊢ (𝜑 → (𝑀...𝐾) ∈ Fin) |
| 9 | | uzublem.3 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ∈ ℤ) |
| 10 | | uzublem.8 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ 𝑍) |
| 11 | | uzublem.4 |
. . . . . . . . . 10
⊢ 𝑍 =
(ℤ≥‘𝑀) |
| 12 | 11 | eluzelz2 45414 |
. . . . . . . . 9
⊢ (𝐾 ∈ 𝑍 → 𝐾 ∈ ℤ) |
| 13 | 10, 12 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐾 ∈ ℤ) |
| 14 | 9 | zred 12722 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ∈ ℝ) |
| 15 | 14 | leidd 11829 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ≤ 𝑀) |
| 16 | 10, 11 | eleqtrdi 2851 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ (ℤ≥‘𝑀)) |
| 17 | | eluzle 12891 |
. . . . . . . . 9
⊢ (𝐾 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝐾) |
| 18 | 16, 17 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑀 ≤ 𝐾) |
| 19 | 9, 13, 9, 15, 18 | elfzd 13555 |
. . . . . . 7
⊢ (𝜑 → 𝑀 ∈ (𝑀...𝐾)) |
| 20 | 19 | ne0d 4342 |
. . . . . 6
⊢ (𝜑 → (𝑀...𝐾) ≠ ∅) |
| 21 | | fzssuz 13605 |
. . . . . . . . 9
⊢ (𝑀...𝐾) ⊆
(ℤ≥‘𝑀) |
| 22 | 11 | eqcomi 2746 |
. . . . . . . . 9
⊢
(ℤ≥‘𝑀) = 𝑍 |
| 23 | 21, 22 | sseqtri 4032 |
. . . . . . . 8
⊢ (𝑀...𝐾) ⊆ 𝑍 |
| 24 | | id 22 |
. . . . . . . 8
⊢ (𝑗 ∈ (𝑀...𝐾) → 𝑗 ∈ (𝑀...𝐾)) |
| 25 | 23, 24 | sselid 3981 |
. . . . . . 7
⊢ (𝑗 ∈ (𝑀...𝐾) → 𝑗 ∈ 𝑍) |
| 26 | | uzublem.9 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐵 ∈ ℝ) |
| 27 | 25, 26 | sylan2 593 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝐾)) → 𝐵 ∈ ℝ) |
| 28 | 5, 7, 8, 20, 27 | fisupclrnmpt 45409 |
. . . . 5
⊢ (𝜑 → sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
| 29 | 4, 28 | eqeltrd 2841 |
. . . 4
⊢ (𝜑 → 𝑊 ∈ ℝ) |
| 30 | 2, 29 | ifcld 4572 |
. . 3
⊢ (𝜑 → if(𝑊 ≤ 𝑌, 𝑌, 𝑊) ∈ ℝ) |
| 31 | 1, 30 | eqeltrid 2845 |
. 2
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 32 | 26 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝐵 ∈ ℝ) |
| 33 | 2 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑌 ∈ ℝ) |
| 34 | 31 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑋 ∈ ℝ) |
| 35 | | uzublem.10 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ (ℤ≥‘𝐾)𝐵 ≤ 𝑌) |
| 36 | 35 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → ∀𝑗 ∈ (ℤ≥‘𝐾)𝐵 ≤ 𝑌) |
| 37 | | eqid 2737 |
. . . . . . . 8
⊢
(ℤ≥‘𝐾) = (ℤ≥‘𝐾) |
| 38 | 13 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝐾 ∈ ℤ) |
| 39 | 11 | eluzelz2 45414 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℤ) |
| 40 | 39 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑗 ∈ ℤ) |
| 41 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝐾 ≤ 𝑗) |
| 42 | 37, 38, 40, 41 | eluzd 45420 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑗 ∈ (ℤ≥‘𝐾)) |
| 43 | | rspa 3248 |
. . . . . . 7
⊢
((∀𝑗 ∈
(ℤ≥‘𝐾)𝐵 ≤ 𝑌 ∧ 𝑗 ∈ (ℤ≥‘𝐾)) → 𝐵 ≤ 𝑌) |
| 44 | 36, 42, 43 | syl2anc 584 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝐵 ≤ 𝑌) |
| 45 | | max2 13229 |
. . . . . . . . 9
⊢ ((𝑊 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑌 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
| 46 | 29, 2, 45 | syl2anc 584 |
. . . . . . . 8
⊢ (𝜑 → 𝑌 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
| 47 | 46, 1 | breqtrrdi 5185 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ≤ 𝑋) |
| 48 | 47 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝑌 ≤ 𝑋) |
| 49 | 32, 33, 34, 44, 48 | letrd 11418 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝐾 ≤ 𝑗) → 𝐵 ≤ 𝑋) |
| 50 | | simpr 484 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝐾 ≤ 𝑗) → ¬ 𝐾 ≤ 𝑗) |
| 51 | | uzssre 12900 |
. . . . . . . . . . 11
⊢
(ℤ≥‘𝑀) ⊆ ℝ |
| 52 | 11, 51 | eqsstri 4030 |
. . . . . . . . . 10
⊢ 𝑍 ⊆
ℝ |
| 53 | 52 | sseli 3979 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ ℝ) |
| 54 | 53 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝐾 ≤ 𝑗) → 𝑗 ∈ ℝ) |
| 55 | 52, 10 | sselid 3981 |
. . . . . . . . 9
⊢ (𝜑 → 𝐾 ∈ ℝ) |
| 56 | 55 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝐾 ≤ 𝑗) → 𝐾 ∈ ℝ) |
| 57 | 54, 56 | ltnled 11408 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝐾 ≤ 𝑗) → (𝑗 < 𝐾 ↔ ¬ 𝐾 ≤ 𝑗)) |
| 58 | 50, 57 | mpbird 257 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝐾 ≤ 𝑗) → 𝑗 < 𝐾) |
| 59 | 26 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝐵 ∈ ℝ) |
| 60 | 3, 29 | eqeltrrid 2846 |
. . . . . . . . 9
⊢ (𝜑 → sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < ) ∈
ℝ) |
| 61 | 3, 60 | eqeltrid 2845 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ∈ ℝ) |
| 62 | 61 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝑊 ∈ ℝ) |
| 63 | 2, 61 | ifcld 4572 |
. . . . . . . . 9
⊢ (𝜑 → if(𝑊 ≤ 𝑌, 𝑌, 𝑊) ∈ ℝ) |
| 64 | 1, 63 | eqeltrid 2845 |
. . . . . . . 8
⊢ (𝜑 → 𝑋 ∈ ℝ) |
| 65 | 64 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝑋 ∈ ℝ) |
| 66 | | simpll 767 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝜑) |
| 67 | 9 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝑀 ∈ ℤ) |
| 68 | 13 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝐾 ∈ ℤ) |
| 69 | 11 | eleq2i 2833 |
. . . . . . . . . . . . . 14
⊢ (𝑗 ∈ 𝑍 ↔ 𝑗 ∈ (ℤ≥‘𝑀)) |
| 70 | 69 | biimpi 216 |
. . . . . . . . . . . . 13
⊢ (𝑗 ∈ 𝑍 → 𝑗 ∈ (ℤ≥‘𝑀)) |
| 71 | 70 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝑗 ∈ (ℤ≥‘𝑀)) |
| 72 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝑗 < 𝐾) |
| 73 | 71, 68, 72 | elfzod 45411 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝑗 ∈ (𝑀..^𝐾)) |
| 74 | | elfzouz 13703 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈ (𝑀..^𝐾) → 𝑗 ∈ (ℤ≥‘𝑀)) |
| 75 | 74, 22 | eleqtrdi 2851 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ (𝑀..^𝐾) → 𝑗 ∈ 𝑍) |
| 76 | 73, 75, 39 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝑗 ∈ ℤ) |
| 77 | | eluzle 12891 |
. . . . . . . . . . . 12
⊢ (𝑗 ∈
(ℤ≥‘𝑀) → 𝑀 ≤ 𝑗) |
| 78 | 70, 77 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 𝑍 → 𝑀 ≤ 𝑗) |
| 79 | 78 | ad2antlr 727 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝑀 ≤ 𝑗) |
| 80 | 73, 75, 53 | 3syl 18 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝑗 ∈ ℝ) |
| 81 | 55 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝐾 ∈ ℝ) |
| 82 | 80, 81, 72 | ltled 11409 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝑗 ≤ 𝐾) |
| 83 | 67, 68, 76, 79, 82 | elfzd 13555 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝑗 ∈ (𝑀...𝐾)) |
| 84 | 5, 27 | ralrimia 3258 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑗 ∈ (𝑀...𝐾)𝐵 ∈ ℝ) |
| 85 | | fimaxre3 12214 |
. . . . . . . . . . 11
⊢ (((𝑀...𝐾) ∈ Fin ∧ ∀𝑗 ∈ (𝑀...𝐾)𝐵 ∈ ℝ) → ∃𝑦 ∈ ℝ ∀𝑗 ∈ (𝑀...𝐾)𝐵 ≤ 𝑦) |
| 86 | 8, 84, 85 | syl2anc 584 |
. . . . . . . . . 10
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑗 ∈ (𝑀...𝐾)𝐵 ≤ 𝑦) |
| 87 | 5, 27, 86 | suprubrnmpt 45260 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ (𝑀...𝐾)) → 𝐵 ≤ sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < )) |
| 88 | 66, 83, 87 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝐵 ≤ sup(ran (𝑗 ∈ (𝑀...𝐾) ↦ 𝐵), ℝ, < )) |
| 89 | 88, 3 | breqtrrdi 5185 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝐵 ≤ 𝑊) |
| 90 | | max1 13227 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ ℝ ∧ 𝑌 ∈ ℝ) → 𝑊 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
| 91 | 29, 2, 90 | syl2anc 584 |
. . . . . . . . 9
⊢ (𝜑 → 𝑊 ≤ if(𝑊 ≤ 𝑌, 𝑌, 𝑊)) |
| 92 | 91, 1 | breqtrrdi 5185 |
. . . . . . . 8
⊢ (𝜑 → 𝑊 ≤ 𝑋) |
| 93 | 92 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝑊 ≤ 𝑋) |
| 94 | 59, 62, 65, 89, 93 | letrd 11418 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ 𝑗 < 𝐾) → 𝐵 ≤ 𝑋) |
| 95 | 58, 94 | syldan 591 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝑍) ∧ ¬ 𝐾 ≤ 𝑗) → 𝐵 ≤ 𝑋) |
| 96 | 49, 95 | pm2.61dan 813 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → 𝐵 ≤ 𝑋) |
| 97 | 96 | ex 412 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝑍 → 𝐵 ≤ 𝑋)) |
| 98 | 5, 97 | ralrimi 3257 |
. 2
⊢ (𝜑 → ∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑋) |
| 99 | | nfv 1914 |
. . 3
⊢
Ⅎ𝑥∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑋 |
| 100 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑗𝑥 |
| 101 | | uzublem.2 |
. . . . 5
⊢
Ⅎ𝑗𝑋 |
| 102 | 100, 101 | nfeq 2919 |
. . . 4
⊢
Ⅎ𝑗 𝑥 = 𝑋 |
| 103 | | breq2 5147 |
. . . 4
⊢ (𝑥 = 𝑋 → (𝐵 ≤ 𝑥 ↔ 𝐵 ≤ 𝑋)) |
| 104 | 102, 103 | ralbid 3273 |
. . 3
⊢ (𝑥 = 𝑋 → (∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑥 ↔ ∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑋)) |
| 105 | 99, 104 | rspce 3611 |
. 2
⊢ ((𝑋 ∈ ℝ ∧
∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑋) → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑥) |
| 106 | 31, 98, 105 | syl2anc 584 |
1
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑗 ∈ 𝑍 𝐵 ≤ 𝑥) |