Step | Hyp | Ref
| Expression |
1 | | simp1 1061 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → 𝐴 ⊆ ℝ) |
2 | | ressxr 10083 |
. . . 4
⊢ ℝ
⊆ ℝ* |
3 | 1, 2 | syl6ss 3615 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → 𝐴 ⊆
ℝ*) |
4 | | infxrcl 12163 |
. . 3
⊢ (𝐴 ⊆ ℝ*
→ inf(𝐴,
ℝ*, < ) ∈ ℝ*) |
5 | 3, 4 | syl 17 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) ∈
ℝ*) |
6 | | infrecl 11005 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ∈
ℝ) |
7 | 6 | rexrd 10089 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ∈
ℝ*) |
8 | | xrleid 11983 |
. . . 4
⊢
(inf(𝐴,
ℝ*, < ) ∈ ℝ* → inf(𝐴, ℝ*, < )
≤ inf(𝐴,
ℝ*, < )) |
9 | 5, 8 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ*, <
)) |
10 | | infxrgelb 12165 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ inf(𝐴,
ℝ*, < ) ∈ ℝ*) → (inf(𝐴, ℝ*, < )
≤ inf(𝐴,
ℝ*, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ*, < ) ≤ 𝑥)) |
11 | 3, 5, 10 | syl2anc 693 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ*, < )
↔ ∀𝑥 ∈
𝐴 inf(𝐴, ℝ*, < ) ≤ 𝑥)) |
12 | | simp2 1062 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → 𝐴 ≠ ∅) |
13 | | n0 3931 |
. . . . . . 7
⊢ (𝐴 ≠ ∅ ↔
∃𝑧 𝑧 ∈ 𝐴) |
14 | 12, 13 | sylib 208 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → ∃𝑧 𝑧 ∈ 𝐴) |
15 | 5 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ∈
ℝ*) |
16 | 1 | sselda 3603 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → 𝑧 ∈ ℝ) |
17 | | mnfxr 10096 |
. . . . . . . . . 10
⊢ -∞
∈ ℝ* |
18 | 17 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → -∞ ∈
ℝ*) |
19 | 6 | mnfltd 11958 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → -∞ < inf(𝐴, ℝ, < )) |
20 | 6 | leidd 10594 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ, < )) |
21 | | infregelb 11007 |
. . . . . . . . . . . 12
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ inf(𝐴, ℝ, < ) ∈ ℝ) →
(inf(𝐴, ℝ, < )
≤ inf(𝐴, ℝ, < )
↔ ∀𝑥 ∈
𝐴 inf(𝐴, ℝ, < ) ≤ 𝑥)) |
22 | 6, 21 | mpdan 702 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ, < ) ≤ 𝑥)) |
23 | | infxrgelb 12165 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ*
∧ inf(𝐴, ℝ, <
) ∈ ℝ*) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ*, < ) ↔
∀𝑥 ∈ 𝐴 inf(𝐴, ℝ, < ) ≤ 𝑥)) |
24 | 3, 7, 23 | syl2anc 693 |
. . . . . . . . . . 11
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ*, < ) ↔
∀𝑥 ∈ 𝐴 inf(𝐴, ℝ, < ) ≤ 𝑥)) |
25 | 22, 24 | bitr4d 271 |
. . . . . . . . . 10
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ, < ) ↔ inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ*, <
))) |
26 | 20, 25 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ, < ) ≤ inf(𝐴, ℝ*, <
)) |
27 | 18, 7, 5, 19, 26 | xrltletrd 11992 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → -∞ < inf(𝐴, ℝ*, <
)) |
28 | 27 | adantr 481 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → -∞ < inf(𝐴, ℝ*, <
)) |
29 | | infxrlb 12164 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑧 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ≤ 𝑧) |
30 | 3, 29 | sylan 488 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ≤ 𝑧) |
31 | | xrre 12000 |
. . . . . . 7
⊢
(((inf(𝐴,
ℝ*, < ) ∈ ℝ* ∧ 𝑧 ∈ ℝ) ∧ (-∞ <
inf(𝐴, ℝ*,
< ) ∧ inf(𝐴,
ℝ*, < ) ≤ 𝑧)) → inf(𝐴, ℝ*, < ) ∈
ℝ) |
32 | 15, 16, 28, 30, 31 | syl22anc 1327 |
. . . . . 6
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ 𝑧 ∈ 𝐴) → inf(𝐴, ℝ*, < ) ∈
ℝ) |
33 | 14, 32 | exlimddv 1863 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) ∈
ℝ) |
34 | | infregelb 11007 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) ∧ inf(𝐴, ℝ*, < ) ∈
ℝ) → (inf(𝐴,
ℝ*, < ) ≤ inf(𝐴, ℝ, < ) ↔ ∀𝑥 ∈ 𝐴 inf(𝐴, ℝ*, < ) ≤ 𝑥)) |
35 | 33, 34 | mpdan 702 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ, < ) ↔
∀𝑥 ∈ 𝐴 inf(𝐴, ℝ*, < ) ≤ 𝑥)) |
36 | 11, 35 | bitr4d 271 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → (inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ*, < )
↔ inf(𝐴,
ℝ*, < ) ≤ inf(𝐴, ℝ, < ))) |
37 | 9, 36 | mpbid 222 |
. 2
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) ≤ inf(𝐴, ℝ, <
)) |
38 | 5, 7, 37, 26 | xrletrid 11986 |
1
⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝐴 𝑥 ≤ 𝑦) → inf(𝐴, ℝ*, < ) = inf(𝐴, ℝ, <
)) |