Step | Hyp | Ref
| Expression |
1 | | supicc.3 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ (𝐵[,]𝐶)) |
2 | | supicc.1 |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ ℝ) |
3 | | supicc.2 |
. . . . 5
⊢ (𝜑 → 𝐶 ∈ ℝ) |
4 | | iccssre 13406 |
. . . . 5
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐵[,]𝐶) ⊆ ℝ) |
5 | 2, 3, 4 | syl2anc 585 |
. . . 4
⊢ (𝜑 → (𝐵[,]𝐶) ⊆ ℝ) |
6 | 1, 5 | sstrd 3993 |
. . 3
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
7 | | supicc.4 |
. . 3
⊢ (𝜑 → 𝐴 ≠ ∅) |
8 | 2 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ ℝ) |
9 | 8 | rexrd 11264 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈
ℝ*) |
10 | 3 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℝ) |
11 | 10 | rexrd 11264 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈
ℝ*) |
12 | 1 | sselda 3983 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ (𝐵[,]𝐶)) |
13 | | iccleub 13379 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵[,]𝐶)) → 𝑥 ≤ 𝐶) |
14 | 9, 11, 12, 13 | syl3anc 1372 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ 𝐶) |
15 | 14 | ralrimiva 3147 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐶) |
16 | | brralrspcev 5209 |
. . . 4
⊢ ((𝐶 ∈ ℝ ∧
∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐶) → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦) |
17 | 3, 15, 16 | syl2anc 585 |
. . 3
⊢ (𝜑 → ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦) |
18 | | suprcl 12174 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦) → sup(𝐴, ℝ, < ) ∈
ℝ) |
19 | 6, 7, 17, 18 | syl3anc 1372 |
. 2
⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈
ℝ) |
20 | 6 | sselda 3983 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ) |
21 | 1 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 ⊆ (𝐵[,]𝐶)) |
22 | | simpr 486 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
23 | | iccsupr 13419 |
. . . . . . 7
⊢ (((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) ∧ 𝐴 ⊆ (𝐵[,]𝐶) ∧ 𝑥 ∈ 𝐴) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦)) |
24 | 8, 10, 21, 22, 23 | syl211anc 1377 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦)) |
25 | 24, 18 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → sup(𝐴, ℝ, < ) ∈
ℝ) |
26 | | iccgelb 13380 |
. . . . . 6
⊢ ((𝐵 ∈ ℝ*
∧ 𝐶 ∈
ℝ* ∧ 𝑥
∈ (𝐵[,]𝐶)) → 𝐵 ≤ 𝑥) |
27 | 9, 11, 12, 26 | syl3anc 1372 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ 𝑥) |
28 | | suprub 12175 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ sup(𝐴, ℝ, < )) |
29 | 24, 22, 28 | syl2anc 585 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ sup(𝐴, ℝ, < )) |
30 | 8, 20, 25, 27, 29 | letrd 11371 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ≤ sup(𝐴, ℝ, < )) |
31 | 30 | ralrimiva 3147 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ≤ sup(𝐴, ℝ, < )) |
32 | | r19.3rzv 4499 |
. . . 4
⊢ (𝐴 ≠ ∅ → (𝐵 ≤ sup(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ sup(𝐴, ℝ, < ))) |
33 | 7, 32 | syl 17 |
. . 3
⊢ (𝜑 → (𝐵 ≤ sup(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 𝐵 ≤ sup(𝐴, ℝ, < ))) |
34 | 31, 33 | mpbird 257 |
. 2
⊢ (𝜑 → 𝐵 ≤ sup(𝐴, ℝ, < )) |
35 | | suprleub 12180 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑦 ∈ ℝ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝐶 ∈ ℝ) → (sup(𝐴, ℝ, < ) ≤ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐶)) |
36 | 6, 7, 17, 3, 35 | syl31anc 1374 |
. . 3
⊢ (𝜑 → (sup(𝐴, ℝ, < ) ≤ 𝐶 ↔ ∀𝑥 ∈ 𝐴 𝑥 ≤ 𝐶)) |
37 | 15, 36 | mpbird 257 |
. 2
⊢ (𝜑 → sup(𝐴, ℝ, < ) ≤ 𝐶) |
38 | | elicc2 13389 |
. . 3
⊢ ((𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) →
(sup(𝐴, ℝ, < )
∈ (𝐵[,]𝐶) ↔ (sup(𝐴, ℝ, < ) ∈ ℝ ∧ 𝐵 ≤ sup(𝐴, ℝ, < ) ∧ sup(𝐴, ℝ, < ) ≤ 𝐶))) |
39 | 2, 3, 38 | syl2anc 585 |
. 2
⊢ (𝜑 → (sup(𝐴, ℝ, < ) ∈ (𝐵[,]𝐶) ↔ (sup(𝐴, ℝ, < ) ∈ ℝ ∧ 𝐵 ≤ sup(𝐴, ℝ, < ) ∧ sup(𝐴, ℝ, < ) ≤ 𝐶))) |
40 | 19, 34, 37, 39 | mpbir3and 1343 |
1
⊢ (𝜑 → sup(𝐴, ℝ, < ) ∈ (𝐵[,]𝐶)) |