Proof of Theorem xrinfmss
Step | Hyp | Ref
| Expression |
1 | | xrinfmsslem 12777 |
. 2
⊢ ((𝐴 ⊆ ℝ*
∧ (𝐴 ⊆ ℝ
∨ -∞ ∈ 𝐴))
→ ∃𝑥 ∈
ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
2 | | ssdifss 4024 |
. . . 4
⊢ (𝐴 ⊆ ℝ*
→ (𝐴 ∖
{+∞}) ⊆ ℝ*) |
3 | | ssxr 10781 |
. . . . 5
⊢ ((𝐴 ∖ {+∞}) ⊆
ℝ* → ((𝐴 ∖ {+∞}) ⊆ ℝ ∨
+∞ ∈ (𝐴 ∖
{+∞}) ∨ -∞ ∈ (𝐴 ∖ {+∞}))) |
4 | | 3orass 1091 |
. . . . . 6
⊢ (((𝐴 ∖ {+∞}) ⊆
ℝ ∨ +∞ ∈ (𝐴 ∖ {+∞}) ∨ -∞ ∈
(𝐴 ∖ {+∞}))
↔ ((𝐴 ∖
{+∞}) ⊆ ℝ ∨ (+∞ ∈ (𝐴 ∖ {+∞}) ∨ -∞ ∈
(𝐴 ∖
{+∞})))) |
5 | | pnfex 10765 |
. . . . . . . . 9
⊢ +∞
∈ V |
6 | 5 | snid 4549 |
. . . . . . . 8
⊢ +∞
∈ {+∞} |
7 | | elndif 4017 |
. . . . . . . 8
⊢ (+∞
∈ {+∞} → ¬ +∞ ∈ (𝐴 ∖ {+∞})) |
8 | | biorf 936 |
. . . . . . . 8
⊢ (¬
+∞ ∈ (𝐴 ∖
{+∞}) → (-∞ ∈ (𝐴 ∖ {+∞}) ↔ (+∞ ∈
(𝐴 ∖ {+∞}) ∨
-∞ ∈ (𝐴 ∖
{+∞})))) |
9 | 6, 7, 8 | mp2b 10 |
. . . . . . 7
⊢ (-∞
∈ (𝐴 ∖
{+∞}) ↔ (+∞ ∈ (𝐴 ∖ {+∞}) ∨ -∞ ∈
(𝐴 ∖
{+∞}))) |
10 | 9 | orbi2i 912 |
. . . . . 6
⊢ (((𝐴 ∖ {+∞}) ⊆
ℝ ∨ -∞ ∈ (𝐴 ∖ {+∞})) ↔ ((𝐴 ∖ {+∞}) ⊆
ℝ ∨ (+∞ ∈ (𝐴 ∖ {+∞}) ∨ -∞ ∈
(𝐴 ∖
{+∞})))) |
11 | 4, 10 | bitr4i 281 |
. . . . 5
⊢ (((𝐴 ∖ {+∞}) ⊆
ℝ ∨ +∞ ∈ (𝐴 ∖ {+∞}) ∨ -∞ ∈
(𝐴 ∖ {+∞}))
↔ ((𝐴 ∖
{+∞}) ⊆ ℝ ∨ -∞ ∈ (𝐴 ∖ {+∞}))) |
12 | 3, 11 | sylib 221 |
. . . 4
⊢ ((𝐴 ∖ {+∞}) ⊆
ℝ* → ((𝐴 ∖ {+∞}) ⊆ ℝ ∨
-∞ ∈ (𝐴 ∖
{+∞}))) |
13 | | xrinfmsslem 12777 |
. . . 4
⊢ (((𝐴 ∖ {+∞}) ⊆
ℝ* ∧ ((𝐴 ∖ {+∞}) ⊆ ℝ ∨
-∞ ∈ (𝐴 ∖
{+∞}))) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∖ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∖ {+∞})𝑧 < 𝑦))) |
14 | 2, 12, 13 | syl2anc2 588 |
. . 3
⊢ (𝐴 ⊆ ℝ*
→ ∃𝑥 ∈
ℝ* (∀𝑦 ∈ (𝐴 ∖ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∖ {+∞})𝑧 < 𝑦))) |
15 | | xrinfmexpnf 12775 |
. . . 4
⊢
(∃𝑥 ∈
ℝ* (∀𝑦 ∈ (𝐴 ∖ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∖ {+∞})𝑧 < 𝑦)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞}) ¬
𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞})𝑧 < 𝑦))) |
16 | 5 | snss 4671 |
. . . . . . 7
⊢ (+∞
∈ 𝐴 ↔ {+∞}
⊆ 𝐴) |
17 | | undif 4368 |
. . . . . . . 8
⊢
({+∞} ⊆ 𝐴 ↔ ({+∞} ∪ (𝐴 ∖ {+∞})) = 𝐴) |
18 | | uncom 4041 |
. . . . . . . . 9
⊢
({+∞} ∪ (𝐴
∖ {+∞})) = ((𝐴
∖ {+∞}) ∪ {+∞}) |
19 | 18 | eqeq1i 2743 |
. . . . . . . 8
⊢
(({+∞} ∪ (𝐴 ∖ {+∞})) = 𝐴 ↔ ((𝐴 ∖ {+∞}) ∪ {+∞}) =
𝐴) |
20 | 17, 19 | bitri 278 |
. . . . . . 7
⊢
({+∞} ⊆ 𝐴 ↔ ((𝐴 ∖ {+∞}) ∪ {+∞}) =
𝐴) |
21 | 16, 20 | bitri 278 |
. . . . . 6
⊢ (+∞
∈ 𝐴 ↔ ((𝐴 ∖ {+∞}) ∪
{+∞}) = 𝐴) |
22 | | raleq 3309 |
. . . . . . 7
⊢ (((𝐴 ∖ {+∞}) ∪
{+∞}) = 𝐴 →
(∀𝑦 ∈ ((𝐴 ∖ {+∞}) ∪
{+∞}) ¬ 𝑦 <
𝑥 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥)) |
23 | | rexeq 3310 |
. . . . . . . . 9
⊢ (((𝐴 ∖ {+∞}) ∪
{+∞}) = 𝐴 →
(∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪
{+∞})𝑧 < 𝑦 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
24 | 23 | imbi2d 344 |
. . . . . . . 8
⊢ (((𝐴 ∖ {+∞}) ∪
{+∞}) = 𝐴 →
((𝑥 < 𝑦 → ∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞})𝑧 < 𝑦) ↔ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
25 | 24 | ralbidv 3109 |
. . . . . . 7
⊢ (((𝐴 ∖ {+∞}) ∪
{+∞}) = 𝐴 →
(∀𝑦 ∈
ℝ* (𝑥 <
𝑦 → ∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞})𝑧 < 𝑦) ↔ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
26 | 22, 25 | anbi12d 634 |
. . . . . 6
⊢ (((𝐴 ∖ {+∞}) ∪
{+∞}) = 𝐴 →
((∀𝑦 ∈ ((𝐴 ∖ {+∞}) ∪
{+∞}) ¬ 𝑦 <
𝑥 ∧ ∀𝑦 ∈ ℝ*
(𝑥 < 𝑦 → ∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞})𝑧 < 𝑦)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
27 | 21, 26 | sylbi 220 |
. . . . 5
⊢ (+∞
∈ 𝐴 →
((∀𝑦 ∈ ((𝐴 ∖ {+∞}) ∪
{+∞}) ¬ 𝑦 <
𝑥 ∧ ∀𝑦 ∈ ℝ*
(𝑥 < 𝑦 → ∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞})𝑧 < 𝑦)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
28 | 27 | rexbidv 3206 |
. . . 4
⊢ (+∞
∈ 𝐴 →
(∃𝑥 ∈
ℝ* (∀𝑦 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞}) ¬
𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞})𝑧 < 𝑦)) ↔ ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
29 | 15, 28 | syl5ib 247 |
. . 3
⊢ (+∞
∈ 𝐴 →
(∃𝑥 ∈
ℝ* (∀𝑦 ∈ (𝐴 ∖ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∖ {+∞})𝑧 < 𝑦)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
30 | 14, 29 | mpan9 510 |
. 2
⊢ ((𝐴 ⊆ ℝ*
∧ +∞ ∈ 𝐴)
→ ∃𝑥 ∈
ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
31 | | ssxr 10781 |
. . 3
⊢ (𝐴 ⊆ ℝ*
→ (𝐴 ⊆ ℝ
∨ +∞ ∈ 𝐴 ∨
-∞ ∈ 𝐴)) |
32 | | df-3or 1089 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∨ +∞
∈ 𝐴 ∨ -∞
∈ 𝐴) ↔ ((𝐴 ⊆ ℝ ∨ +∞
∈ 𝐴) ∨ -∞
∈ 𝐴)) |
33 | | or32 925 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∨ +∞
∈ 𝐴) ∨ -∞
∈ 𝐴) ↔ ((𝐴 ⊆ ℝ ∨ -∞
∈ 𝐴) ∨ +∞
∈ 𝐴)) |
34 | 32, 33 | bitri 278 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∨ +∞
∈ 𝐴 ∨ -∞
∈ 𝐴) ↔ ((𝐴 ⊆ ℝ ∨ -∞
∈ 𝐴) ∨ +∞
∈ 𝐴)) |
35 | 31, 34 | sylib 221 |
. 2
⊢ (𝐴 ⊆ ℝ*
→ ((𝐴 ⊆ ℝ
∨ -∞ ∈ 𝐴)
∨ +∞ ∈ 𝐴)) |
36 | 1, 30, 35 | mpjaodan 958 |
1
⊢ (𝐴 ⊆ ℝ*
→ ∃𝑥 ∈
ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |