Step | Hyp | Ref
| Expression |
1 | | supicc.3 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) |
2 | | supicc.1 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | supicc.2 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℝ) |
4 | | iccssre 12126 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵[,]𝐶) ⊆ ℝ) |
5 | 2, 3, 4 | syl2anc 691 |
. . . 4
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ ℝ) |
6 | 1, 5 | sstrd 3578 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
7 | | supicc.4 |
. . 3
⊢ (𝜑 → 𝐴 ≠ ∅) |
8 | 2 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
9 | 8 | rexrd 9968 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈
ℝ*) |
10 | 3 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) |
11 | 10 | rexrd 9968 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈
ℝ*) |
12 | 1 | sselda 3568 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (𝐵[,]𝐶)) |
13 | | iccleub 12100 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵[,]𝐶)) → 𝑥 ≤ 𝐶) |
14 | 9, 11, 12, 13 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ 𝐶) |
15 | 14 | ralrimiva 2949 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐶) |
16 | | breq2 4587 |
. . . . . 6
⊢ (𝑦 = 𝐶 → (𝑥 ≤ 𝑦 ↔ 𝑥 ≤ 𝐶)) |
17 | 16 | ralbidv 2969 |
. . . . 5
⊢ (𝑦 = 𝐶 → (∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦 ↔ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐶)) |
18 | 17 | rspcev 3282 |
. . . 4
⊢ ((𝐶 ∈ ℝ ∧
∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐶) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦) |
19 | 3, 15, 18 | syl2anc 691 |
. . 3
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦) |
20 | | suprcl 10862 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦) → sup(𝐴, ℝ, < ) ∈
ℝ) |
21 | 6, 7, 19, 20 | syl3anc 1318 |
. 2
⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈
ℝ) |
22 | 6 | sselda 3568 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
23 | 1 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 ⊆ (𝐵[,]𝐶)) |
24 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
25 | | iccsupr 12137 |
. . . . . . 7
⊢ (((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ⊆ (𝐵[,]𝐶) ∧ 𝑥 ∈ 𝐴) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦)) |
26 | 8, 10, 23, 24, 25 | syl211anc 1324 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦)) |
27 | 26, 20 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → sup(𝐴, ℝ, < ) ∈
ℝ) |
28 | | iccgelb 12101 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵[,]𝐶)) → 𝐵 ≤ 𝑥) |
29 | 9, 11, 12, 28 | syl3anc 1318 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑥) |
30 | | suprub 10863 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ sup(𝐴, ℝ, < )) |
31 | 26, 24, 30 | syl2anc 691 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ sup(𝐴, ℝ, < )) |
32 | 8, 22, 27, 29, 31 | letrd 10073 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ sup(𝐴, ℝ, < )) |
33 | 32 | ralrimiva 2949 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ≤ sup(𝐴, ℝ, < )) |
34 | | r19.3rzv 4016 |
. . . 4
⊢ (𝐴 ≠ ∅ → (𝐵 ≤ sup(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ sup(𝐴, ℝ, < ))) |
35 | 7, 34 | syl 17 |
. . 3
⊢ (𝜑 → (𝐵 ≤ sup(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ sup(𝐴, ℝ, < ))) |
36 | 33, 35 | mpbird 246 |
. 2
⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < )) |
37 | | suprleub 10866 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝐶 ∈ ℝ) → (sup(𝐴, ℝ, < ) ≤ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐶)) |
38 | 6, 7, 19, 3, 37 | syl31anc 1321 |
. . 3
⊢ (𝜑 → (sup(𝐴, ℝ, < ) ≤ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐶)) |
39 | 15, 38 | mpbird 246 |
. 2
⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐶) |
40 | | elicc2 12109 |
. . 3
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) →
(sup(𝐴, ℝ, < )
∈ (𝐵[,]𝐶) ↔ (sup(𝐴, ℝ, < ) ∈ ℝ ∧ 𝐵 ≤ sup(𝐴, ℝ, < ) ∧ sup(𝐴, ℝ, < ) ≤ 𝐶))) |
41 | 2, 3, 40 | syl2anc 691 |
. 2
⊢ (𝜑 → (sup(𝐴, ℝ, < ) ∈ (𝐵[,]𝐶) ↔ (sup(𝐴, ℝ, < ) ∈ ℝ ∧ 𝐵 ≤ sup(𝐴, ℝ, < ) ∧ sup(𝐴, ℝ, < ) ≤ 𝐶))) |
42 | 21, 36, 39, 41 | mpbir3and 1238 |
1
⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ (𝐵[,]𝐶)) |