Step | Hyp | Ref
| Expression |
1 | | suprcl 10862 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈
ℝ) |
2 | 1 | leidd 10473 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ≤ sup(𝐴, ℝ, < )) |
3 | | suprleub 10866 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ sup(𝐴, ℝ, < ) ∈ ℝ) →
(sup(𝐴, ℝ, < )
≤ sup(𝐴, ℝ, < )
↔ ∀𝑧 ∈
𝐴 𝑧 ≤ sup(𝐴, ℝ, < ))) |
4 | 1, 3 | mpdan 699 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (sup(𝐴, ℝ, < ) ≤ sup(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 𝑧 ≤ sup(𝐴, ℝ, < ))) |
5 | | simp1 1054 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → 𝐴 ⊆ ℝ) |
6 | | ressxr 9962 |
. . . . . 6
⊢ ℝ
⊆ ℝ* |
7 | 5, 6 | syl6ss 3580 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → 𝐴 ⊆
ℝ*) |
8 | 1 | rexrd 9968 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈
ℝ*) |
9 | | supxrleub 12028 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ sup(𝐴, ℝ, <
) ∈ ℝ*) → (sup(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ, < ) ↔
∀𝑧 ∈ 𝐴 𝑧 ≤ sup(𝐴, ℝ, < ))) |
10 | 7, 8, 9 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (sup(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ, < ) ↔
∀𝑧 ∈ 𝐴 𝑧 ≤ sup(𝐴, ℝ, < ))) |
11 | 4, 10 | bitr4d 270 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (sup(𝐴, ℝ, < ) ≤ sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ*, < )
≤ sup(𝐴, ℝ, <
))) |
12 | 2, 11 | mpbid 221 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ, <
)) |
13 | | supxrcl 12017 |
. . . . 5
⊢ (𝐴 ⊆ ℝ*
→ sup(𝐴,
ℝ*, < ) ∈ ℝ*) |
14 | 7, 13 | syl 17 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ*, < ) ∈
ℝ*) |
15 | | xrleid 11859 |
. . . 4
⊢
(sup(𝐴,
ℝ*, < ) ∈ ℝ* → sup(𝐴, ℝ*, < )
≤ sup(𝐴,
ℝ*, < )) |
16 | 14, 15 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ*, <
)) |
17 | | supxrleub 12028 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ sup(𝐴,
ℝ*, < ) ∈ ℝ*) → (sup(𝐴, ℝ*, < )
≤ sup(𝐴,
ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 𝑥 ≤ sup(𝐴, ℝ*, <
))) |
18 | 7, 14, 17 | syl2anc 691 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (sup(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ*, < )
↔ ∀𝑥 ∈
𝐴 𝑥 ≤ sup(𝐴, ℝ*, <
))) |
19 | | simp2 1055 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → 𝐴 ≠ ∅) |
20 | | n0 3890 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝐴) |
21 | 19, 20 | sylib 207 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑧 𝑧 ∈ 𝐴) |
22 | | mnfxr 9975 |
. . . . . . . . 9
⊢ -∞
∈ ℝ* |
23 | 22 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → -∞ ∈
ℝ*) |
24 | 5 | sselda 3568 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) |
25 | 24 | rexrd 9968 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ*) |
26 | 14 | adantr 480 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → sup(𝐴, ℝ*, < ) ∈
ℝ*) |
27 | | mnflt 11833 |
. . . . . . . . 9
⊢ (𝑧 ∈ ℝ → -∞
< 𝑧) |
28 | 24, 27 | syl 17 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → -∞ < 𝑧) |
29 | | supxrub 12026 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑧 ∈ 𝐴) → 𝑧 ≤ sup(𝐴, ℝ*, <
)) |
30 | 7, 29 | sylan 487 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → 𝑧 ≤ sup(𝐴, ℝ*, <
)) |
31 | 23, 25, 26, 28, 30 | xrltletrd 11868 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → -∞ < sup(𝐴, ℝ*, <
)) |
32 | 21, 31 | exlimddv 1850 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → -∞ < sup(𝐴, ℝ*, <
)) |
33 | | xrre 11874 |
. . . . . 6
⊢
(((sup(𝐴,
ℝ*, < ) ∈ ℝ* ∧ sup(𝐴, ℝ, < ) ∈
ℝ) ∧ (-∞ < sup(𝐴, ℝ*, < ) ∧
sup(𝐴, ℝ*,
< ) ≤ sup(𝐴, ℝ,
< ))) → sup(𝐴,
ℝ*, < ) ∈ ℝ) |
34 | 14, 1, 32, 12, 33 | syl22anc 1319 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ*, < ) ∈
ℝ) |
35 | | suprleub 10866 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) → (sup(𝐴,
ℝ, < ) ≤ sup(𝐴,
ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 𝑥 ≤ sup(𝐴, ℝ*, <
))) |
36 | 34, 35 | mpdan 699 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (sup(𝐴, ℝ, < ) ≤ sup(𝐴, ℝ*, < ) ↔
∀𝑥 ∈ 𝐴 𝑥 ≤ sup(𝐴, ℝ*, <
))) |
37 | 18, 36 | bitr4d 270 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (sup(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ*, < )
↔ sup(𝐴, ℝ, <
) ≤ sup(𝐴,
ℝ*, < ))) |
38 | 16, 37 | mpbid 221 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ≤ sup(𝐴, ℝ*, <
)) |
39 | | xrletri3 11861 |
. . 3
⊢
((sup(𝐴,
ℝ*, < ) ∈ ℝ* ∧ sup(𝐴, ℝ, < ) ∈
ℝ*) → (sup(𝐴, ℝ*, < ) = sup(𝐴, ℝ, < ) ↔
(sup(𝐴,
ℝ*, < ) ≤ sup(𝐴, ℝ, < ) ∧ sup(𝐴, ℝ, < ) ≤ sup(𝐴, ℝ*, <
)))) |
40 | 14, 8, 39 | syl2anc 691 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (sup(𝐴, ℝ*, < ) = sup(𝐴, ℝ, < ) ↔
(sup(𝐴,
ℝ*, < ) ≤ sup(𝐴, ℝ, < ) ∧ sup(𝐴, ℝ, < ) ≤ sup(𝐴, ℝ*, <
)))) |
41 | 12, 38, 40 | mpbir2and 959 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ*, < ) = sup(𝐴, ℝ, <
)) |