Step | Hyp | Ref
| Expression |
1 | | suprnmpt.c |
. . 3
⊢ 𝐶 = sup(ran 𝐹, ℝ, < ) |
2 | | suprnmpt.b |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
3 | 2 | ralrimiva 3149 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ ℝ) |
4 | | suprnmpt.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
5 | 4 | rnmptss 6863 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ ℝ → ran 𝐹 ⊆ ℝ) |
6 | 3, 5 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
7 | | nfv 1915 |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
8 | | nfmpt1 5128 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
9 | 4, 8 | nfcxfr 2953 |
. . . . . . 7
⊢
Ⅎ𝑥𝐹 |
10 | 9 | nfrn 5788 |
. . . . . 6
⊢
Ⅎ𝑥ran
𝐹 |
11 | | nfcv 2955 |
. . . . . 6
⊢
Ⅎ𝑥∅ |
12 | 10, 11 | nfne 3087 |
. . . . 5
⊢
Ⅎ𝑥ran 𝐹 ≠ ∅ |
13 | | suprnmpt.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ ∅) |
14 | | n0 4260 |
. . . . . 6
⊢ (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
15 | 13, 14 | sylib 221 |
. . . . 5
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) |
16 | | simpr 488 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
17 | 4 | elrnmpt1 5794 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ran 𝐹) |
18 | 16, 2, 17 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran 𝐹) |
19 | 18 | ne0d 4251 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝐹 ≠ ∅) |
20 | 7, 12, 15, 19 | exlimdd 2218 |
. . . 4
⊢ (𝜑 → ran 𝐹 ≠ ∅) |
21 | | suprnmpt.bnd |
. . . . 5
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
22 | | nfv 1915 |
. . . . . 6
⊢
Ⅎ𝑦𝜑 |
23 | | nfre1 3265 |
. . . . . 6
⊢
Ⅎ𝑦∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 |
24 | | simp2 1134 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → 𝑦 ∈ ℝ) |
25 | | simpl1 1188 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran 𝐹) → 𝜑) |
26 | | simpl3 1190 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran 𝐹) → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
27 | | vex 3444 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
28 | 4 | elrnmpt 5792 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V → (𝑧 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
30 | 29 | biimpi 219 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
31 | 30 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran 𝐹) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
32 | | simp3 1135 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
33 | | nfra1 3183 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 |
34 | | nfre1 3265 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑧 = 𝐵 |
35 | 7, 33, 34 | nf3an 1902 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
36 | | nfv 1915 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥 𝑧 ≤ 𝑦 |
37 | | simp3 1135 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵) |
38 | | rspa 3171 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑦) |
39 | 38 | 3adant3 1129 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝐵 ≤ 𝑦) |
40 | 37, 39 | eqbrtrd 5052 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑧 ≤ 𝑦) |
41 | 40 | 3exp 1116 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 → (𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑧 ≤ 𝑦))) |
42 | 41 | 3ad2ant2 1131 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → (𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑧 ≤ 𝑦))) |
43 | 35, 36, 42 | rexlimd 3276 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝑦)) |
44 | 32, 43 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → 𝑧 ≤ 𝑦) |
45 | 25, 26, 31, 44 | syl3anc 1368 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran 𝐹) → 𝑧 ≤ 𝑦) |
46 | 45 | ralrimiva 3149 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) |
47 | | 19.8a 2178 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) → ∃𝑦(𝑦 ∈ ℝ ∧ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦)) |
48 | 24, 46, 47 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑦(𝑦 ∈ ℝ ∧ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦)) |
49 | | df-rex 3112 |
. . . . . . . 8
⊢
(∃𝑦 ∈
ℝ ∀𝑧 ∈
ran 𝐹 𝑧 ≤ 𝑦 ↔ ∃𝑦(𝑦 ∈ ℝ ∧ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦)) |
50 | 48, 49 | sylibr 237 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) |
51 | 50 | 3exp 1116 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ℝ → (∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦))) |
52 | 22, 23, 51 | rexlimd 3276 |
. . . . 5
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦)) |
53 | 21, 52 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) |
54 | | suprcl 11588 |
. . . 4
⊢ ((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑦 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
55 | 6, 20, 53, 54 | syl3anc 1368 |
. . 3
⊢ (𝜑 → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
56 | 1, 55 | eqeltrid 2894 |
. 2
⊢ (𝜑 → 𝐶 ∈ ℝ) |
57 | 6 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝐹 ⊆ ℝ) |
58 | 53 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) |
59 | | suprub 11589 |
. . . . 5
⊢ (((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑦 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) ∧ 𝐵 ∈ ran 𝐹) → 𝐵 ≤ sup(ran 𝐹, ℝ, < )) |
60 | 57, 19, 58, 18, 59 | syl31anc 1370 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ sup(ran 𝐹, ℝ, < )) |
61 | 60, 1 | breqtrrdi 5072 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶) |
62 | 61 | ralrimiva 3149 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶) |
63 | 56, 62 | jca 515 |
1
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) |