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 22308 |
. . 3
⊢
(ordTop‘ ≤ ) = (topGen‘((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∪ ran (,))) |
5 | 4 | eleq2i 2828 |
. 2
⊢ (𝐴 ∈ (ordTop‘ ≤ )
↔ 𝐴 ∈
(topGen‘((ran (𝑦
∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,)))) |
6 | | tg2 22059 |
. . 3
⊢ ((𝐴 ∈ (topGen‘((ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))) ∧ -∞ ∈ 𝐴) → ∃𝑢 ∈ ((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∪ ran (,))(-∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴)) |
7 | | elun 4084 |
. . . . 5
⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
∪ ran (𝑦 ∈
ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,)) ↔ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∨ 𝑢 ∈ ran
(,))) |
8 | | elun 4084 |
. . . . . . 7
⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
↔ (𝑢 ∈ ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
∨ 𝑢 ∈ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))) |
9 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞)) =
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) |
10 | 9 | elrnmpt 5859 |
. . . . . . . . . 10
⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞))) |
11 | 10 | elv 3433 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞)) |
12 | | nltmnf 12810 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ ¬ 𝑦 <
-∞) |
13 | | pnfxr 10976 |
. . . . . . . . . . . . . . . 16
⊢ +∞
∈ ℝ* |
14 | | elioc1 13066 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (-∞ ∈ (𝑦(,]+∞) ↔ (-∞
∈ ℝ* ∧ 𝑦 < -∞ ∧ -∞ ≤
+∞))) |
15 | 13, 14 | mpan2 687 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ*
→ (-∞ ∈ (𝑦(,]+∞) ↔ (-∞ ∈
ℝ* ∧ 𝑦
< -∞ ∧ -∞ ≤ +∞))) |
16 | | simp2 1135 |
. . . . . . . . . . . . . . 15
⊢
((-∞ ∈ ℝ* ∧ 𝑦 < -∞ ∧ -∞ ≤ +∞)
→ 𝑦 <
-∞) |
17 | 15, 16 | syl6bi 252 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ (-∞ ∈ (𝑦(,]+∞) → 𝑦 < -∞)) |
18 | 12, 17 | mtod 197 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ ¬ -∞ ∈ (𝑦(,]+∞)) |
19 | | eleq2 2825 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (𝑦(,]+∞) → (-∞ ∈ 𝑢 ↔ -∞ ∈ (𝑦(,]+∞))) |
20 | 19 | notbid 317 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (𝑦(,]+∞) → (¬ -∞ ∈
𝑢 ↔ ¬ -∞
∈ (𝑦(,]+∞))) |
21 | 18, 20 | syl5ibrcom 246 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ (𝑢 = (𝑦(,]+∞) → ¬
-∞ ∈ 𝑢)) |
22 | 21 | rexlimiv 3207 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞) → ¬
-∞ ∈ 𝑢) |
23 | 22 | pm2.21d 121 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞) →
(-∞ ∈ 𝑢 →
∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
24 | 23 | adantrd 491 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
25 | 11, 24 | sylbi 216 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) → ((-∞
∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
26 | | eqid 2737 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)) =
(𝑦 ∈
ℝ* ↦ (-∞[,)𝑦)) |
27 | 26 | elrnmpt 5859 |
. . . . . . . . . 10
⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦))) |
28 | 27 | elv 3433 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦)) |
29 | | mnfxr 10979 |
. . . . . . . . . . . . . 14
⊢ -∞
∈ ℝ* |
30 | 29 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ ∈
ℝ*) |
31 | | 0xr 10969 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ* |
32 | | simprl 767 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 𝑦 ∈ ℝ*) |
33 | | ifcl 4506 |
. . . . . . . . . . . . . 14
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → if(0 ≤
𝑦, 0, 𝑦) ∈
ℝ*) |
34 | 31, 32, 33 | sylancr 586 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ∈
ℝ*) |
35 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → +∞ ∈
ℝ*) |
36 | | mnflt0 12806 |
. . . . . . . . . . . . . 14
⊢ -∞
< 0 |
37 | | simpll 763 |
. . . . . . . . . . . . . . . . 17
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ ∈ 𝑢) |
38 | | simprr 769 |
. . . . . . . . . . . . . . . . 17
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 𝑢 = (-∞[,)𝑦)) |
39 | 37, 38 | eleqtrd 2839 |
. . . . . . . . . . . . . . . 16
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ ∈
(-∞[,)𝑦)) |
40 | | elico1 13067 |
. . . . . . . . . . . . . . . . 17
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (-∞
∈ (-∞[,)𝑦)
↔ (-∞ ∈ ℝ* ∧ -∞ ≤ -∞ ∧
-∞ < 𝑦))) |
41 | 29, 32, 40 | sylancr 586 |
. . . . . . . . . . . . . . . 16
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞ ∈
(-∞[,)𝑦) ↔
(-∞ ∈ ℝ* ∧ -∞ ≤ -∞ ∧
-∞ < 𝑦))) |
42 | 39, 41 | mpbid 231 |
. . . . . . . . . . . . . . 15
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞ ∈
ℝ* ∧ -∞ ≤ -∞ ∧ -∞ < 𝑦)) |
43 | 42 | simp3d 1142 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ < 𝑦) |
44 | | breq2 5079 |
. . . . . . . . . . . . . . 15
⊢ (0 = if(0
≤ 𝑦, 0, 𝑦) → (-∞ < 0 ↔
-∞ < if(0 ≤ 𝑦,
0, 𝑦))) |
45 | | breq2 5079 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = if(0 ≤ 𝑦, 0, 𝑦) → (-∞ < 𝑦 ↔ -∞ < if(0 ≤ 𝑦, 0, 𝑦))) |
46 | 44, 45 | ifboth 4500 |
. . . . . . . . . . . . . 14
⊢
((-∞ < 0 ∧ -∞ < 𝑦) → -∞ < if(0 ≤ 𝑦, 0, 𝑦)) |
47 | 36, 43, 46 | sylancr 586 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → -∞ < if(0
≤ 𝑦, 0, 𝑦)) |
48 | 31 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 0 ∈
ℝ*) |
49 | | xrmin1 12856 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → if(0 ≤
𝑦, 0, 𝑦) ≤ 0) |
50 | 31, 32, 49 | sylancr 586 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ≤ 0) |
51 | | 0re 10924 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
52 | | ltpnf 12801 |
. . . . . . . . . . . . . . 15
⊢ (0 ∈
ℝ → 0 < +∞) |
53 | 51, 52 | mp1i 13 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 0 <
+∞) |
54 | 34, 48, 35, 50, 53 | xrlelttrd 12839 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) < +∞) |
55 | | xrre2 12849 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ ℝ* ∧ if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ* ∧ +∞
∈ ℝ*) ∧ (-∞ < if(0 ≤ 𝑦, 0, 𝑦) ∧ if(0 ≤ 𝑦, 0, 𝑦) < +∞)) → if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ) |
56 | 30, 34, 35, 47, 54, 55 | syl32anc 1376 |
. . . . . . . . . . . 12
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ) |
57 | | xrmin2 12857 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → if(0 ≤
𝑦, 0, 𝑦) ≤ 𝑦) |
58 | 31, 32, 57 | sylancr 586 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → if(0 ≤ 𝑦, 0, 𝑦) ≤ 𝑦) |
59 | | df-ico 13030 |
. . . . . . . . . . . . . . 15
⊢ [,) =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 ≤ 𝑐 ∧ 𝑐 < 𝑏)}) |
60 | | xrltletr 12836 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ*
∧ if(0 ≤ 𝑦, 0, 𝑦) ∈ ℝ*
∧ 𝑦 ∈
ℝ*) → ((𝑥 < if(0 ≤ 𝑦, 0, 𝑦) ∧ if(0 ≤ 𝑦, 0, 𝑦) ≤ 𝑦) → 𝑥 < 𝑦)) |
61 | 59, 59, 60 | ixxss2 13043 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ*
∧ if(0 ≤ 𝑦, 0, 𝑦) ≤ 𝑦) → (-∞[,)if(0 ≤ 𝑦, 0, 𝑦)) ⊆ (-∞[,)𝑦)) |
62 | 32, 58, 61 | syl2anc 583 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞[,)if(0 ≤
𝑦, 0, 𝑦)) ⊆ (-∞[,)𝑦)) |
63 | | simplr 765 |
. . . . . . . . . . . . . 14
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → 𝑢 ⊆ 𝐴) |
64 | 38, 63 | eqsstrrd 3961 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞[,)𝑦) ⊆ 𝐴) |
65 | 62, 64 | sstrd 3932 |
. . . . . . . . . . . 12
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → (-∞[,)if(0 ≤
𝑦, 0, 𝑦)) ⊆ 𝐴) |
66 | | oveq2 7268 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = if(0 ≤ 𝑦, 0, 𝑦) → (-∞[,)𝑥) = (-∞[,)if(0 ≤ 𝑦, 0, 𝑦))) |
67 | 66 | sseq1d 3953 |
. . . . . . . . . . . . 13
⊢ (𝑥 = if(0 ≤ 𝑦, 0, 𝑦) → ((-∞[,)𝑥) ⊆ 𝐴 ↔ (-∞[,)if(0 ≤ 𝑦, 0, 𝑦)) ⊆ 𝐴)) |
68 | 67 | rspcev 3557 |
. . . . . . . . . . . 12
⊢ ((if(0
≤ 𝑦, 0, 𝑦) ∈ ℝ ∧
(-∞[,)if(0 ≤ 𝑦, 0,
𝑦)) ⊆ 𝐴) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴) |
69 | 56, 65, 68 | syl2anc 583 |
. . . . . . . . . . 11
⊢
(((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (-∞[,)𝑦))) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴) |
70 | 69 | rexlimdvaa 3212 |
. . . . . . . . . 10
⊢
((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → (∃𝑦 ∈ ℝ*
𝑢 = (-∞[,)𝑦) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
71 | 70 | com12 32 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
72 | 28, 71 | sylbi 216 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
73 | 25, 72 | jaoi 853 |
. . . . . . 7
⊢ ((𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∨ 𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
74 | 8, 73 | sylbi 216 |
. . . . . 6
⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
→ ((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
75 | | mnfnre 10965 |
. . . . . . . . . 10
⊢ -∞
∉ ℝ |
76 | 75 | neli 3049 |
. . . . . . . . 9
⊢ ¬
-∞ ∈ ℝ |
77 | | elssuni 4873 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆ ∪ ran (,)) |
78 | | unirnioo 13126 |
. . . . . . . . . . 11
⊢ ℝ =
∪ ran (,) |
79 | 77, 78 | sseqtrrdi 3973 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆
ℝ) |
80 | 79 | sseld 3921 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (,) → (-∞
∈ 𝑢 → -∞
∈ ℝ)) |
81 | 76, 80 | mtoi 198 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (,) → ¬
-∞ ∈ 𝑢) |
82 | 81 | pm2.21d 121 |
. . . . . . 7
⊢ (𝑢 ∈ ran (,) → (-∞
∈ 𝑢 →
∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
83 | 82 | adantrd 491 |
. . . . . 6
⊢ (𝑢 ∈ ran (,) →
((-∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
84 | 74, 83 | jaoi 853 |
. . . . 5
⊢ ((𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∨ 𝑢 ∈ ran (,))
→ ((-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴)) |
85 | 7, 84 | sylbi 216 |
. . . 4
⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
∪ ran (𝑦 ∈
ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,)) → ((-∞ ∈
𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴)) |
86 | 85 | rexlimiv 3207 |
. . 3
⊢
(∃𝑢 ∈
((ran (𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))(-∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ
(-∞[,)𝑥) ⊆
𝐴) |
87 | 6, 86 | syl 17 |
. 2
⊢ ((𝐴 ∈ (topGen‘((ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))) ∧ -∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (-∞[,)𝑥) ⊆ 𝐴) |
88 | 5, 87 | sylanb 580 |
1
⊢ ((𝐴 ∈ (ordTop‘ ≤ )
∧ -∞ ∈ 𝐴)
→ ∃𝑥 ∈
ℝ (-∞[,)𝑥)
⊆ 𝐴) |