Step | Hyp | Ref
| Expression |
1 | | eqid 2622 |
. . . 4
⊢ ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) = ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) |
2 | | eqid 2622 |
. . . 4
⊢ ran
(𝑦 ∈
ℝ* ↦ (-∞[,)𝑦)) = ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) |
3 | | eqid 2622 |
. . . 4
⊢ ran (,) =
ran (,) |
4 | 1, 2, 3 | leordtval 21017 |
. . 3
⊢
(ordTop‘ ≤ ) = (topGen‘((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∪ ran (,))) |
5 | 4 | eleq2i 2693 |
. 2
⊢ (𝐴 ∈ (ordTop‘ ≤ )
↔ 𝐴 ∈
(topGen‘((ran (𝑦
∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,)))) |
6 | | tg2 20769 |
. . 3
⊢ ((𝐴 ∈ (topGen‘((ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))) ∧ +∞ ∈ 𝐴) → ∃𝑢 ∈ ((ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∪ ran (,))(+∞ ∈ 𝑢 ∧ 𝑢 ⊆ 𝐴)) |
7 | | elun 3753 |
. . . . 5
⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
∪ ran (𝑦 ∈
ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,)) ↔ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∨ 𝑢 ∈ ran
(,))) |
8 | | elun 3753 |
. . . . . . 7
⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
↔ (𝑢 ∈ ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
∨ 𝑢 ∈ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))) |
9 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
10 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞)) =
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) |
11 | 10 | elrnmpt 5372 |
. . . . . . . . . 10
⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞))) |
12 | 9, 11 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞)) |
13 | | mnfxr 10096 |
. . . . . . . . . . . . . 14
⊢ -∞
∈ ℝ* |
14 | 13 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → -∞ ∈
ℝ*) |
15 | | simprl 794 |
. . . . . . . . . . . . . 14
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 ∈ ℝ*) |
16 | | 0xr 10086 |
. . . . . . . . . . . . . 14
⊢ 0 ∈
ℝ* |
17 | | ifcl 4130 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ*
∧ 0 ∈ ℝ*) → if(0 ≤ 𝑦, 𝑦, 0) ∈
ℝ*) |
18 | 15, 16, 17 | sylancl 694 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) ∈
ℝ*) |
19 | | pnfxr 10092 |
. . . . . . . . . . . . . 14
⊢ +∞
∈ ℝ* |
20 | 19 | a1i 11 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈
ℝ*) |
21 | | xrmax1 12006 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → 0 ≤
if(0 ≤ 𝑦, 𝑦, 0)) |
22 | 16, 15, 21 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → 0 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
23 | | ge0gtmnf 12003 |
. . . . . . . . . . . . . 14
⊢ ((if(0
≤ 𝑦, 𝑦, 0) ∈ ℝ* ∧ 0 ≤
if(0 ≤ 𝑦, 𝑦, 0)) → -∞ < if(0
≤ 𝑦, 𝑦, 0)) |
24 | 18, 22, 23 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → -∞ < if(0 ≤
𝑦, 𝑦, 0)) |
25 | | simpll 790 |
. . . . . . . . . . . . . . . . 17
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈ 𝑢) |
26 | | simprr 796 |
. . . . . . . . . . . . . . . . 17
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑢 = (𝑦(,]+∞)) |
27 | 25, 26 | eleqtrd 2703 |
. . . . . . . . . . . . . . . 16
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → +∞ ∈ (𝑦(,]+∞)) |
28 | | elioc1 12217 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℝ*
∧ +∞ ∈ ℝ*) → (+∞ ∈ (𝑦(,]+∞) ↔ (+∞
∈ ℝ* ∧ 𝑦 < +∞ ∧ +∞ ≤
+∞))) |
29 | 15, 19, 28 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → (+∞ ∈ (𝑦(,]+∞) ↔ (+∞
∈ ℝ* ∧ 𝑦 < +∞ ∧ +∞ ≤
+∞))) |
30 | 27, 29 | mpbid 222 |
. . . . . . . . . . . . . . 15
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → (+∞ ∈
ℝ* ∧ 𝑦
< +∞ ∧ +∞ ≤ +∞)) |
31 | 30 | simp2d 1074 |
. . . . . . . . . . . . . 14
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 < +∞) |
32 | | 0ltpnf 11956 |
. . . . . . . . . . . . . 14
⊢ 0 <
+∞ |
33 | | breq1 4656 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = if(0 ≤ 𝑦, 𝑦, 0) → (𝑦 < +∞ ↔ if(0 ≤ 𝑦, 𝑦, 0) < +∞)) |
34 | | breq1 4656 |
. . . . . . . . . . . . . . 15
⊢ (0 = if(0
≤ 𝑦, 𝑦, 0) → (0 < +∞ ↔ if(0 ≤
𝑦, 𝑦, 0) < +∞)) |
35 | 33, 34 | ifboth 4124 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 < +∞ ∧ 0 <
+∞) → if(0 ≤ 𝑦, 𝑦, 0) < +∞) |
36 | 31, 32, 35 | sylancl 694 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) < +∞) |
37 | | xrre2 12001 |
. . . . . . . . . . . . 13
⊢
(((-∞ ∈ ℝ* ∧ if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ* ∧
+∞ ∈ ℝ*) ∧ (-∞ < if(0 ≤ 𝑦, 𝑦, 0) ∧ if(0 ≤ 𝑦, 𝑦, 0) < +∞)) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
38 | 14, 18, 20, 24, 36, 37 | syl32anc 1334 |
. . . . . . . . . . . 12
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ) |
39 | | xrmax2 12007 |
. . . . . . . . . . . . . . 15
⊢ ((0
∈ ℝ* ∧ 𝑦 ∈ ℝ*) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
40 | 16, 15, 39 | sylancr 695 |
. . . . . . . . . . . . . 14
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0)) |
41 | | df-ioc 12180 |
. . . . . . . . . . . . . . 15
⊢ (,] =
(𝑎 ∈
ℝ*, 𝑏
∈ ℝ* ↦ {𝑐 ∈ ℝ* ∣ (𝑎 < 𝑐 ∧ 𝑐 ≤ 𝑏)}) |
42 | | xrlelttr 11987 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℝ*
∧ if(0 ≤ 𝑦, 𝑦, 0) ∈ ℝ*
∧ 𝑥 ∈
ℝ*) → ((𝑦 ≤ if(0 ≤ 𝑦, 𝑦, 0) ∧ if(0 ≤ 𝑦, 𝑦, 0) < 𝑥) → 𝑦 < 𝑥)) |
43 | 41, 41, 42 | ixxss1 12193 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℝ*
∧ 𝑦 ≤ if(0 ≤
𝑦, 𝑦, 0)) → (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ (𝑦(,]+∞)) |
44 | 15, 40, 43 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ (𝑦(,]+∞)) |
45 | | simplr 792 |
. . . . . . . . . . . . . 14
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → 𝑢 ⊆ 𝐴) |
46 | 26, 45 | eqsstr3d 3640 |
. . . . . . . . . . . . 13
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → (𝑦(,]+∞) ⊆ 𝐴) |
47 | 44, 46 | sstrd 3613 |
. . . . . . . . . . . 12
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴) |
48 | | oveq1 6657 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = if(0 ≤ 𝑦, 𝑦, 0) → (𝑥(,]+∞) = (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞)) |
49 | 48 | sseq1d 3632 |
. . . . . . . . . . . . 13
⊢ (𝑥 = if(0 ≤ 𝑦, 𝑦, 0) → ((𝑥(,]+∞) ⊆ 𝐴 ↔ (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴)) |
50 | 49 | rspcev 3309 |
. . . . . . . . . . . 12
⊢ ((if(0
≤ 𝑦, 𝑦, 0) ∈ ℝ ∧ (if(0 ≤ 𝑦, 𝑦, 0)(,]+∞) ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) |
51 | 38, 47, 50 | syl2anc 693 |
. . . . . . . . . . 11
⊢
(((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) ∧ (𝑦 ∈ ℝ* ∧ 𝑢 = (𝑦(,]+∞))) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) |
52 | 51 | rexlimdvaa 3032 |
. . . . . . . . . 10
⊢
((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → (∃𝑦 ∈ ℝ*
𝑢 = (𝑦(,]+∞) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
53 | 52 | com12 32 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(𝑦(,]+∞) →
((+∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
54 | 12, 53 | sylbi 207 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) → ((+∞
∈ 𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
55 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)) =
(𝑦 ∈
ℝ* ↦ (-∞[,)𝑦)) |
56 | 55 | elrnmpt 5372 |
. . . . . . . . . 10
⊢ (𝑢 ∈ V → (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦))) |
57 | 9, 56 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) ↔
∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦)) |
58 | | pnfnlt 11962 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ ¬ +∞ < 𝑦) |
59 | | elico1 12218 |
. . . . . . . . . . . . . . . 16
⊢
((-∞ ∈ ℝ* ∧ 𝑦 ∈ ℝ*) → (+∞
∈ (-∞[,)𝑦)
↔ (+∞ ∈ ℝ* ∧ -∞ ≤ +∞ ∧
+∞ < 𝑦))) |
60 | 13, 59 | mpan 706 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℝ*
→ (+∞ ∈ (-∞[,)𝑦) ↔ (+∞ ∈ ℝ*
∧ -∞ ≤ +∞ ∧ +∞ < 𝑦))) |
61 | | simp3 1063 |
. . . . . . . . . . . . . . 15
⊢
((+∞ ∈ ℝ* ∧ -∞ ≤ +∞ ∧
+∞ < 𝑦) →
+∞ < 𝑦) |
62 | 60, 61 | syl6bi 243 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℝ*
→ (+∞ ∈ (-∞[,)𝑦) → +∞ < 𝑦)) |
63 | 58, 62 | mtod 189 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℝ*
→ ¬ +∞ ∈ (-∞[,)𝑦)) |
64 | | eleq2 2690 |
. . . . . . . . . . . . . 14
⊢ (𝑢 = (-∞[,)𝑦) → (+∞ ∈ 𝑢 ↔ +∞ ∈
(-∞[,)𝑦))) |
65 | 64 | notbid 308 |
. . . . . . . . . . . . 13
⊢ (𝑢 = (-∞[,)𝑦) → (¬ +∞ ∈
𝑢 ↔ ¬ +∞
∈ (-∞[,)𝑦))) |
66 | 63, 65 | syl5ibrcom 237 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℝ*
→ (𝑢 =
(-∞[,)𝑦) → ¬
+∞ ∈ 𝑢)) |
67 | 66 | rexlimiv 3027 |
. . . . . . . . . . 11
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦) → ¬
+∞ ∈ 𝑢) |
68 | 67 | pm2.21d 118 |
. . . . . . . . . 10
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦) →
(+∞ ∈ 𝑢 →
∃𝑥 ∈ ℝ
(𝑥(,]+∞) ⊆
𝐴)) |
69 | 68 | adantrd 484 |
. . . . . . . . 9
⊢
(∃𝑦 ∈
ℝ* 𝑢 =
(-∞[,)𝑦) →
((+∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
70 | 57, 69 | sylbi 207 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦)) →
((+∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
71 | 54, 70 | jaoi 394 |
. . . . . . 7
⊢ ((𝑢 ∈ ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∨ 𝑢 ∈ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) →
((+∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
72 | 8, 71 | sylbi 207 |
. . . . . 6
⊢ (𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
→ ((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
73 | | pnfnre 10081 |
. . . . . . . . . 10
⊢ +∞
∉ ℝ |
74 | 73 | neli 2899 |
. . . . . . . . 9
⊢ ¬
+∞ ∈ ℝ |
75 | | elssuni 4467 |
. . . . . . . . . . 11
⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆ ∪ ran (,)) |
76 | | unirnioo 12273 |
. . . . . . . . . . 11
⊢ ℝ =
∪ ran (,) |
77 | 75, 76 | syl6sseqr 3652 |
. . . . . . . . . 10
⊢ (𝑢 ∈ ran (,) → 𝑢 ⊆
ℝ) |
78 | 77 | sseld 3602 |
. . . . . . . . 9
⊢ (𝑢 ∈ ran (,) → (+∞
∈ 𝑢 → +∞
∈ ℝ)) |
79 | 74, 78 | mtoi 190 |
. . . . . . . 8
⊢ (𝑢 ∈ ran (,) → ¬
+∞ ∈ 𝑢) |
80 | 79 | pm2.21d 118 |
. . . . . . 7
⊢ (𝑢 ∈ ran (,) → (+∞
∈ 𝑢 →
∃𝑥 ∈ ℝ
(𝑥(,]+∞) ⊆
𝐴)) |
81 | 80 | adantrd 484 |
. . . . . 6
⊢ (𝑢 ∈ ran (,) →
((+∞ ∈ 𝑢 ∧
𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
82 | 72, 81 | jaoi 394 |
. . . . 5
⊢ ((𝑢 ∈ (ran (𝑦 ∈ ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ*
↦ (-∞[,)𝑦)))
∨ 𝑢 ∈ ran (,))
→ ((+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
83 | 7, 82 | sylbi 207 |
. . . 4
⊢ (𝑢 ∈ ((ran (𝑦 ∈ ℝ*
↦ (𝑦(,]+∞))
∪ ran (𝑦 ∈
ℝ* ↦ (-∞[,)𝑦))) ∪ ran (,)) → ((+∞ ∈
𝑢 ∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴)) |
84 | 83 | rexlimiv 3027 |
. . 3
⊢
(∃𝑢 ∈
((ran (𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))(+∞ ∈ 𝑢
∧ 𝑢 ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) |
85 | 6, 84 | syl 17 |
. 2
⊢ ((𝐴 ∈ (topGen‘((ran
(𝑦 ∈
ℝ* ↦ (𝑦(,]+∞)) ∪ ran (𝑦 ∈ ℝ* ↦
(-∞[,)𝑦))) ∪ ran
(,))) ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) |
86 | 5, 85 | sylanb 489 |
1
⊢ ((𝐴 ∈ (ordTop‘ ≤ )
∧ +∞ ∈ 𝐴)
→ ∃𝑥 ∈
ℝ (𝑥(,]+∞)
⊆ 𝐴) |