| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . 4
⊢ ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) = ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) |
| 2 | | eqid 2737 |
. . . 4
⊢ ran
(𝑦 ∈
ℝ* ↦ (-∞[,)𝑦)) = ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) |
| 3 | | eqid 2737 |
. . . 4
⊢ ran (,) =
ran (,) |
| 4 | 1, 2, 3 | leordtval 23221 |
. . 3
⊢
(ordTop‘ ≤ ) = (topGen‘((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∪ ran (,))) |
| 5 | 4 | eleq2i 2833 |
. 2
⊢ (𝐴 ∈ (ordTop‘ ≤ )
↔ 𝐴 ∈
(topGen‘((ran (𝑦
∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,)))) |
| 6 | | tg2 22972 |
. . 3
⊢ ((𝐴 ∈ (topGen‘((ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))) ∧ +∞ ∈ 𝐴) → ∃𝑢 ∈ ((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∪ ran (,))(+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴)) |
| 7 | | elun 4153 |
. . . . 5
⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
∪ ran (𝑦 ∈
ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,)) ↔ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∨ 𝑢 ∈ ran
(,))) |
| 8 | | elun 4153 |
. . . . . . 7
⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
↔ (𝑢 ∈ ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
∨ 𝑢 ∈ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))) |
| 9 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞)) =
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) |
| 10 | 9 | elrnmpt 5969 |
. . . . . . . . . 10
⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞))) |
| 11 | 10 | elv 3485 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞)) |
| 12 | | mnfxr 11318 |
. . . . . . . . . . . . . 14
⊢ -∞
∈ ℝ* |
| 13 | 12 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → -∞ ∈
ℝ*) |
| 14 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 ∈ ℝ*) |
| 15 | | 0xr 11308 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ* |
| 16 | | ifcl 4571 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ*
∧ 0 ∈ ℝ*) → if(0 ≤ 𝑦, 𝑦, 0) ∈
ℝ*) |
| 17 | 14, 15, 16 | sylancl 586 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) ∈
ℝ*) |
| 18 | | pnfxr 11315 |
. . . . . . . . . . . . . 14
⊢ +∞
∈ ℝ* |
| 19 | 18 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈
ℝ*) |
| 20 | | xrmax1 13217 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → 0 ≤
if(0 ≤ 𝑦, 𝑦, 0)) |
| 21 | 15, 14, 20 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
| 22 | | ge0gtmnf 13214 |
. . . . . . . . . . . . . 14
⊢ ((if(0
≤ 𝑦, 𝑦, 0) ∈ ℝ* ∧ 0 ≤
if(0 ≤ 𝑦, 𝑦, 0)) → -∞ < if(0
≤ 𝑦, 𝑦, 0)) |
| 23 | 17, 21, 22 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → -∞ < if(0 ≤
𝑦, 𝑦, 0)) |
| 24 | | simpll 767 |
. . . . . . . . . . . . . . . . 17
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈ 𝑢) |
| 25 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑢 = (𝑦(,]+∞)) |
| 26 | 24, 25 | eleqtrd 2843 |
. . . . . . . . . . . . . . . 16
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈ (𝑦(,]+∞)) |
| 27 | | elioc1 13429 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (+∞ ∈ (𝑦(,]+∞) ↔ (+∞
∈ ℝ* ∧ 𝑦 < +∞ ∧ +∞ ≤
+∞))) |
| 28 | 14, 18, 27 | sylancl 586 |
. . . . . . . . . . . . . . . 16
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → (+∞ ∈ (𝑦(,]+∞) ↔ (+∞
∈ ℝ* ∧ 𝑦 < +∞ ∧ +∞ ≤
+∞))) |
| 29 | 26, 28 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → (+∞ ∈
ℝ* ∧ 𝑦
< +∞ ∧ +∞ ≤ +∞)) |
| 30 | 29 | simp2d 1144 |
. . . . . . . . . . . . . 14
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 < +∞) |
| 31 | | 0ltpnf 13164 |
. . . . . . . . . . . . . 14
⊢ 0 <
+∞ |
| 32 | | breq1 5146 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = if(0 ≤ 𝑦, 𝑦, 0) → (𝑦 < +∞ ↔ if(0 ≤ 𝑦, 𝑦, 0) < +∞)) |
| 33 | | breq1 5146 |
. . . . . . . . . . . . . . 15
⊢ (0 = if(0
≤ 𝑦, 𝑦, 0) → (0 < +∞ ↔ if(0 ≤
𝑦, 𝑦, 0) < +∞)) |
| 34 | 32, 33 | ifboth 4565 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 < +∞ ∧ 0 <
+∞) → if(0 ≤ 𝑦, 𝑦, 0) < +∞) |
| 35 | 30, 31, 34 | sylancl 586 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) < +∞) |
| 36 | | xrre2 13212 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ ℝ* ∧ if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ* ∧
+∞ ∈ ℝ*) ∧ (-∞ < if(0 ≤ 𝑦, 𝑦, 0) ∧ if(0 ≤ 𝑦, 𝑦, 0) < +∞)) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
| 37 | 13, 17, 19, 23, 35, 36 | syl32anc 1380 |
. . . . . . . . . . . 12
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
| 38 | | xrmax2 13218 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
| 39 | 15, 14, 38 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
| 40 | | df-ioc 13392 |
. . . . . . . . . . . . . . 15
⊢ (,] =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 < 𝑐 ∧ 𝑐 ≤ 𝑏)}) |
| 41 | | xrlelttr 13198 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ*
∧ if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → ((𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0) ∧ if(0 ≤ 𝑦, 𝑦, 0) < 𝑥) → 𝑦 < 𝑥)) |
| 42 | 40, 40, 41 | ixxss1 13405 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ*
∧ 𝑦 ≤ if(0 ≤
𝑦, 𝑦, 0)) → (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ (𝑦(,]+∞)) |
| 43 | 14, 39, 42 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ (𝑦(,]+∞)) |
| 44 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑢 ⊆ 𝐴) |
| 45 | 25, 44 | eqsstrrd 4019 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → (𝑦(,]+∞) ⊆ 𝐴) |
| 46 | 43, 45 | sstrd 3994 |
. . . . . . . . . . . 12
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴) |
| 47 | | oveq1 7438 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = if(0 ≤ 𝑦, 𝑦, 0) → (𝑥(,]+∞) = (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞)) |
| 48 | 47 | sseq1d 4015 |
. . . . . . . . . . . . 13
⊢ (𝑥 = if(0 ≤ 𝑦, 𝑦, 0) → ((𝑥(,]+∞) ⊆ 𝐴 ↔ (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴)) |
| 49 | 48 | rspcev 3622 |
. . . . . . . . . . . 12
⊢ ((if(0
≤ 𝑦, 𝑦, 0) ∈ ℝ ∧ (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) |
| 50 | 37, 46, 49 | syl2anc 584 |
. . . . . . . . . . 11
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) |
| 51 | 50 | rexlimdvaa 3156 |
. . . . . . . . . 10
⊢
((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → (∃𝑦 ∈ ℝ*
𝑢 = (𝑦(,]+∞) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
| 52 | 51 | com12 32 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞) →
((+∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
| 53 | 11, 52 | sylbi 217 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) → ((+∞
∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
| 54 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)) =
(𝑦 ∈
ℝ* ↦ (-∞[,)𝑦)) |
| 55 | 54 | elrnmpt 5969 |
. . . . . . . . . 10
⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦))) |
| 56 | 55 | elv 3485 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦)) |
| 57 | | pnfnlt 13170 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ ¬ +∞ < 𝑦) |
| 58 | | elico1 13430 |
. . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (+∞
∈ (-∞[,)𝑦)
↔ (+∞ ∈ ℝ* ∧ -∞ ≤ +∞ ∧
+∞ < 𝑦))) |
| 59 | 12, 58 | mpan 690 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ*
→ (+∞ ∈ (-∞[,)𝑦) ↔ (+∞ ∈ ℝ*
∧ -∞ ≤ +∞ ∧ +∞ < 𝑦))) |
| 60 | | simp3 1139 |
. . . . . . . . . . . . . . 15
⊢
((+∞ ∈ ℝ* ∧ -∞ ≤ +∞ ∧
+∞ < 𝑦) →
+∞ < 𝑦) |
| 61 | 59, 60 | biimtrdi 253 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ (+∞ ∈ (-∞[,)𝑦) → +∞ < 𝑦)) |
| 62 | 57, 61 | mtod 198 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ ¬ +∞ ∈ (-∞[,)𝑦)) |
| 63 | | eleq2 2830 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (-∞[,)𝑦) → (+∞ ∈ 𝑢 ↔ +∞ ∈
(-∞[,)𝑦))) |
| 64 | 63 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (-∞[,)𝑦) → (¬ +∞ ∈
𝑢 ↔ ¬ +∞
∈ (-∞[,)𝑦))) |
| 65 | 62, 64 | syl5ibrcom 247 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ (𝑢 =
(-∞[,)𝑦) → ¬
+∞ ∈ 𝑢)) |
| 66 | 65 | rexlimiv 3148 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦) → ¬
+∞ ∈ 𝑢) |
| 67 | 66 | pm2.21d 121 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦) →
(+∞ ∈ 𝑢 →
∃𝑥 ∈ ℝ
(𝑥(,]+∞) ⊆
𝐴)) |
| 68 | 67 | adantrd 491 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦) →
((+∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
| 69 | 56, 68 | sylbi 217 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) →
((+∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
| 70 | 53, 69 | jaoi 858 |
. . . . . . 7
⊢ ((𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∨ 𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) →
((+∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
| 71 | 8, 70 | sylbi 217 |
. . . . . 6
⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
→ ((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
| 72 | | pnfnre 11302 |
. . . . . . . . . 10
⊢ +∞
∉ ℝ |
| 73 | 72 | neli 3048 |
. . . . . . . . 9
⊢ ¬
+∞ ∈ ℝ |
| 74 | | elssuni 4937 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆ ∪ ran (,)) |
| 75 | | unirnioo 13489 |
. . . . . . . . . . 11
⊢ ℝ =
∪ ran (,) |
| 76 | 74, 75 | sseqtrrdi 4025 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆
ℝ) |
| 77 | 76 | sseld 3982 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (,) → (+∞
∈ 𝑢 → +∞
∈ ℝ)) |
| 78 | 73, 77 | mtoi 199 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (,) → ¬
+∞ ∈ 𝑢) |
| 79 | 78 | pm2.21d 121 |
. . . . . . 7
⊢ (𝑢 ∈ ran (,) → (+∞
∈ 𝑢 →
∃𝑥 ∈ ℝ
(𝑥(,]+∞) ⊆
𝐴)) |
| 80 | 79 | adantrd 491 |
. . . . . 6
⊢ (𝑢 ∈ ran (,) →
((+∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
| 81 | 71, 80 | jaoi 858 |
. . . . 5
⊢ ((𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∨ 𝑢 ∈ ran (,))
→ ((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
| 82 | 7, 81 | sylbi 217 |
. . . 4
⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
∪ ran (𝑦 ∈
ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,)) → ((+∞ ∈
𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
| 83 | 82 | rexlimiv 3148 |
. . 3
⊢
(∃𝑢 ∈
((ran (𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))(+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) |
| 84 | 6, 83 | syl 17 |
. 2
⊢ ((𝐴 ∈ (topGen‘((ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))) ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) |
| 85 | 5, 84 | sylanb 581 |
1
⊢ ((𝐴 ∈ (ordTop‘ ≤ )
∧ +∞ ∈ 𝐴)
→ ∃𝑥 ∈
ℝ (𝑥(,]+∞)
⊆ 𝐴) |