Step | Hyp | Ref
| Expression |
1 | | suprnmpt.c |
. . 3
⊢ 𝐶 = sup(ran 𝐹, ℝ, < ) |
2 | | suprnmpt.b |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
3 | 2 | ralrimiva 3179 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ ℝ) |
4 | | suprnmpt.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
5 | 4 | rnmptss 6878 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ ℝ → ran 𝐹 ⊆ ℝ) |
6 | 3, 5 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
7 | | nfv 1906 |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
8 | | nfmpt1 5155 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
9 | 4, 8 | nfcxfr 2972 |
. . . . . . 7
⊢
Ⅎ𝑥𝐹 |
10 | 9 | nfrn 5817 |
. . . . . 6
⊢
Ⅎ𝑥ran
𝐹 |
11 | | nfcv 2974 |
. . . . . 6
⊢
Ⅎ𝑥∅ |
12 | 10, 11 | nfne 3116 |
. . . . 5
⊢
Ⅎ𝑥ran 𝐹 ≠ ∅ |
13 | | suprnmpt.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ ∅) |
14 | | n0 4307 |
. . . . . 6
⊢ (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
15 | 13, 14 | sylib 219 |
. . . . 5
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) |
16 | | simpr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
17 | 4 | elrnmpt1 5823 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ran 𝐹) |
18 | 16, 2, 17 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran 𝐹) |
19 | 18 | ne0d 4298 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝐹 ≠ ∅) |
20 | 7, 12, 15, 19 | exlimdd 2210 |
. . . 4
⊢ (𝜑 → ran 𝐹 ≠ ∅) |
21 | | suprnmpt.bnd |
. . . . 5
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
22 | | nfv 1906 |
. . . . . 6
⊢
Ⅎ𝑦𝜑 |
23 | | nfre1 3303 |
. . . . . 6
⊢
Ⅎ𝑦∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 |
24 | | simp2 1129 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → 𝑦 ∈ ℝ) |
25 | | simpl1 1183 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran 𝐹) → 𝜑) |
26 | | simpl3 1185 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran 𝐹) → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
27 | | vex 3495 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
28 | 4 | elrnmpt 5821 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V → (𝑧 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
29 | 27, 28 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
30 | 29 | biimpi 217 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
31 | 30 | adantl 482 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran 𝐹) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
32 | | simp3 1130 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
33 | | nfra1 3216 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 |
34 | | nfre1 3303 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑧 = 𝐵 |
35 | 7, 33, 34 | nf3an 1893 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
36 | | nfv 1906 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥 𝑧 ≤ 𝑦 |
37 | | simp3 1130 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵) |
38 | | rspa 3203 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑦) |
39 | 38 | 3adant3 1124 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝐵 ≤ 𝑦) |
40 | 37, 39 | eqbrtrd 5079 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑧 ≤ 𝑦) |
41 | 40 | 3exp 1111 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 → (𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑧 ≤ 𝑦))) |
42 | 41 | 3ad2ant2 1126 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → (𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑧 ≤ 𝑦))) |
43 | 35, 36, 42 | rexlimd 3314 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝑦)) |
44 | 32, 43 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → 𝑧 ≤ 𝑦) |
45 | 25, 26, 31, 44 | syl3anc 1363 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran 𝐹) → 𝑧 ≤ 𝑦) |
46 | 45 | ralrimiva 3179 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) |
47 | | 19.8a 2170 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) → ∃𝑦(𝑦 ∈ ℝ ∧ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦)) |
48 | 24, 46, 47 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑦(𝑦 ∈ ℝ ∧ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦)) |
49 | | df-rex 3141 |
. . . . . . . 8
⊢
(∃𝑦 ∈
ℝ ∀𝑧 ∈
ran 𝐹 𝑧 ≤ 𝑦 ↔ ∃𝑦(𝑦 ∈ ℝ ∧ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦)) |
50 | 48, 49 | sylibr 235 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) |
51 | 50 | 3exp 1111 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ℝ → (∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦))) |
52 | 22, 23, 51 | rexlimd 3314 |
. . . . 5
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦)) |
53 | 21, 52 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) |
54 | | suprcl 11589 |
. . . 4
⊢ ((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑦 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
55 | 6, 20, 53, 54 | syl3anc 1363 |
. . 3
⊢ (𝜑 → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
56 | 1, 55 | eqeltrid 2914 |
. 2
⊢ (𝜑 → 𝐶 ∈ ℝ) |
57 | 6 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝐹 ⊆ ℝ) |
58 | 53 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) |
59 | | suprub 11590 |
. . . . 5
⊢ (((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑦 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) ∧ 𝐵 ∈ ran 𝐹) → 𝐵 ≤ sup(ran 𝐹, ℝ, < )) |
60 | 57, 19, 58, 18, 59 | syl31anc 1365 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ sup(ran 𝐹, ℝ, < )) |
61 | 60, 1 | breqtrrdi 5099 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶) |
62 | 61 | ralrimiva 3179 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶) |
63 | 56, 62 | jca 512 |
1
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) |