Step | Hyp | Ref
| Expression |
1 | | simp1 1135 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → 𝐴 ⊆ ℝ) |
2 | | ressxr 11019 |
. . . 4
⊢ ℝ
⊆ ℝ* |
3 | 1, 2 | sstrdi 3933 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → 𝐴 ⊆
ℝ*) |
4 | | supxrcl 13049 |
. . 3
⊢ (𝐴 ⊆ ℝ*
→ sup(𝐴,
ℝ*, < ) ∈ ℝ*) |
5 | 3, 4 | syl 17 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ*, < ) ∈
ℝ*) |
6 | | suprcl 11935 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈
ℝ) |
7 | 6 | rexrd 11025 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ∈
ℝ*) |
8 | 6 | leidd 11541 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ≤ sup(𝐴, ℝ, < )) |
9 | | suprleub 11941 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ sup(𝐴, ℝ, < ) ∈ ℝ) →
(sup(𝐴, ℝ, < )
≤ sup(𝐴, ℝ, < )
↔ ∀𝑧 ∈
𝐴 𝑧 ≤ sup(𝐴, ℝ, < ))) |
10 | 6, 9 | mpdan 684 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (sup(𝐴, ℝ, < ) ≤ sup(𝐴, ℝ, < ) ↔ ∀𝑧 ∈ 𝐴 𝑧 ≤ sup(𝐴, ℝ, < ))) |
11 | | supxrleub 13060 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ sup(𝐴, ℝ, <
) ∈ ℝ*) → (sup(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ, < ) ↔
∀𝑧 ∈ 𝐴 𝑧 ≤ sup(𝐴, ℝ, < ))) |
12 | 3, 7, 11 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (sup(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ, < ) ↔
∀𝑧 ∈ 𝐴 𝑧 ≤ sup(𝐴, ℝ, < ))) |
13 | 10, 12 | bitr4d 281 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (sup(𝐴, ℝ, < ) ≤ sup(𝐴, ℝ, < ) ↔ sup(𝐴, ℝ*, < )
≤ sup(𝐴, ℝ, <
))) |
14 | 8, 13 | mpbid 231 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ, <
)) |
15 | 5 | xrleidd 12886 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ*, <
)) |
16 | | supxrleub 13060 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ sup(𝐴,
ℝ*, < ) ∈ ℝ*) → (sup(𝐴, ℝ*, < )
≤ sup(𝐴,
ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 𝑥 ≤ sup(𝐴, ℝ*, <
))) |
17 | 3, 5, 16 | syl2anc 584 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (sup(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ*, < )
↔ ∀𝑥 ∈
𝐴 𝑥 ≤ sup(𝐴, ℝ*, <
))) |
18 | | simp2 1136 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → 𝐴 ≠ ∅) |
19 | | n0 4280 |
. . . . . . . 8
⊢ (𝐴 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝐴) |
20 | 18, 19 | sylib 217 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑧 𝑧 ∈ 𝐴) |
21 | | mnfxr 11032 |
. . . . . . . . 9
⊢ -∞
∈ ℝ* |
22 | 21 | a1i 11 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → -∞ ∈
ℝ*) |
23 | 1 | sselda 3921 |
. . . . . . . . 9
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) |
24 | 23 | rexrd 11025 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ*) |
25 | 5 | adantr 481 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → sup(𝐴, ℝ*, < ) ∈
ℝ*) |
26 | 23 | mnfltd 12860 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → -∞ < 𝑧) |
27 | | supxrub 13058 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑧 ∈ 𝐴) → 𝑧 ≤ sup(𝐴, ℝ*, <
)) |
28 | 3, 27 | sylan 580 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → 𝑧 ≤ sup(𝐴, ℝ*, <
)) |
29 | 22, 24, 25, 26, 28 | xrltletrd 12895 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ 𝑧 ∈ 𝐴) → -∞ < sup(𝐴, ℝ*, <
)) |
30 | 20, 29 | exlimddv 1938 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → -∞ < sup(𝐴, ℝ*, <
)) |
31 | | xrre 12903 |
. . . . . 6
⊢
(((sup(𝐴,
ℝ*, < ) ∈ ℝ* ∧ sup(𝐴, ℝ, < ) ∈
ℝ) ∧ (-∞ < sup(𝐴, ℝ*, < ) ∧
sup(𝐴, ℝ*,
< ) ≤ sup(𝐴, ℝ,
< ))) → sup(𝐴,
ℝ*, < ) ∈ ℝ) |
32 | 5, 6, 30, 14, 31 | syl22anc 836 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ*, < ) ∈
ℝ) |
33 | | suprleub 11941 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) ∧ sup(𝐴, ℝ*, < ) ∈
ℝ) → (sup(𝐴,
ℝ, < ) ≤ sup(𝐴,
ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 𝑥 ≤ sup(𝐴, ℝ*, <
))) |
34 | 32, 33 | mpdan 684 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (sup(𝐴, ℝ, < ) ≤ sup(𝐴, ℝ*, < ) ↔
∀𝑥 ∈ 𝐴 𝑥 ≤ sup(𝐴, ℝ*, <
))) |
35 | 17, 34 | bitr4d 281 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → (sup(𝐴, ℝ*, < ) ≤ sup(𝐴, ℝ*, < )
↔ sup(𝐴, ℝ, <
) ≤ sup(𝐴,
ℝ*, < ))) |
36 | 15, 35 | mpbid 231 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ, < ) ≤ sup(𝐴, ℝ*, <
)) |
37 | 5, 7, 14, 36 | xrletrid 12889 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → sup(𝐴, ℝ*, < ) = sup(𝐴, ℝ, <
)) |