Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . 4
⊢ ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) = ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) |
2 | | eqid 2610 |
. . . 4
⊢ ran
(𝑦 ∈
ℝ* ↦ (-∞[,)𝑦)) = ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) |
3 | | eqid 2610 |
. . . 4
⊢ ran (,) =
ran (,) |
4 | 1, 2, 3 | leordtval 20827 |
. . 3
⊢
(ordTop‘ ≤ ) = (topGen‘((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∪ ran (,))) |
5 | 4 | eleq2i 2680 |
. 2
⊢ (𝐴 ∈ (ordTop‘ ≤ )
↔ 𝐴 ∈
(topGen‘((ran (𝑦
∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,)))) |
6 | | tg2 20580 |
. . 3
⊢ ((𝐴 ∈ (topGen‘((ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))) ∧ -∞ ∈ 𝐴) → ∃𝑢 ∈ ((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∪ ran (,))(-∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴)) |
7 | | elun 3715 |
. . . . 5
⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
∪ ran (𝑦 ∈
ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,)) ↔ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∨ 𝑢 ∈ ran
(,))) |
8 | | elun 3715 |
. . . . . . 7
⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
↔ (𝑢 ∈ ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
∨ 𝑢 ∈ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))) |
9 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
10 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞)) =
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) |
11 | 10 | elrnmpt 5293 |
. . . . . . . . . 10
⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞))) |
12 | 9, 11 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞)) |
13 | | nltmnf 11839 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ ¬ 𝑦 <
-∞) |
14 | | pnfxr 9971 |
. . . . . . . . . . . . . . . 16
⊢ +∞
∈ ℝ* |
15 | | elioc1 12088 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (-∞ ∈ (𝑦(,]+∞) ↔ (-∞
∈ ℝ* ∧ 𝑦 < -∞ ∧ -∞ ≤
+∞))) |
16 | 14, 15 | mpan2 703 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ*
→ (-∞ ∈ (𝑦(,]+∞) ↔ (-∞ ∈
ℝ* ∧ 𝑦
< -∞ ∧ -∞ ≤ +∞))) |
17 | | simp2 1055 |
. . . . . . . . . . . . . . 15
⊢
((-∞ ∈ ℝ* ∧ 𝑦 < -∞ ∧ -∞ ≤ +∞)
→ 𝑦 <
-∞) |
18 | 16, 17 | syl6bi 242 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ (-∞ ∈ (𝑦(,]+∞) → 𝑦 < -∞)) |
19 | 13, 18 | mtod 188 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ ¬ -∞ ∈ (𝑦(,]+∞)) |
20 | | eleq2 2677 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (𝑦(,]+∞) → (-∞ ∈ 𝑢 ↔ -∞ ∈ (𝑦(,]+∞))) |
21 | 20 | notbid 307 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝑦(,]+∞) → (¬ -∞ ∈
𝑢 ↔ ¬ -∞
∈ (𝑦(,]+∞))) |
22 | 19, 21 | syl5ibrcom 236 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ (𝑢 = (𝑦(,]+∞) → ¬
-∞ ∈ 𝑢)) |
23 | 22 | rexlimiv 3009 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞) → ¬
-∞ ∈ 𝑢) |
24 | 23 | pm2.21d 117 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞) →
(-∞ ∈ 𝑢 →
∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
25 | 24 | adantrd 483 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
26 | 12, 25 | sylbi 206 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) → ((-∞
∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
27 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)) =
(𝑦 ∈
ℝ* ↦ (-∞[,)𝑦)) |
28 | 27 | elrnmpt 5293 |
. . . . . . . . . 10
⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦))) |
29 | 9, 28 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦)) |
30 | | mnfxr 9975 |
. . . . . . . . . . . . . 14
⊢ -∞
∈ ℝ* |
31 | 30 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ ∈
ℝ*) |
32 | | 0xr 9965 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ* |
33 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 𝑦 ∈ ℝ*) |
34 | | ifcl 4080 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → if(0 ≤
𝑦, 0, 𝑦) ∈
ℝ*) |
35 | 32, 33, 34 | sylancr 694 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ∈
ℝ*) |
36 | 14 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → +∞ ∈
ℝ*) |
37 | | mnflt0 11835 |
. . . . . . . . . . . . . 14
⊢ -∞
< 0 |
38 | | simpll 786 |
. . . . . . . . . . . . . . . . 17
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ ∈ 𝑢) |
39 | | simprr 792 |
. . . . . . . . . . . . . . . . 17
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 𝑢 = (-∞[,)𝑦)) |
40 | 38, 39 | eleqtrd 2690 |
. . . . . . . . . . . . . . . 16
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ ∈
(-∞[,)𝑦)) |
41 | | elico1 12089 |
. . . . . . . . . . . . . . . . 17
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (-∞
∈ (-∞[,)𝑦)
↔ (-∞ ∈ ℝ* ∧ -∞ ≤ -∞ ∧
-∞ < 𝑦))) |
42 | 30, 33, 41 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞ ∈
(-∞[,)𝑦) ↔
(-∞ ∈ ℝ* ∧ -∞ ≤ -∞ ∧
-∞ < 𝑦))) |
43 | 40, 42 | mpbid 221 |
. . . . . . . . . . . . . . 15
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞ ∈
ℝ* ∧ -∞ ≤ -∞ ∧ -∞ < 𝑦)) |
44 | 43 | simp3d 1068 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ < 𝑦) |
45 | | breq2 4587 |
. . . . . . . . . . . . . . 15
⊢ (0 = if(0
≤ 𝑦, 0, 𝑦) → (-∞ < 0 ↔
-∞ < if(0 ≤ 𝑦,
0, 𝑦))) |
46 | | breq2 4587 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = if(0 ≤ 𝑦, 0, 𝑦) → (-∞ < 𝑦 ↔ -∞ < if(0 ≤ 𝑦, 0, 𝑦))) |
47 | 45, 46 | ifboth 4074 |
. . . . . . . . . . . . . 14
⊢
((-∞ < 0 ∧ -∞ < 𝑦) → -∞ < if(0 ≤ 𝑦, 0, 𝑦)) |
48 | 37, 44, 47 | sylancr 694 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ < if(0
≤ 𝑦, 0, 𝑦)) |
49 | 32 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 0 ∈
ℝ*) |
50 | | xrmin1 11882 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → if(0 ≤
𝑦, 0, 𝑦) ≤ 0) |
51 | 32, 33, 50 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ≤ 0) |
52 | | 0re 9919 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
53 | | ltpnf 11830 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
ℝ → 0 < +∞) |
54 | 52, 53 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 0 <
+∞) |
55 | 35, 49, 36, 51, 54 | xrlelttrd 11867 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) < +∞) |
56 | | xrre2 11875 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ ℝ* ∧ if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ* ∧ +∞
∈ ℝ*) ∧ (-∞ < if(0 ≤ 𝑦, 0, 𝑦) ∧ if(0 ≤ 𝑦, 0, 𝑦) < +∞)) → if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ) |
57 | 31, 35, 36, 48, 55, 56 | syl32anc 1326 |
. . . . . . . . . . . 12
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ) |
58 | | xrmin2 11883 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → if(0 ≤
𝑦, 0, 𝑦) ≤ 𝑦) |
59 | 32, 33, 58 | sylancr 694 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ≤ 𝑦) |
60 | | df-ico 12052 |
. . . . . . . . . . . . . . 15
⊢ [,) =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 ≤ 𝑐 ∧ 𝑐 < 𝑏)}) |
61 | | xrltletr 11864 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → ((𝑥 < if(0 ≤ 𝑦, 0, 𝑦) ∧ if(0 ≤ 𝑦, 0, 𝑦) ≤ 𝑦) → 𝑥 < 𝑦)) |
62 | 60, 60, 61 | ixxss2 12065 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ*
∧ if(0 ≤ 𝑦, 0, 𝑦) ≤ 𝑦) → (-∞[,)if(0 ≤ 𝑦, 0, 𝑦)) ⊆ (-∞[,)𝑦)) |
63 | 33, 59, 62 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞[,)if(0 ≤
𝑦, 0, 𝑦)) ⊆ (-∞[,)𝑦)) |
64 | | simplr 788 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 𝑢 ⊆ 𝐴) |
65 | 39, 64 | eqsstr3d 3603 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞[,)𝑦) ⊆ 𝐴) |
66 | 63, 65 | sstrd 3578 |
. . . . . . . . . . . 12
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞[,)if(0 ≤
𝑦, 0, 𝑦)) ⊆ 𝐴) |
67 | | oveq2 6557 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = if(0 ≤ 𝑦, 0, 𝑦) → (-∞[,)𝑥) = (-∞[,)if(0 ≤ 𝑦, 0, 𝑦))) |
68 | 67 | sseq1d 3595 |
. . . . . . . . . . . . 13
⊢ (𝑥 = if(0 ≤ 𝑦, 0, 𝑦) → ((-∞[,)𝑥) ⊆ 𝐴 ↔ (-∞[,)if(0 ≤ 𝑦, 0, 𝑦)) ⊆ 𝐴)) |
69 | 68 | rspcev 3282 |
. . . . . . . . . . . 12
⊢ ((if(0
≤ 𝑦, 0, 𝑦) ∈ ℝ ∧
(-∞[,)if(0 ≤ 𝑦, 0,
𝑦)) ⊆ 𝐴) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴) |
70 | 57, 66, 69 | syl2anc 691 |
. . . . . . . . . . 11
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴) |
71 | 70 | rexlimdvaa 3014 |
. . . . . . . . . 10
⊢
((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → (∃𝑦 ∈ ℝ*
𝑢 = (-∞[,)𝑦) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
72 | 71 | com12 32 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
73 | 29, 72 | sylbi 206 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
74 | 26, 73 | jaoi 393 |
. . . . . . 7
⊢ ((𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∨ 𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
75 | 8, 74 | sylbi 206 |
. . . . . 6
⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
→ ((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
76 | | mnfnre 9961 |
. . . . . . . . . 10
⊢ -∞
∉ ℝ |
77 | 76 | neli 2885 |
. . . . . . . . 9
⊢ ¬
-∞ ∈ ℝ |
78 | | elssuni 4403 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆ ∪ ran (,)) |
79 | | unirnioo 12144 |
. . . . . . . . . . 11
⊢ ℝ =
∪ ran (,) |
80 | 78, 79 | syl6sseqr 3615 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆
ℝ) |
81 | 80 | sseld 3567 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (,) → (-∞
∈ 𝑢 → -∞
∈ ℝ)) |
82 | 77, 81 | mtoi 189 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (,) → ¬
-∞ ∈ 𝑢) |
83 | 82 | pm2.21d 117 |
. . . . . . 7
⊢ (𝑢 ∈ ran (,) → (-∞
∈ 𝑢 →
∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
84 | 83 | adantrd 483 |
. . . . . 6
⊢ (𝑢 ∈ ran (,) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
85 | 75, 84 | jaoi 393 |
. . . . 5
⊢ ((𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∨ 𝑢 ∈ ran (,))
→ ((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
86 | 7, 85 | sylbi 206 |
. . . 4
⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
∪ ran (𝑦 ∈
ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,)) → ((-∞ ∈
𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
87 | 86 | rexlimiv 3009 |
. . 3
⊢
(∃𝑢 ∈
((ran (𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))(-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴) |
88 | 6, 87 | syl 17 |
. 2
⊢ ((𝐴 ∈ (topGen‘((ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))) ∧ -∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴) |
89 | 5, 88 | sylanb 488 |
1
⊢ ((𝐴 ∈ (ordTop‘ ≤ )
∧ -∞ ∈ 𝐴)
→ ∃𝑥 ∈
ℝ (-∞[,)𝑥)
⊆ 𝐴) |