Step | Hyp | Ref
| Expression |
1 | | supadd.a1 |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
2 | | supadd.a2 |
. . . . 5
⊢ (𝜑 → 𝐴 ≠ ∅) |
3 | | supadd.a3 |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
4 | | supadd.b1 |
. . . . . 6
⊢ (𝜑 → 𝐵 ⊆ ℝ) |
5 | | supadd.b2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ≠ ∅) |
6 | | supadd.b3 |
. . . . . 6
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥) |
7 | | suprcl 10862 |
. . . . . 6
⊢ ((𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥) → sup(𝐵, ℝ, < ) ∈
ℝ) |
8 | 4, 5, 6, 7 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → sup(𝐵, ℝ, < ) ∈
ℝ) |
9 | | eqid 2610 |
. . . . 5
⊢ {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))} = {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))} |
10 | 1, 2, 3, 8, 9 | supaddc 10867 |
. . . 4
⊢ (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup({𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}, ℝ, <
)) |
11 | 1 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ ℝ) |
12 | 11 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ ℂ) |
13 | 8 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → sup(𝐵, ℝ, < ) ∈
ℝ) |
14 | 13 | recnd 9947 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → sup(𝐵, ℝ, < ) ∈
ℂ) |
15 | 12, 14 | addcomd 10117 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑎 + sup(𝐵, ℝ, < )) = (sup(𝐵, ℝ, < ) + 𝑎)) |
16 | 15 | eqeq2d 2620 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑧 = (𝑎 + sup(𝐵, ℝ, < )) ↔ 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))) |
17 | 16 | rexbidva 3031 |
. . . . . 6
⊢ (𝜑 → (∃𝑎 ∈ 𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < )) ↔ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎))) |
18 | 17 | abbidv 2728 |
. . . . 5
⊢ (𝜑 → {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))} = {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}) |
19 | 18 | supeq1d 8235 |
. . . 4
⊢ (𝜑 → sup({𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (𝑎 + sup(𝐵, ℝ, < ))}, ℝ, < ) =
sup({𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < )) |
20 | 10, 19 | eqtrd 2644 |
. . 3
⊢ (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup({𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < )) |
21 | | vex 3176 |
. . . . . . 7
⊢ 𝑤 ∈ V |
22 | | eqeq1 2614 |
. . . . . . . 8
⊢ (𝑧 = 𝑤 → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎))) |
23 | 22 | rexbidv 3034 |
. . . . . . 7
⊢ (𝑧 = 𝑤 → (∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ ∃𝑎 ∈ 𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎))) |
24 | 21, 23 | elab 3319 |
. . . . . 6
⊢ (𝑤 ∈ {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ↔ ∃𝑎 ∈ 𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎)) |
25 | 4 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐵 ⊆ ℝ) |
26 | 5 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐵 ≠ ∅) |
27 | 6 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥) |
28 | | eqid 2610 |
. . . . . . . . . . 11
⊢ {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑏 + 𝑎)} = {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑏 + 𝑎)} |
29 | 25, 26, 27, 11, 28 | supaddc 10867 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) = sup({𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑏 + 𝑎)}, ℝ, < )) |
30 | 4 | sselda 3568 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ℝ) |
31 | 30 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ℝ) |
32 | 31 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ ℂ) |
33 | 11 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) → 𝑎 ∈ ℝ) |
34 | 33 | recnd 9947 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) → 𝑎 ∈ ℂ) |
35 | 32, 34 | addcomd 10117 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) → (𝑏 + 𝑎) = (𝑎 + 𝑏)) |
36 | 35 | eqeq2d 2620 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) → (𝑧 = (𝑏 + 𝑎) ↔ 𝑧 = (𝑎 + 𝑏))) |
37 | 36 | rexbidva 3031 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 𝑧 = (𝑏 + 𝑎) ↔ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏))) |
38 | 37 | abbidv 2728 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑏 + 𝑎)} = {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}) |
39 | 38 | supeq1d 8235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → sup({𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑏 + 𝑎)}, ℝ, < ) = sup({𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < )) |
40 | 29, 39 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) = sup({𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < )) |
41 | | eqeq1 2614 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = 𝑤 → (𝑧 = (𝑎 + 𝑏) ↔ 𝑤 = (𝑎 + 𝑏))) |
42 | 41 | rexbidv 3034 |
. . . . . . . . . . . . 13
⊢ (𝑧 = 𝑤 → (∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏))) |
43 | 21, 42 | elab 3319 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)} ↔ ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) |
44 | | rspe 2986 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ 𝐴 ∧ ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) → ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) |
45 | | oveq1 6556 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑣 = 𝑎 → (𝑣 + 𝑏) = (𝑎 + 𝑏)) |
46 | 45 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑣 = 𝑎 → (𝑧 = (𝑣 + 𝑏) ↔ 𝑧 = (𝑎 + 𝑏))) |
47 | 46 | rexbidv 3034 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑣 = 𝑎 → (∃𝑏 ∈ 𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏))) |
48 | 47 | cbvrexv 3148 |
. . . . . . . . . . . . . . . . 17
⊢
(∃𝑣 ∈
𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)) |
49 | 41 | 2rexbidv 3039 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑤 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏))) |
50 | 48, 49 | syl5bb 271 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = 𝑤 → (∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 + 𝑏) ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏))) |
51 | | supadd.c |
. . . . . . . . . . . . . . . 16
⊢ 𝐶 = {𝑧 ∣ ∃𝑣 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑧 = (𝑣 + 𝑏)} |
52 | 21, 50, 51 | elab2 3323 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ 𝐶 ↔ ∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) |
53 | 44, 52 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ 𝐴 ∧ ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) → 𝑤 ∈ 𝐶) |
54 | 53 | ex 449 |
. . . . . . . . . . . . 13
⊢ (𝑎 ∈ 𝐴 → (∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ 𝐶)) |
55 | 1 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑎 ∈ 𝐴 → 𝑎 ∈ ℝ)) |
56 | 4 | sseld 3567 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝑏 ∈ 𝐵 → 𝑏 ∈ ℝ)) |
57 | 55, 56 | anim12d 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ))) |
58 | | readdcl 9898 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 ∈ ℝ ∧ 𝑏 ∈ ℝ) → (𝑎 + 𝑏) ∈ ℝ) |
59 | 57, 58 | syl6 34 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑎 + 𝑏) ∈ ℝ)) |
60 | | eleq1a 2683 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑎 + 𝑏) ∈ ℝ → (𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ)) |
61 | 59, 60 | syl6 34 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ))) |
62 | 61 | rexlimdvv 3019 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ∈ ℝ)) |
63 | 52, 62 | syl5bi 231 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑤 ∈ 𝐶 → 𝑤 ∈ ℝ)) |
64 | 63 | ssrdv 3574 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ⊆ ℝ) |
65 | | ovex 6577 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑎 + 𝑏) ∈ V |
66 | 65 | isseti 3182 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
∃𝑤 𝑤 = (𝑎 + 𝑏) |
67 | 66 | rgenw 2908 |
. . . . . . . . . . . . . . . . . . . 20
⊢
∀𝑏 ∈
𝐵 ∃𝑤 𝑤 = (𝑎 + 𝑏) |
68 | | r19.2z 4012 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ≠ ∅ ∧
∀𝑏 ∈ 𝐵 ∃𝑤 𝑤 = (𝑎 + 𝑏)) → ∃𝑏 ∈ 𝐵 ∃𝑤 𝑤 = (𝑎 + 𝑏)) |
69 | 5, 67, 68 | sylancl 693 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ∃𝑏 ∈ 𝐵 ∃𝑤 𝑤 = (𝑎 + 𝑏)) |
70 | | rexcom4 3198 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃𝑏 ∈
𝐵 ∃𝑤 𝑤 = (𝑎 + 𝑏) ↔ ∃𝑤∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) |
71 | 69, 70 | sylib 207 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∃𝑤∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) |
72 | 71 | ralrimivw 2950 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∃𝑤∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) |
73 | | r19.2z 4012 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ≠ ∅ ∧
∀𝑎 ∈ 𝐴 ∃𝑤∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) → ∃𝑎 ∈ 𝐴 ∃𝑤∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) |
74 | 2, 72, 73 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∃𝑎 ∈ 𝐴 ∃𝑤∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) |
75 | | rexcom4 3198 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑎 ∈
𝐴 ∃𝑤∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏) ↔ ∃𝑤∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) |
76 | 74, 75 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∃𝑤∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) |
77 | | n0 3890 |
. . . . . . . . . . . . . . . 16
⊢ (𝐶 ≠ ∅ ↔
∃𝑤 𝑤 ∈ 𝐶) |
78 | 52 | exbii 1764 |
. . . . . . . . . . . . . . . 16
⊢
(∃𝑤 𝑤 ∈ 𝐶 ↔ ∃𝑤∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) |
79 | 77, 78 | bitri 263 |
. . . . . . . . . . . . . . 15
⊢ (𝐶 ≠ ∅ ↔
∃𝑤∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏)) |
80 | 76, 79 | sylibr 223 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ≠ ∅) |
81 | | suprcl 10862 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈
ℝ) |
82 | 1, 2, 3, 81 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈
ℝ) |
83 | 82, 8 | readdcld 9948 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈
ℝ) |
84 | 11 | adantrr 749 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ ℝ) |
85 | 30 | adantrl 748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ ℝ) |
86 | 82 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → sup(𝐴, ℝ, < ) ∈
ℝ) |
87 | 8 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → sup(𝐵, ℝ, < ) ∈
ℝ) |
88 | 1, 2, 3 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥)) |
89 | | suprub 10863 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑎 ∈ 𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < )) |
90 | 88, 89 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ≤ sup(𝐴, ℝ, < )) |
91 | 90 | adantrr 749 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ≤ sup(𝐴, ℝ, < )) |
92 | 4, 5, 6 | 3jca 1235 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝜑 → (𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥)) |
93 | | suprub 10863 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐵 ⊆ ℝ ∧ 𝐵 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐵 𝑦 ≤ 𝑥) ∧ 𝑏 ∈ 𝐵) → 𝑏 ≤ sup(𝐵, ℝ, < )) |
94 | 92, 93 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ≤ sup(𝐵, ℝ, < )) |
95 | 94 | adantrl 748 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ≤ sup(𝐵, ℝ, < )) |
96 | 84, 85, 86, 87, 91, 95 | le2addd 10525 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵)) → (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))) |
97 | 96 | ex 449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))) |
98 | | breq1 4586 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (𝑎 + 𝑏) → (𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔ (𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))) |
99 | 98 | biimprcd 239 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑎 + 𝑏) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))) |
100 | 97, 99 | syl6 34 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ((𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵) → (𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))))) |
101 | 100 | rexlimdvv 3019 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∃𝑎 ∈ 𝐴 ∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))) |
102 | 52, 101 | syl5bi 231 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → (𝑤 ∈ 𝐶 → 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))) |
103 | 102 | ralrimiv 2948 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑤 ∈ 𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))) |
104 | | breq2 4587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) → (𝑤 ≤ 𝑥 ↔ 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))) |
105 | 104 | ralbidv 2969 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) → (∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥 ↔ ∀𝑤 ∈ 𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))) |
106 | 105 | rspcev 3282 |
. . . . . . . . . . . . . . 15
⊢
(((sup(𝐴, ℝ,
< ) + sup(𝐵, ℝ,
< )) ∈ ℝ ∧ ∀𝑤 ∈ 𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < ))) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥) |
107 | 83, 103, 106 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥) |
108 | | suprub 10863 |
. . . . . . . . . . . . . . 15
⊢ (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥) ∧ 𝑤 ∈ 𝐶) → 𝑤 ≤ sup(𝐶, ℝ, < )) |
109 | 108 | ex 449 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥) → (𝑤 ∈ 𝐶 → 𝑤 ≤ sup(𝐶, ℝ, < ))) |
110 | 64, 80, 107, 109 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑤 ∈ 𝐶 → 𝑤 ≤ sup(𝐶, ℝ, < ))) |
111 | 54, 110 | sylan9r 688 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 𝑤 = (𝑎 + 𝑏) → 𝑤 ≤ sup(𝐶, ℝ, < ))) |
112 | 43, 111 | syl5bi 231 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑤 ∈ {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)} → 𝑤 ≤ sup(𝐶, ℝ, < ))) |
113 | 112 | ralrimiv 2948 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∀𝑤 ∈ {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )) |
114 | 33, 31 | readdcld 9948 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) → (𝑎 + 𝑏) ∈ ℝ) |
115 | | eleq1a 2683 |
. . . . . . . . . . . . . 14
⊢ ((𝑎 + 𝑏) ∈ ℝ → (𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ)) |
116 | 114, 115 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑏 ∈ 𝐵) → (𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ)) |
117 | 116 | rexlimdva 3013 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏) → 𝑧 ∈ ℝ)) |
118 | 117 | abssdv 3639 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)} ⊆ ℝ) |
119 | 65 | isseti 3182 |
. . . . . . . . . . . . . . . 16
⊢
∃𝑧 𝑧 = (𝑎 + 𝑏) |
120 | 119 | rgenw 2908 |
. . . . . . . . . . . . . . 15
⊢
∀𝑏 ∈
𝐵 ∃𝑧 𝑧 = (𝑎 + 𝑏) |
121 | | r19.2z 4012 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ≠ ∅ ∧
∀𝑏 ∈ 𝐵 ∃𝑧 𝑧 = (𝑎 + 𝑏)) → ∃𝑏 ∈ 𝐵 ∃𝑧 𝑧 = (𝑎 + 𝑏)) |
122 | 5, 120, 121 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ∃𝑏 ∈ 𝐵 ∃𝑧 𝑧 = (𝑎 + 𝑏)) |
123 | | rexcom4 3198 |
. . . . . . . . . . . . . 14
⊢
(∃𝑏 ∈
𝐵 ∃𝑧 𝑧 = (𝑎 + 𝑏) ↔ ∃𝑧∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)) |
124 | 122, 123 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∃𝑧∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)) |
125 | | abn0 3908 |
. . . . . . . . . . . . 13
⊢ ({𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅ ↔ ∃𝑧∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)) |
126 | 124, 125 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (𝜑 → {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅) |
127 | 126 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅) |
128 | | suprcl 10862 |
. . . . . . . . . . . . . 14
⊢ ((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥) → sup(𝐶, ℝ, < ) ∈
ℝ) |
129 | 64, 80, 107, 128 | syl3anc 1318 |
. . . . . . . . . . . . 13
⊢ (𝜑 → sup(𝐶, ℝ, < ) ∈
ℝ) |
130 | 129 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → sup(𝐶, ℝ, < ) ∈
ℝ) |
131 | | breq2 4587 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = sup(𝐶, ℝ, < ) → (𝑤 ≤ 𝑥 ↔ 𝑤 ≤ sup(𝐶, ℝ, < ))) |
132 | 131 | ralbidv 2969 |
. . . . . . . . . . . . 13
⊢ (𝑥 = sup(𝐶, ℝ, < ) → (∀𝑤 ∈ {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ 𝑥 ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < ))) |
133 | 132 | rspcev 3282 |
. . . . . . . . . . . 12
⊢
((sup(𝐶, ℝ,
< ) ∈ ℝ ∧ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < )) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ 𝑥) |
134 | 130, 113,
133 | syl2anc 691 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ 𝑥) |
135 | | suprleub 10866 |
. . . . . . . . . . 11
⊢ ((({𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ 𝑥) ∧ sup(𝐶, ℝ, < ) ∈ ℝ) →
(sup({𝑧 ∣
∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔
∀𝑤 ∈ {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < ))) |
136 | 118, 127,
134, 130, 135 | syl31anc 1321 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (sup({𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔
∀𝑤 ∈ {𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}𝑤 ≤ sup(𝐶, ℝ, < ))) |
137 | 113, 136 | mpbird 246 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → sup({𝑧 ∣ ∃𝑏 ∈ 𝐵 𝑧 = (𝑎 + 𝑏)}, ℝ, < ) ≤ sup(𝐶, ℝ, <
)) |
138 | 40, 137 | eqbrtrd 4605 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) ≤ sup(𝐶, ℝ, < )) |
139 | | breq1 4586 |
. . . . . . . 8
⊢ (𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → (𝑤 ≤ sup(𝐶, ℝ, < ) ↔ (sup(𝐵, ℝ, < ) + 𝑎) ≤ sup(𝐶, ℝ, < ))) |
140 | 138, 139 | syl5ibrcom 236 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑤 ≤ sup(𝐶, ℝ, < ))) |
141 | 140 | rexlimdva 3013 |
. . . . . 6
⊢ (𝜑 → (∃𝑎 ∈ 𝐴 𝑤 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑤 ≤ sup(𝐶, ℝ, < ))) |
142 | 24, 141 | syl5bi 231 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} → 𝑤 ≤ sup(𝐶, ℝ, < ))) |
143 | 142 | ralrimiv 2948 |
. . . 4
⊢ (𝜑 → ∀𝑤 ∈ {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )) |
144 | 13, 11 | readdcld 9948 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (sup(𝐵, ℝ, < ) + 𝑎) ∈ ℝ) |
145 | | eleq1a 2683 |
. . . . . . . 8
⊢
((sup(𝐵, ℝ,
< ) + 𝑎) ∈ ℝ
→ (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ)) |
146 | 144, 145 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ)) |
147 | 146 | rexlimdva 3013 |
. . . . . 6
⊢ (𝜑 → (∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) → 𝑧 ∈ ℝ)) |
148 | 147 | abssdv 3639 |
. . . . 5
⊢ (𝜑 → {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ⊆ ℝ) |
149 | | ovex 6577 |
. . . . . . . . . 10
⊢
(sup(𝐵, ℝ,
< ) + 𝑎) ∈
V |
150 | 149 | isseti 3182 |
. . . . . . . . 9
⊢
∃𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) |
151 | 150 | rgenw 2908 |
. . . . . . . 8
⊢
∀𝑎 ∈
𝐴 ∃𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) |
152 | | r19.2z 4012 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧
∀𝑎 ∈ 𝐴 ∃𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)) → ∃𝑎 ∈ 𝐴 ∃𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)) |
153 | 2, 151, 152 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → ∃𝑎 ∈ 𝐴 ∃𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)) |
154 | | rexcom4 3198 |
. . . . . . 7
⊢
(∃𝑎 ∈
𝐴 ∃𝑧 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎) ↔ ∃𝑧∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)) |
155 | 153, 154 | sylib 207 |
. . . . . 6
⊢ (𝜑 → ∃𝑧∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)) |
156 | | abn0 3908 |
. . . . . 6
⊢ ({𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅ ↔ ∃𝑧∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)) |
157 | 155, 156 | sylibr 223 |
. . . . 5
⊢ (𝜑 → {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅) |
158 | 131 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑥 = sup(𝐶, ℝ, < ) → (∀𝑤 ∈ {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ 𝑥 ↔ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < ))) |
159 | 158 | rspcev 3282 |
. . . . . 6
⊢
((sup(𝐶, ℝ,
< ) ∈ ℝ ∧ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < )) → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ 𝑥) |
160 | 129, 143,
159 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ 𝑥) |
161 | | suprleub 10866 |
. . . . 5
⊢ ((({𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ⊆ ℝ ∧ {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)} ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ 𝑥) ∧ sup(𝐶, ℝ, < ) ∈ ℝ) →
(sup({𝑧 ∣
∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔
∀𝑤 ∈ {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < ))) |
162 | 148, 157,
160, 129, 161 | syl31anc 1321 |
. . . 4
⊢ (𝜑 → (sup({𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, < ) ↔
∀𝑤 ∈ {𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}𝑤 ≤ sup(𝐶, ℝ, < ))) |
163 | 143, 162 | mpbird 246 |
. . 3
⊢ (𝜑 → sup({𝑧 ∣ ∃𝑎 ∈ 𝐴 𝑧 = (sup(𝐵, ℝ, < ) + 𝑎)}, ℝ, < ) ≤ sup(𝐶, ℝ, <
)) |
164 | 20, 163 | eqbrtrd 4605 |
. 2
⊢ (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ≤ sup(𝐶, ℝ, <
)) |
165 | | suprleub 10866 |
. . . 4
⊢ (((𝐶 ⊆ ℝ ∧ 𝐶 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑤 ∈ 𝐶 𝑤 ≤ 𝑥) ∧ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ∈ ℝ) →
(sup(𝐶, ℝ, < )
≤ (sup(𝐴, ℝ, <
) + sup(𝐵, ℝ, < ))
↔ ∀𝑤 ∈
𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))) |
166 | 64, 80, 107, 83, 165 | syl31anc 1321 |
. . 3
⊢ (𝜑 → (sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ↔
∀𝑤 ∈ 𝐶 𝑤 ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )))) |
167 | 103, 166 | mpbird 246 |
. 2
⊢ (𝜑 → sup(𝐶, ℝ, < ) ≤ (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, <
))) |
168 | 83, 129 | letri3d 10058 |
. 2
⊢ (𝜑 → ((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < ) ↔ ((sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) ≤
sup(𝐶, ℝ, < )
∧ sup(𝐶, ℝ, <
) ≤ (sup(𝐴, ℝ,
< ) + sup(𝐵, ℝ,
< ))))) |
169 | 164, 167,
168 | mpbir2and 959 |
1
⊢ (𝜑 → (sup(𝐴, ℝ, < ) + sup(𝐵, ℝ, < )) = sup(𝐶, ℝ, < )) |