Step | Hyp | Ref
| Expression |
1 | | suprnmpt.c |
. . 3
⊢ 𝐶 = sup(ran 𝐹, ℝ, < ) |
2 | | suprnmpt.b |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
3 | 2 | ralrimiva 2949 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ ℝ) |
4 | | suprnmpt.f |
. . . . . 6
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
5 | 4 | rnmptss 6299 |
. . . . 5
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ ℝ → ran 𝐹 ⊆ ℝ) |
6 | 3, 5 | syl 17 |
. . . 4
⊢ (𝜑 → ran 𝐹 ⊆ ℝ) |
7 | | nfv 1830 |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
8 | | nfmpt1 4675 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) |
9 | 4, 8 | nfcxfr 2749 |
. . . . . . 7
⊢
Ⅎ𝑥𝐹 |
10 | 9 | nfrn 5289 |
. . . . . 6
⊢
Ⅎ𝑥ran
𝐹 |
11 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑥∅ |
12 | 10, 11 | nfne 2882 |
. . . . 5
⊢
Ⅎ𝑥ran 𝐹 ≠ ∅ |
13 | | suprnmpt.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ≠ ∅) |
14 | | n0 3890 |
. . . . . 6
⊢ (𝐴 ≠ ∅ ↔
∃𝑥 𝑥 ∈ 𝐴) |
15 | 13, 14 | sylib 207 |
. . . . 5
⊢ (𝜑 → ∃𝑥 𝑥 ∈ 𝐴) |
16 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
17 | 4 | elrnmpt1 5295 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ℝ) → 𝐵 ∈ ran 𝐹) |
18 | 16, 2, 17 | syl2anc 691 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ran 𝐹) |
19 | | ne0i 3880 |
. . . . . 6
⊢ (𝐵 ∈ ran 𝐹 → ran 𝐹 ≠ ∅) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝐹 ≠ ∅) |
21 | 7, 12, 15, 20 | exlimdd 2075 |
. . . 4
⊢ (𝜑 → ran 𝐹 ≠ ∅) |
22 | | suprnmpt.bnd |
. . . . 5
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
23 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑦𝜑 |
24 | | nfre1 2988 |
. . . . . 6
⊢
Ⅎ𝑦∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦 |
25 | | simp2 1055 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → 𝑦 ∈ ℝ) |
26 | | simpl1 1057 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran 𝐹) → 𝜑) |
27 | | simpl3 1059 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran 𝐹) → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) |
28 | | vex 3176 |
. . . . . . . . . . . . . 14
⊢ 𝑧 ∈ V |
29 | 4 | elrnmpt 5293 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ V → (𝑧 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵)) |
30 | 28, 29 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (𝑧 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
31 | 30 | biimpi 205 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ran 𝐹 → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
32 | 31 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran 𝐹) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
33 | | simp3 1056 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
34 | | nfra1 2925 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 |
35 | | nfre1 2988 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥∃𝑥 ∈ 𝐴 𝑧 = 𝐵 |
36 | 7, 34, 35 | nf3an 1819 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) |
37 | | nfv 1830 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥 𝑧 ≤ 𝑦 |
38 | | simp3 1056 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑧 = 𝐵) |
39 | | rspa 2914 |
. . . . . . . . . . . . . . . . 17
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑦) |
40 | 39 | 3adant3 1074 |
. . . . . . . . . . . . . . . 16
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝐵 ≤ 𝑦) |
41 | 38, 40 | eqbrtrd 4605 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 ∧ 𝑥 ∈ 𝐴 ∧ 𝑧 = 𝐵) → 𝑧 ≤ 𝑦) |
42 | 41 | 3exp 1256 |
. . . . . . . . . . . . . 14
⊢
(∀𝑥 ∈
𝐴 𝐵 ≤ 𝑦 → (𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑧 ≤ 𝑦))) |
43 | 42 | 3ad2ant2 1076 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → (𝑥 ∈ 𝐴 → (𝑧 = 𝐵 → 𝑧 ≤ 𝑦))) |
44 | 36, 37, 43 | rexlimd 3008 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → (∃𝑥 ∈ 𝐴 𝑧 = 𝐵 → 𝑧 ≤ 𝑦)) |
45 | 33, 44 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 ∧ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵) → 𝑧 ≤ 𝑦) |
46 | 26, 27, 32, 45 | syl3anc 1318 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) ∧ 𝑧 ∈ ran 𝐹) → 𝑧 ≤ 𝑦) |
47 | 46 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) |
48 | | 19.8a 2039 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℝ ∧
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) → ∃𝑦(𝑦 ∈ ℝ ∧ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦)) |
49 | 25, 47, 48 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑦(𝑦 ∈ ℝ ∧ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦)) |
50 | | df-rex 2902 |
. . . . . . . 8
⊢
(∃𝑦 ∈
ℝ ∀𝑧 ∈
ran 𝐹 𝑧 ≤ 𝑦 ↔ ∃𝑦(𝑦 ∈ ℝ ∧ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦)) |
51 | 49, 50 | sylibr 223 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) |
52 | 51 | 3exp 1256 |
. . . . . 6
⊢ (𝜑 → (𝑦 ∈ ℝ → (∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦))) |
53 | 23, 24, 52 | rexlimd 3008 |
. . . . 5
⊢ (𝜑 → (∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝑦 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦)) |
54 | 22, 53 | mpd 15 |
. . . 4
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) |
55 | | suprcl 10862 |
. . . 4
⊢ ((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑦 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
56 | 6, 21, 54, 55 | syl3anc 1318 |
. . 3
⊢ (𝜑 → sup(ran 𝐹, ℝ, < ) ∈
ℝ) |
57 | 1, 56 | syl5eqel 2692 |
. 2
⊢ (𝜑 → 𝐶 ∈ ℝ) |
58 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ran 𝐹 ⊆ ℝ) |
59 | 54 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ ℝ ∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) |
60 | | suprub 10863 |
. . . . 5
⊢ (((ran
𝐹 ⊆ ℝ ∧ ran
𝐹 ≠ ∅ ∧
∃𝑦 ∈ ℝ
∀𝑧 ∈ ran 𝐹 𝑧 ≤ 𝑦) ∧ 𝐵 ∈ ran 𝐹) → 𝐵 ≤ sup(ran 𝐹, ℝ, < )) |
61 | 58, 20, 59, 18, 60 | syl31anc 1321 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ sup(ran 𝐹, ℝ, < )) |
62 | 61, 1 | syl6breqr 4625 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝐶) |
63 | 62 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶) |
64 | 57, 63 | jca 553 |
1
⊢ (𝜑 → (𝐶 ∈ ℝ ∧ ∀𝑥 ∈ 𝐴 𝐵 ≤ 𝐶)) |