| 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 | | nltmnf 13171 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ ¬ 𝑦 <
-∞) |
| 13 | | pnfxr 11315 |
. . . . . . . . . . . . . . . 16
⊢ +∞
∈ ℝ* |
| 14 | | elioc1 13429 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (-∞ ∈ (𝑦(,]+∞) ↔ (-∞
∈ ℝ* ∧ 𝑦 < -∞ ∧ -∞ ≤
+∞))) |
| 15 | 13, 14 | mpan2 691 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ*
→ (-∞ ∈ (𝑦(,]+∞) ↔ (-∞ ∈
ℝ* ∧ 𝑦
< -∞ ∧ -∞ ≤ +∞))) |
| 16 | | simp2 1138 |
. . . . . . . . . . . . . . 15
⊢
((-∞ ∈ ℝ* ∧ 𝑦 < -∞ ∧ -∞ ≤ +∞)
→ 𝑦 <
-∞) |
| 17 | 15, 16 | biimtrdi 253 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ (-∞ ∈ (𝑦(,]+∞) → 𝑦 < -∞)) |
| 18 | 12, 17 | mtod 198 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ ¬ -∞ ∈ (𝑦(,]+∞)) |
| 19 | | eleq2 2830 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (𝑦(,]+∞) → (-∞ ∈ 𝑢 ↔ -∞ ∈ (𝑦(,]+∞))) |
| 20 | 19 | notbid 318 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝑦(,]+∞) → (¬ -∞ ∈
𝑢 ↔ ¬ -∞
∈ (𝑦(,]+∞))) |
| 21 | 18, 20 | syl5ibrcom 247 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ (𝑢 = (𝑦(,]+∞) → ¬
-∞ ∈ 𝑢)) |
| 22 | 21 | rexlimiv 3148 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞) → ¬
-∞ ∈ 𝑢) |
| 23 | 22 | pm2.21d 121 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞) →
(-∞ ∈ 𝑢 →
∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
| 24 | 23 | adantrd 491 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
| 25 | 11, 24 | sylbi 217 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) → ((-∞
∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
| 26 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)) =
(𝑦 ∈
ℝ* ↦ (-∞[,)𝑦)) |
| 27 | 26 | elrnmpt 5969 |
. . . . . . . . . 10
⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦))) |
| 28 | 27 | elv 3485 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦)) |
| 29 | | mnfxr 11318 |
. . . . . . . . . . . . . 14
⊢ -∞
∈ ℝ* |
| 30 | 29 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ ∈
ℝ*) |
| 31 | | 0xr 11308 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ* |
| 32 | | simprl 771 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 𝑦 ∈ ℝ*) |
| 33 | | ifcl 4571 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → if(0 ≤
𝑦, 0, 𝑦) ∈
ℝ*) |
| 34 | 31, 32, 33 | sylancr 587 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ∈
ℝ*) |
| 35 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → +∞ ∈
ℝ*) |
| 36 | | mnflt0 13167 |
. . . . . . . . . . . . . 14
⊢ -∞
< 0 |
| 37 | | simpll 767 |
. . . . . . . . . . . . . . . . 17
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ ∈ 𝑢) |
| 38 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 𝑢 = (-∞[,)𝑦)) |
| 39 | 37, 38 | eleqtrd 2843 |
. . . . . . . . . . . . . . . 16
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ ∈
(-∞[,)𝑦)) |
| 40 | | elico1 13430 |
. . . . . . . . . . . . . . . . 17
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (-∞
∈ (-∞[,)𝑦)
↔ (-∞ ∈ ℝ* ∧ -∞ ≤ -∞ ∧
-∞ < 𝑦))) |
| 41 | 29, 32, 40 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞ ∈
(-∞[,)𝑦) ↔
(-∞ ∈ ℝ* ∧ -∞ ≤ -∞ ∧
-∞ < 𝑦))) |
| 42 | 39, 41 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞ ∈
ℝ* ∧ -∞ ≤ -∞ ∧ -∞ < 𝑦)) |
| 43 | 42 | simp3d 1145 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ < 𝑦) |
| 44 | | breq2 5147 |
. . . . . . . . . . . . . . 15
⊢ (0 = if(0
≤ 𝑦, 0, 𝑦) → (-∞ < 0 ↔
-∞ < if(0 ≤ 𝑦,
0, 𝑦))) |
| 45 | | breq2 5147 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = if(0 ≤ 𝑦, 0, 𝑦) → (-∞ < 𝑦 ↔ -∞ < if(0 ≤ 𝑦, 0, 𝑦))) |
| 46 | 44, 45 | ifboth 4565 |
. . . . . . . . . . . . . 14
⊢
((-∞ < 0 ∧ -∞ < 𝑦) → -∞ < if(0 ≤ 𝑦, 0, 𝑦)) |
| 47 | 36, 43, 46 | sylancr 587 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ < if(0
≤ 𝑦, 0, 𝑦)) |
| 48 | 31 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 0 ∈
ℝ*) |
| 49 | | xrmin1 13219 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → if(0 ≤
𝑦, 0, 𝑦) ≤ 0) |
| 50 | 31, 32, 49 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ≤ 0) |
| 51 | | 0re 11263 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
| 52 | | ltpnf 13162 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
ℝ → 0 < +∞) |
| 53 | 51, 52 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 0 <
+∞) |
| 54 | 34, 48, 35, 50, 53 | xrlelttrd 13202 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) < +∞) |
| 55 | | xrre2 13212 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ ℝ* ∧ if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ* ∧ +∞
∈ ℝ*) ∧ (-∞ < if(0 ≤ 𝑦, 0, 𝑦) ∧ if(0 ≤ 𝑦, 0, 𝑦) < +∞)) → if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ) |
| 56 | 30, 34, 35, 47, 54, 55 | syl32anc 1380 |
. . . . . . . . . . . 12
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ) |
| 57 | | xrmin2 13220 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → if(0 ≤
𝑦, 0, 𝑦) ≤ 𝑦) |
| 58 | 31, 32, 57 | sylancr 587 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ≤ 𝑦) |
| 59 | | df-ico 13393 |
. . . . . . . . . . . . . . 15
⊢ [,) =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 ≤ 𝑐 ∧ 𝑐 < 𝑏)}) |
| 60 | | xrltletr 13199 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → ((𝑥 < if(0 ≤ 𝑦, 0, 𝑦) ∧ if(0 ≤ 𝑦, 0, 𝑦) ≤ 𝑦) → 𝑥 < 𝑦)) |
| 61 | 59, 59, 60 | ixxss2 13406 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ*
∧ if(0 ≤ 𝑦, 0, 𝑦) ≤ 𝑦) → (-∞[,)if(0 ≤ 𝑦, 0, 𝑦)) ⊆ (-∞[,)𝑦)) |
| 62 | 32, 58, 61 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞[,)if(0 ≤
𝑦, 0, 𝑦)) ⊆ (-∞[,)𝑦)) |
| 63 | | simplr 769 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 𝑢 ⊆ 𝐴) |
| 64 | 38, 63 | eqsstrrd 4019 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞[,)𝑦) ⊆ 𝐴) |
| 65 | 62, 64 | sstrd 3994 |
. . . . . . . . . . . 12
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞[,)if(0 ≤
𝑦, 0, 𝑦)) ⊆ 𝐴) |
| 66 | | oveq2 7439 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = if(0 ≤ 𝑦, 0, 𝑦) → (-∞[,)𝑥) = (-∞[,)if(0 ≤ 𝑦, 0, 𝑦))) |
| 67 | 66 | sseq1d 4015 |
. . . . . . . . . . . . 13
⊢ (𝑥 = if(0 ≤ 𝑦, 0, 𝑦) → ((-∞[,)𝑥) ⊆ 𝐴 ↔ (-∞[,)if(0 ≤ 𝑦, 0, 𝑦)) ⊆ 𝐴)) |
| 68 | 67 | rspcev 3622 |
. . . . . . . . . . . 12
⊢ ((if(0
≤ 𝑦, 0, 𝑦) ∈ ℝ ∧
(-∞[,)if(0 ≤ 𝑦, 0,
𝑦)) ⊆ 𝐴) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴) |
| 69 | 56, 65, 68 | syl2anc 584 |
. . . . . . . . . . 11
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴) |
| 70 | 69 | rexlimdvaa 3156 |
. . . . . . . . . 10
⊢
((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → (∃𝑦 ∈ ℝ*
𝑢 = (-∞[,)𝑦) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
| 71 | 70 | com12 32 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
| 72 | 28, 71 | sylbi 217 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
| 73 | 25, 72 | jaoi 858 |
. . . . . . 7
⊢ ((𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∨ 𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
| 74 | 8, 73 | sylbi 217 |
. . . . . 6
⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
→ ((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
| 75 | | mnfnre 11304 |
. . . . . . . . . 10
⊢ -∞
∉ ℝ |
| 76 | 75 | neli 3048 |
. . . . . . . . 9
⊢ ¬
-∞ ∈ ℝ |
| 77 | | elssuni 4937 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆ ∪ ran (,)) |
| 78 | | unirnioo 13489 |
. . . . . . . . . . 11
⊢ ℝ =
∪ ran (,) |
| 79 | 77, 78 | sseqtrrdi 4025 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆
ℝ) |
| 80 | 79 | sseld 3982 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (,) → (-∞
∈ 𝑢 → -∞
∈ ℝ)) |
| 81 | 76, 80 | mtoi 199 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (,) → ¬
-∞ ∈ 𝑢) |
| 82 | 81 | pm2.21d 121 |
. . . . . . 7
⊢ (𝑢 ∈ ran (,) → (-∞
∈ 𝑢 →
∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
| 83 | 82 | adantrd 491 |
. . . . . 6
⊢ (𝑢 ∈ ran (,) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
| 84 | 74, 83 | jaoi 858 |
. . . . 5
⊢ ((𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∨ 𝑢 ∈ ran (,))
→ ((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
| 85 | 7, 84 | sylbi 217 |
. . . 4
⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
∪ ran (𝑦 ∈
ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,)) → ((-∞ ∈
𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
| 86 | 85 | rexlimiv 3148 |
. . 3
⊢
(∃𝑢 ∈
((ran (𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))(-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴) |
| 87 | 6, 86 | syl 17 |
. 2
⊢ ((𝐴 ∈ (topGen‘((ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))) ∧ -∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴) |
| 88 | 5, 87 | sylanb 581 |
1
⊢ ((𝐴 ∈ (ordTop‘ ≤ )
∧ -∞ ∈ 𝐴)
→ ∃𝑥 ∈
ℝ (-∞[,)𝑥)
⊆ 𝐴) |