Proof of Theorem xrinfmss
Step | Hyp | Ref
| Expression |
1 | | xrinfmsslem 12426 |
. 2
⊢ ((𝐴 ⊆ ℝ*
∧ (𝐴 ⊆ ℝ
∨ -∞ ∈ 𝐴))
→ ∃𝑥 ∈
ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
2 | | ssdifss 3968 |
. . . 4
⊢ (𝐴 ⊆ ℝ*
→ (𝐴 ∖
{+∞}) ⊆ ℝ*) |
3 | | ssxr 10426 |
. . . . . 6
⊢ ((𝐴 ∖ {+∞}) ⊆
ℝ* → ((𝐴 ∖ {+∞}) ⊆ ℝ ∨
+∞ ∈ (𝐴 ∖
{+∞}) ∨ -∞ ∈ (𝐴 ∖ {+∞}))) |
4 | | 3orass 1114 |
. . . . . . 7
⊢ (((𝐴 ∖ {+∞}) ⊆
ℝ ∨ +∞ ∈ (𝐴 ∖ {+∞}) ∨ -∞ ∈
(𝐴 ∖ {+∞}))
↔ ((𝐴 ∖
{+∞}) ⊆ ℝ ∨ (+∞ ∈ (𝐴 ∖ {+∞}) ∨ -∞ ∈
(𝐴 ∖
{+∞})))) |
5 | | pnfex 10409 |
. . . . . . . . . 10
⊢ +∞
∈ V |
6 | 5 | snid 4429 |
. . . . . . . . 9
⊢ +∞
∈ {+∞} |
7 | | elndif 3961 |
. . . . . . . . 9
⊢ (+∞
∈ {+∞} → ¬ +∞ ∈ (𝐴 ∖ {+∞})) |
8 | | biorf 965 |
. . . . . . . . 9
⊢ (¬
+∞ ∈ (𝐴 ∖
{+∞}) → (-∞ ∈ (𝐴 ∖ {+∞}) ↔ (+∞ ∈
(𝐴 ∖ {+∞}) ∨
-∞ ∈ (𝐴 ∖
{+∞})))) |
9 | 6, 7, 8 | mp2b 10 |
. . . . . . . 8
⊢ (-∞
∈ (𝐴 ∖
{+∞}) ↔ (+∞ ∈ (𝐴 ∖ {+∞}) ∨ -∞ ∈
(𝐴 ∖
{+∞}))) |
10 | 9 | orbi2i 941 |
. . . . . . 7
⊢ (((𝐴 ∖ {+∞}) ⊆
ℝ ∨ -∞ ∈ (𝐴 ∖ {+∞})) ↔ ((𝐴 ∖ {+∞}) ⊆
ℝ ∨ (+∞ ∈ (𝐴 ∖ {+∞}) ∨ -∞ ∈
(𝐴 ∖
{+∞})))) |
11 | 4, 10 | bitr4i 270 |
. . . . . 6
⊢ (((𝐴 ∖ {+∞}) ⊆
ℝ ∨ +∞ ∈ (𝐴 ∖ {+∞}) ∨ -∞ ∈
(𝐴 ∖ {+∞}))
↔ ((𝐴 ∖
{+∞}) ⊆ ℝ ∨ -∞ ∈ (𝐴 ∖ {+∞}))) |
12 | 3, 11 | sylib 210 |
. . . . 5
⊢ ((𝐴 ∖ {+∞}) ⊆
ℝ* → ((𝐴 ∖ {+∞}) ⊆ ℝ ∨
-∞ ∈ (𝐴 ∖
{+∞}))) |
13 | | xrinfmsslem 12426 |
. . . . 5
⊢ (((𝐴 ∖ {+∞}) ⊆
ℝ* ∧ ((𝐴 ∖ {+∞}) ⊆ ℝ ∨
-∞ ∈ (𝐴 ∖
{+∞}))) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∖ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∖ {+∞})𝑧 < 𝑦))) |
14 | 12, 13 | mpdan 678 |
. . . 4
⊢ ((𝐴 ∖ {+∞}) ⊆
ℝ* → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ (𝐴 ∖ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∖ {+∞})𝑧 < 𝑦))) |
15 | 2, 14 | syl 17 |
. . 3
⊢ (𝐴 ⊆ ℝ*
→ ∃𝑥 ∈
ℝ* (∀𝑦 ∈ (𝐴 ∖ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∖ {+∞})𝑧 < 𝑦))) |
16 | | xrinfmexpnf 12424 |
. . . 4
⊢
(∃𝑥 ∈
ℝ* (∀𝑦 ∈ (𝐴 ∖ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∖ {+∞})𝑧 < 𝑦)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞}) ¬
𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞})𝑧 < 𝑦))) |
17 | 5 | snss 4535 |
. . . . . . 7
⊢ (+∞
∈ 𝐴 ↔ {+∞}
⊆ 𝐴) |
18 | | undif 4272 |
. . . . . . . 8
⊢
({+∞} ⊆ 𝐴 ↔ ({+∞} ∪ (𝐴 ∖ {+∞})) = 𝐴) |
19 | | uncom 3984 |
. . . . . . . . 9
⊢
({+∞} ∪ (𝐴
∖ {+∞})) = ((𝐴
∖ {+∞}) ∪ {+∞}) |
20 | 19 | eqeq1i 2830 |
. . . . . . . 8
⊢
(({+∞} ∪ (𝐴 ∖ {+∞})) = 𝐴 ↔ ((𝐴 ∖ {+∞}) ∪ {+∞}) =
𝐴) |
21 | 18, 20 | bitri 267 |
. . . . . . 7
⊢
({+∞} ⊆ 𝐴 ↔ ((𝐴 ∖ {+∞}) ∪ {+∞}) =
𝐴) |
22 | 17, 21 | bitri 267 |
. . . . . 6
⊢ (+∞
∈ 𝐴 ↔ ((𝐴 ∖ {+∞}) ∪
{+∞}) = 𝐴) |
23 | | raleq 3350 |
. . . . . . 7
⊢ (((𝐴 ∖ {+∞}) ∪
{+∞}) = 𝐴 →
(∀𝑦 ∈ ((𝐴 ∖ {+∞}) ∪
{+∞}) ¬ 𝑦 <
𝑥 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥)) |
24 | | rexeq 3351 |
. . . . . . . . 9
⊢ (((𝐴 ∖ {+∞}) ∪
{+∞}) = 𝐴 →
(∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪
{+∞})𝑧 < 𝑦 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) |
25 | 24 | imbi2d 332 |
. . . . . . . 8
⊢ (((𝐴 ∖ {+∞}) ∪
{+∞}) = 𝐴 →
((𝑥 < 𝑦 → ∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞})𝑧 < 𝑦) ↔ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
26 | 25 | ralbidv 3195 |
. . . . . . 7
⊢ (((𝐴 ∖ {+∞}) ∪
{+∞}) = 𝐴 →
(∀𝑦 ∈
ℝ* (𝑥 <
𝑦 → ∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞})𝑧 < 𝑦) ↔ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
27 | 23, 26 | anbi12d 624 |
. . . . . 6
⊢ (((𝐴 ∖ {+∞}) ∪
{+∞}) = 𝐴 →
((∀𝑦 ∈ ((𝐴 ∖ {+∞}) ∪
{+∞}) ¬ 𝑦 <
𝑥 ∧ ∀𝑦 ∈ ℝ*
(𝑥 < 𝑦 → ∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞})𝑧 < 𝑦)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
28 | 22, 27 | sylbi 209 |
. . . . 5
⊢ (+∞
∈ 𝐴 →
((∀𝑦 ∈ ((𝐴 ∖ {+∞}) ∪
{+∞}) ¬ 𝑦 <
𝑥 ∧ ∀𝑦 ∈ ℝ*
(𝑥 < 𝑦 → ∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞})𝑧 < 𝑦)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
29 | 28 | rexbidv 3262 |
. . . 4
⊢ (+∞
∈ 𝐴 →
(∃𝑥 ∈
ℝ* (∀𝑦 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞}) ¬
𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ ((𝐴 ∖ {+∞}) ∪ {+∞})𝑧 < 𝑦)) ↔ ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
30 | 16, 29 | syl5ib 236 |
. . 3
⊢ (+∞
∈ 𝐴 →
(∃𝑥 ∈
ℝ* (∀𝑦 ∈ (𝐴 ∖ {+∞}) ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ (𝐴 ∖ {+∞})𝑧 < 𝑦)) → ∃𝑥 ∈ ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))) |
31 | 15, 30 | mpan9 502 |
. 2
⊢ ((𝐴 ⊆ ℝ*
∧ +∞ ∈ 𝐴)
→ ∃𝑥 ∈
ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |
32 | | ssxr 10426 |
. . 3
⊢ (𝐴 ⊆ ℝ*
→ (𝐴 ⊆ ℝ
∨ +∞ ∈ 𝐴 ∨
-∞ ∈ 𝐴)) |
33 | | df-3or 1112 |
. . . 4
⊢ ((𝐴 ⊆ ℝ ∨ +∞
∈ 𝐴 ∨ -∞
∈ 𝐴) ↔ ((𝐴 ⊆ ℝ ∨ +∞
∈ 𝐴) ∨ -∞
∈ 𝐴)) |
34 | | or32 954 |
. . . 4
⊢ (((𝐴 ⊆ ℝ ∨ +∞
∈ 𝐴) ∨ -∞
∈ 𝐴) ↔ ((𝐴 ⊆ ℝ ∨ -∞
∈ 𝐴) ∨ +∞
∈ 𝐴)) |
35 | 33, 34 | bitri 267 |
. . 3
⊢ ((𝐴 ⊆ ℝ ∨ +∞
∈ 𝐴 ∨ -∞
∈ 𝐴) ↔ ((𝐴 ⊆ ℝ ∨ -∞
∈ 𝐴) ∨ +∞
∈ 𝐴)) |
36 | 32, 35 | sylib 210 |
. 2
⊢ (𝐴 ⊆ ℝ*
→ ((𝐴 ⊆ ℝ
∨ -∞ ∈ 𝐴)
∨ +∞ ∈ 𝐴)) |
37 | 1, 31, 36 | mpjaodan 986 |
1
⊢ (𝐴 ⊆ ℝ*
→ ∃𝑥 ∈
ℝ* (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ* (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))) |