Step | Hyp | Ref
| Expression |
1 | | id 22 |
. . . 4
⊢ (𝐴 ⊆ ℝ*
→ 𝐴 ⊆
ℝ*) |
2 | | pnfxr 10960 |
. . . . . 6
⊢ +∞
∈ ℝ* |
3 | | snssi 4738 |
. . . . . 6
⊢ (+∞
∈ ℝ* → {+∞} ⊆
ℝ*) |
4 | 2, 3 | ax-mp 5 |
. . . . 5
⊢
{+∞} ⊆ ℝ* |
5 | 4 | a1i 11 |
. . . 4
⊢ (𝐴 ⊆ ℝ*
→ {+∞} ⊆ ℝ*) |
6 | 1, 5 | unssd 4116 |
. . 3
⊢ (𝐴 ⊆ ℝ*
→ (𝐴 ∪ {+∞})
⊆ ℝ*) |
7 | 6 | infxrcld 42819 |
. 2
⊢ (𝐴 ⊆ ℝ*
→ inf((𝐴 ∪
{+∞}), ℝ*, < ) ∈
ℝ*) |
8 | | infxrcl 12996 |
. 2
⊢ (𝐴 ⊆ ℝ*
→ inf(𝐴,
ℝ*, < ) ∈ ℝ*) |
9 | | ssun1 4102 |
. . . 4
⊢ 𝐴 ⊆ (𝐴 ∪ {+∞}) |
10 | 9 | a1i 11 |
. . 3
⊢ (𝐴 ⊆ ℝ*
→ 𝐴 ⊆ (𝐴 ∪
{+∞})) |
11 | | infxrss 13002 |
. . 3
⊢ ((𝐴 ⊆ (𝐴 ∪ {+∞}) ∧ (𝐴 ∪ {+∞}) ⊆
ℝ*) → inf((𝐴 ∪ {+∞}), ℝ*,
< ) ≤ inf(𝐴,
ℝ*, < )) |
12 | 10, 6, 11 | syl2anc 583 |
. 2
⊢ (𝐴 ⊆ ℝ*
→ inf((𝐴 ∪
{+∞}), ℝ*, < ) ≤ inf(𝐴, ℝ*, <
)) |
13 | | infeq1 9165 |
. . . . . 6
⊢ (𝐴 = ∅ → inf(𝐴, ℝ*, < ) =
inf(∅, ℝ*, < )) |
14 | | xrinf0 13001 |
. . . . . . . 8
⊢
inf(∅, ℝ*, < ) = +∞ |
15 | 14, 2 | eqeltri 2835 |
. . . . . . 7
⊢
inf(∅, ℝ*, < ) ∈
ℝ* |
16 | 15 | a1i 11 |
. . . . . 6
⊢ (𝐴 = ∅ → inf(∅,
ℝ*, < ) ∈ ℝ*) |
17 | 13, 16 | eqeltrd 2839 |
. . . . 5
⊢ (𝐴 = ∅ → inf(𝐴, ℝ*, < )
∈ ℝ*) |
18 | | xrltso 12804 |
. . . . . . . . 9
⊢ < Or
ℝ* |
19 | | infsn 9194 |
. . . . . . . . 9
⊢ (( <
Or ℝ* ∧ +∞ ∈ ℝ*) →
inf({+∞}, ℝ*, < ) = +∞) |
20 | 18, 2, 19 | mp2an 688 |
. . . . . . . 8
⊢
inf({+∞}, ℝ*, < ) = +∞ |
21 | 20 | eqcomi 2747 |
. . . . . . 7
⊢ +∞
= inf({+∞}, ℝ*, < ) |
22 | 21 | a1i 11 |
. . . . . 6
⊢ (𝐴 = ∅ → +∞ =
inf({+∞}, ℝ*, < )) |
23 | 13, 14 | eqtrdi 2795 |
. . . . . 6
⊢ (𝐴 = ∅ → inf(𝐴, ℝ*, < ) =
+∞) |
24 | | uneq1 4086 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (𝐴 ∪ {+∞}) = (∅
∪ {+∞})) |
25 | | 0un 4323 |
. . . . . . . . 9
⊢ (∅
∪ {+∞}) = {+∞} |
26 | 25 | a1i 11 |
. . . . . . . 8
⊢ (𝐴 = ∅ → (∅ ∪
{+∞}) = {+∞}) |
27 | 24, 26 | eqtrd 2778 |
. . . . . . 7
⊢ (𝐴 = ∅ → (𝐴 ∪ {+∞}) =
{+∞}) |
28 | 27 | infeq1d 9166 |
. . . . . 6
⊢ (𝐴 = ∅ → inf((𝐴 ∪ {+∞}),
ℝ*, < ) = inf({+∞}, ℝ*, <
)) |
29 | 22, 23, 28 | 3eqtr4d 2788 |
. . . . 5
⊢ (𝐴 = ∅ → inf(𝐴, ℝ*, < ) =
inf((𝐴 ∪ {+∞}),
ℝ*, < )) |
30 | 17, 29 | xreqled 42759 |
. . . 4
⊢ (𝐴 = ∅ → inf(𝐴, ℝ*, < )
≤ inf((𝐴 ∪
{+∞}), ℝ*, < )) |
31 | 30 | adantl 481 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐴 = ∅) →
inf(𝐴, ℝ*,
< ) ≤ inf((𝐴 ∪
{+∞}), ℝ*, < )) |
32 | | neqne 2950 |
. . . 4
⊢ (¬
𝐴 = ∅ → 𝐴 ≠ ∅) |
33 | | nfv 1918 |
. . . . 5
⊢
Ⅎ𝑥(𝐴 ⊆ ℝ*
∧ 𝐴 ≠
∅) |
34 | | nfv 1918 |
. . . . 5
⊢
Ⅎ𝑦(𝐴 ⊆ ℝ*
∧ 𝐴 ≠
∅) |
35 | | simpl 482 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐴 ≠ ∅)
→ 𝐴 ⊆
ℝ*) |
36 | 35, 6 | syl 17 |
. . . . 5
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐴 ≠ ∅)
→ (𝐴 ∪ {+∞})
⊆ ℝ*) |
37 | | simpr 484 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
38 | | ssel2 3912 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ ℝ*) |
39 | 38 | xrleidd 12815 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ 𝐴) → 𝑥 ≤ 𝑥) |
40 | | breq1 5073 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → (𝑦 ≤ 𝑥 ↔ 𝑥 ≤ 𝑥)) |
41 | 40 | rspcev 3552 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ 𝑥 ≤ 𝑥) → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
42 | 37, 39, 41 | syl2anc 583 |
. . . . . . 7
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
43 | 42 | ad4ant14 748 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝐴 ≠ ∅) ∧
𝑥 ∈ (𝐴 ∪ {+∞})) ∧ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
44 | | simpll 763 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝐴 ≠ ∅) ∧
𝑥 ∈ (𝐴 ∪ {+∞})) ∧ ¬ 𝑥 ∈ 𝐴) → (𝐴 ⊆ ℝ* ∧ 𝐴 ≠ ∅)) |
45 | | elunnel1 4080 |
. . . . . . . . 9
⊢ ((𝑥 ∈ (𝐴 ∪ {+∞}) ∧ ¬ 𝑥 ∈ 𝐴) → 𝑥 ∈ {+∞}) |
46 | | elsni 4575 |
. . . . . . . . 9
⊢ (𝑥 ∈ {+∞} → 𝑥 = +∞) |
47 | 45, 46 | syl 17 |
. . . . . . . 8
⊢ ((𝑥 ∈ (𝐴 ∪ {+∞}) ∧ ¬ 𝑥 ∈ 𝐴) → 𝑥 = +∞) |
48 | 47 | adantll 710 |
. . . . . . 7
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝐴 ≠ ∅) ∧
𝑥 ∈ (𝐴 ∪ {+∞})) ∧ ¬ 𝑥 ∈ 𝐴) → 𝑥 = +∞) |
49 | | simplr 765 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐴 ≠ ∅) ∧
𝑥 = +∞) → 𝐴 ≠ ∅) |
50 | | ssel2 3912 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑦 ∈ 𝐴) → 𝑦 ∈ ℝ*) |
51 | | pnfge 12795 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ 𝑦 ≤
+∞) |
52 | 50, 51 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑦 ∈ 𝐴) → 𝑦 ≤ +∞) |
53 | 52 | adantlr 711 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑥 = +∞) ∧
𝑦 ∈ 𝐴) → 𝑦 ≤ +∞) |
54 | | simplr 765 |
. . . . . . . . . . 11
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑥 = +∞) ∧
𝑦 ∈ 𝐴) → 𝑥 = +∞) |
55 | 53, 54 | breqtrrd 5098 |
. . . . . . . . . 10
⊢ (((𝐴 ⊆ ℝ*
∧ 𝑥 = +∞) ∧
𝑦 ∈ 𝐴) → 𝑦 ≤ 𝑥) |
56 | 55 | ralrimiva 3107 |
. . . . . . . . 9
⊢ ((𝐴 ⊆ ℝ*
∧ 𝑥 = +∞) →
∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
57 | 56 | adantlr 711 |
. . . . . . . 8
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐴 ≠ ∅) ∧
𝑥 = +∞) →
∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
58 | | r19.2z 4422 |
. . . . . . . 8
⊢ ((𝐴 ≠ ∅ ∧
∀𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
59 | 49, 57, 58 | syl2anc 583 |
. . . . . . 7
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐴 ≠ ∅) ∧
𝑥 = +∞) →
∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
60 | 44, 48, 59 | syl2anc 583 |
. . . . . 6
⊢ ((((𝐴 ⊆ ℝ*
∧ 𝐴 ≠ ∅) ∧
𝑥 ∈ (𝐴 ∪ {+∞})) ∧ ¬ 𝑥 ∈ 𝐴) → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
61 | 43, 60 | pm2.61dan 809 |
. . . . 5
⊢ (((𝐴 ⊆ ℝ*
∧ 𝐴 ≠ ∅) ∧
𝑥 ∈ (𝐴 ∪ {+∞})) → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥) |
62 | 33, 34, 35, 36, 61 | infleinf2 42844 |
. . . 4
⊢ ((𝐴 ⊆ ℝ*
∧ 𝐴 ≠ ∅)
→ inf(𝐴,
ℝ*, < ) ≤ inf((𝐴 ∪ {+∞}), ℝ*,
< )) |
63 | 32, 62 | sylan2 592 |
. . 3
⊢ ((𝐴 ⊆ ℝ*
∧ ¬ 𝐴 = ∅)
→ inf(𝐴,
ℝ*, < ) ≤ inf((𝐴 ∪ {+∞}), ℝ*,
< )) |
64 | 31, 63 | pm2.61dan 809 |
. 2
⊢ (𝐴 ⊆ ℝ*
→ inf(𝐴,
ℝ*, < ) ≤ inf((𝐴 ∪ {+∞}), ℝ*,
< )) |
65 | 7, 8, 12, 64 | xrletrid 12818 |
1
⊢ (𝐴 ⊆ ℝ*
→ inf((𝐴 ∪
{+∞}), ℝ*, < ) = inf(𝐴, ℝ*, <
)) |