Step | Hyp | Ref
| Expression |
1 | | 0red 10643 |
. . . 4
⊢
(((((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) ∧ 𝑦 ∈ ℝ) ∧ (𝑦(,]+∞) ⊆ (𝐴 ∩ (0(,]+∞))) ∧ 𝑦 < 0) → 0 ∈
ℝ) |
2 | | simpllr 774 |
. . . 4
⊢
(((((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) ∧ 𝑦 ∈ ℝ) ∧ (𝑦(,]+∞) ⊆ (𝐴 ∩ (0(,]+∞))) ∧ ¬ 𝑦 < 0) → 𝑦 ∈
ℝ) |
3 | 1, 2 | ifclda 4500 |
. . 3
⊢ ((((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) ∧ 𝑦 ∈ ℝ) ∧ (𝑦(,]+∞) ⊆ (𝐴 ∩ (0(,]+∞))) → if(𝑦 < 0, 0, 𝑦) ∈ ℝ) |
4 | | rexr 10686 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → 𝑦 ∈
ℝ*) |
5 | | 0xr 10687 |
. . . . . . . 8
⊢ 0 ∈
ℝ* |
6 | 5 | a1i 11 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → 0 ∈
ℝ*) |
7 | | pnfxr 10694 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
8 | 7 | a1i 11 |
. . . . . . 7
⊢ (𝑦 ∈ ℝ → +∞
∈ ℝ*) |
9 | | iocinif 30503 |
. . . . . . 7
⊢ ((𝑦 ∈ ℝ*
∧ 0 ∈ ℝ* ∧ +∞ ∈ ℝ*)
→ ((𝑦(,]+∞)
∩ (0(,]+∞)) = if(𝑦 < 0, (0(,]+∞), (𝑦(,]+∞))) |
10 | 4, 6, 8, 9 | syl3anc 1367 |
. . . . . 6
⊢ (𝑦 ∈ ℝ → ((𝑦(,]+∞) ∩
(0(,]+∞)) = if(𝑦 <
0, (0(,]+∞), (𝑦(,]+∞))) |
11 | | ovif 7250 |
. . . . . 6
⊢ (if(𝑦 < 0, 0, 𝑦)(,]+∞) = if(𝑦 < 0, (0(,]+∞), (𝑦(,]+∞)) |
12 | 10, 11 | syl6reqr 2875 |
. . . . 5
⊢ (𝑦 ∈ ℝ → (if(𝑦 < 0, 0, 𝑦)(,]+∞) = ((𝑦(,]+∞) ∩
(0(,]+∞))) |
13 | 12 | ad2antlr 725 |
. . . 4
⊢ ((((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) ∧ 𝑦 ∈ ℝ) ∧ (𝑦(,]+∞) ⊆ (𝐴 ∩ (0(,]+∞))) → (if(𝑦 < 0, 0, 𝑦)(,]+∞) = ((𝑦(,]+∞) ∩
(0(,]+∞))) |
14 | | iocssicc 12824 |
. . . . . 6
⊢
(0(,]+∞) ⊆ (0[,]+∞) |
15 | | sslin 4210 |
. . . . . 6
⊢
((0(,]+∞) ⊆ (0[,]+∞) → ((𝑦(,]+∞) ∩ (0(,]+∞)) ⊆
((𝑦(,]+∞) ∩
(0[,]+∞))) |
16 | 14, 15 | mp1i 13 |
. . . . 5
⊢ ((((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) ∧ 𝑦 ∈ ℝ) ∧ (𝑦(,]+∞) ⊆ (𝐴 ∩ (0(,]+∞))) → ((𝑦(,]+∞) ∩
(0(,]+∞)) ⊆ ((𝑦(,]+∞) ∩
(0[,]+∞))) |
17 | | simpr 487 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) ∧ 𝑦 ∈ ℝ) ∧ (𝑦(,]+∞) ⊆ (𝐴 ∩ (0(,]+∞))) → (𝑦(,]+∞) ⊆ (𝐴 ∩
(0(,]+∞))) |
18 | | ssin 4206 |
. . . . . . . 8
⊢ (((𝑦(,]+∞) ⊆ 𝐴 ∧ (𝑦(,]+∞) ⊆ (0(,]+∞)) ↔
(𝑦(,]+∞) ⊆
(𝐴 ∩
(0(,]+∞))) |
19 | 18 | biimpri 230 |
. . . . . . 7
⊢ ((𝑦(,]+∞) ⊆ (𝐴 ∩ (0(,]+∞)) →
((𝑦(,]+∞) ⊆
𝐴 ∧ (𝑦(,]+∞) ⊆
(0(,]+∞))) |
20 | 19 | simpld 497 |
. . . . . 6
⊢ ((𝑦(,]+∞) ⊆ (𝐴 ∩ (0(,]+∞)) →
(𝑦(,]+∞) ⊆
𝐴) |
21 | | ssinss1 4213 |
. . . . . 6
⊢ ((𝑦(,]+∞) ⊆ 𝐴 → ((𝑦(,]+∞) ∩ (0[,]+∞)) ⊆
𝐴) |
22 | 17, 20, 21 | 3syl 18 |
. . . . 5
⊢ ((((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) ∧ 𝑦 ∈ ℝ) ∧ (𝑦(,]+∞) ⊆ (𝐴 ∩ (0(,]+∞))) → ((𝑦(,]+∞) ∩
(0[,]+∞)) ⊆ 𝐴) |
23 | 16, 22 | sstrd 3976 |
. . . 4
⊢ ((((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) ∧ 𝑦 ∈ ℝ) ∧ (𝑦(,]+∞) ⊆ (𝐴 ∩ (0(,]+∞))) → ((𝑦(,]+∞) ∩
(0(,]+∞)) ⊆ 𝐴) |
24 | 13, 23 | eqsstrd 4004 |
. . 3
⊢ ((((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) ∧ 𝑦 ∈ ℝ) ∧ (𝑦(,]+∞) ⊆ (𝐴 ∩ (0(,]+∞))) → (if(𝑦 < 0, 0, 𝑦)(,]+∞) ⊆ 𝐴) |
25 | | oveq1 7162 |
. . . . 5
⊢ (𝑥 = if(𝑦 < 0, 0, 𝑦) → (𝑥(,]+∞) = (if(𝑦 < 0, 0, 𝑦)(,]+∞)) |
26 | 25 | sseq1d 3997 |
. . . 4
⊢ (𝑥 = if(𝑦 < 0, 0, 𝑦) → ((𝑥(,]+∞) ⊆ 𝐴 ↔ (if(𝑦 < 0, 0, 𝑦)(,]+∞) ⊆ 𝐴)) |
27 | 26 | rspcev 3622 |
. . 3
⊢
((if(𝑦 < 0, 0,
𝑦) ∈ ℝ ∧
(if(𝑦 < 0, 0, 𝑦)(,]+∞) ⊆ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) |
28 | 3, 24, 27 | syl2anc 586 |
. 2
⊢ ((((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) ∧ 𝑦 ∈ ℝ) ∧ (𝑦(,]+∞) ⊆ (𝐴 ∩ (0(,]+∞))) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) |
29 | | letopon 21812 |
. . . . . . . . . 10
⊢
(ordTop‘ ≤ ) ∈
(TopOn‘ℝ*) |
30 | | iccssxr 12818 |
. . . . . . . . . 10
⊢
(0[,]+∞) ⊆ ℝ* |
31 | | resttopon 21768 |
. . . . . . . . . 10
⊢
(((ordTop‘ ≤ ) ∈ (TopOn‘ℝ*) ∧
(0[,]+∞) ⊆ ℝ*) → ((ordTop‘ ≤ )
↾t (0[,]+∞)) ∈
(TopOn‘(0[,]+∞))) |
32 | 29, 30, 31 | mp2an 690 |
. . . . . . . . 9
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈
(TopOn‘(0[,]+∞)) |
33 | 32 | topontopi 21522 |
. . . . . . . 8
⊢
((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈
Top |
34 | 33 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐽 → ((ordTop‘ ≤ )
↾t (0[,]+∞)) ∈ Top) |
35 | | ovex 7188 |
. . . . . . . 8
⊢
(0(,]+∞) ∈ V |
36 | 35 | a1i 11 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐽 → (0(,]+∞) ∈
V) |
37 | | pnfneige0.j |
. . . . . . . . . 10
⊢ 𝐽 =
(TopOpen‘(ℝ*𝑠 ↾s
(0[,]+∞))) |
38 | | xrge0topn 31186 |
. . . . . . . . . 10
⊢
(TopOpen‘(ℝ*𝑠
↾s (0[,]+∞))) = ((ordTop‘ ≤ )
↾t (0[,]+∞)) |
39 | 37, 38 | eqtri 2844 |
. . . . . . . . 9
⊢ 𝐽 = ((ordTop‘ ≤ )
↾t (0[,]+∞)) |
40 | 39 | eleq2i 2904 |
. . . . . . . 8
⊢ (𝐴 ∈ 𝐽 ↔ 𝐴 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞))) |
41 | 40 | biimpi 218 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐽 → 𝐴 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞))) |
42 | | elrestr 16701 |
. . . . . . 7
⊢
((((ordTop‘ ≤ ) ↾t (0[,]+∞)) ∈ Top
∧ (0(,]+∞) ∈ V ∧ 𝐴 ∈ ((ordTop‘ ≤ )
↾t (0[,]+∞))) → (𝐴 ∩ (0(,]+∞)) ∈
(((ordTop‘ ≤ ) ↾t (0[,]+∞)) ↾t
(0(,]+∞))) |
43 | 34, 36, 41, 42 | syl3anc 1367 |
. . . . . 6
⊢ (𝐴 ∈ 𝐽 → (𝐴 ∩ (0(,]+∞)) ∈
(((ordTop‘ ≤ ) ↾t (0[,]+∞)) ↾t
(0(,]+∞))) |
44 | | letop 21813 |
. . . . . . 7
⊢
(ordTop‘ ≤ ) ∈ Top |
45 | | ovex 7188 |
. . . . . . 7
⊢
(0[,]+∞) ∈ V |
46 | | restabs 21772 |
. . . . . . 7
⊢
(((ordTop‘ ≤ ) ∈ Top ∧ (0(,]+∞) ⊆
(0[,]+∞) ∧ (0[,]+∞) ∈ V) → (((ordTop‘ ≤ )
↾t (0[,]+∞)) ↾t (0(,]+∞)) =
((ordTop‘ ≤ ) ↾t (0(,]+∞))) |
47 | 44, 14, 45, 46 | mp3an 1457 |
. . . . . 6
⊢
(((ordTop‘ ≤ ) ↾t (0[,]+∞))
↾t (0(,]+∞)) = ((ordTop‘ ≤ )
↾t (0(,]+∞)) |
48 | 43, 47 | eleqtrdi 2923 |
. . . . 5
⊢ (𝐴 ∈ 𝐽 → (𝐴 ∩ (0(,]+∞)) ∈
((ordTop‘ ≤ ) ↾t (0(,]+∞))) |
49 | 44 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ 𝐽 → (ordTop‘ ≤ ) ∈
Top) |
50 | | iocpnfordt 21822 |
. . . . . . 7
⊢
(0(,]+∞) ∈ (ordTop‘ ≤ ) |
51 | 50 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ 𝐽 → (0(,]+∞) ∈ (ordTop‘
≤ )) |
52 | | ssidd 3989 |
. . . . . 6
⊢ (𝐴 ∈ 𝐽 → (0(,]+∞) ⊆
(0(,]+∞)) |
53 | | inss2 4205 |
. . . . . . 7
⊢ (𝐴 ∩ (0(,]+∞)) ⊆
(0(,]+∞) |
54 | 53 | a1i 11 |
. . . . . 6
⊢ (𝐴 ∈ 𝐽 → (𝐴 ∩ (0(,]+∞)) ⊆
(0(,]+∞)) |
55 | | restopnb 21782 |
. . . . . 6
⊢
((((ordTop‘ ≤ ) ∈ Top ∧ (0(,]+∞) ∈ V) ∧
((0(,]+∞) ∈ (ordTop‘ ≤ ) ∧ (0(,]+∞) ⊆
(0(,]+∞) ∧ (𝐴
∩ (0(,]+∞)) ⊆ (0(,]+∞))) → ((𝐴 ∩ (0(,]+∞)) ∈ (ordTop‘
≤ ) ↔ (𝐴 ∩
(0(,]+∞)) ∈ ((ordTop‘ ≤ ) ↾t
(0(,]+∞)))) |
56 | 49, 36, 51, 52, 54, 55 | syl23anc 1373 |
. . . . 5
⊢ (𝐴 ∈ 𝐽 → ((𝐴 ∩ (0(,]+∞)) ∈ (ordTop‘
≤ ) ↔ (𝐴 ∩
(0(,]+∞)) ∈ ((ordTop‘ ≤ ) ↾t
(0(,]+∞)))) |
57 | 48, 56 | mpbird 259 |
. . . 4
⊢ (𝐴 ∈ 𝐽 → (𝐴 ∩ (0(,]+∞)) ∈ (ordTop‘
≤ )) |
58 | 57 | adantr 483 |
. . 3
⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → (𝐴 ∩ (0(,]+∞)) ∈ (ordTop‘
≤ )) |
59 | | simpr 487 |
. . . 4
⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → +∞ ∈ 𝐴) |
60 | | 0ltpnf 12516 |
. . . . . 6
⊢ 0 <
+∞ |
61 | | ubioc1 12789 |
. . . . . 6
⊢ ((0
∈ ℝ* ∧ +∞ ∈ ℝ* ∧ 0
< +∞) → +∞ ∈ (0(,]+∞)) |
62 | 5, 7, 60, 61 | mp3an 1457 |
. . . . 5
⊢ +∞
∈ (0(,]+∞) |
63 | 62 | a1i 11 |
. . . 4
⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → +∞ ∈
(0(,]+∞)) |
64 | 59, 63 | elind 4170 |
. . 3
⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → +∞ ∈ (𝐴 ∩ (0(,]+∞))) |
65 | | pnfnei 21827 |
. . 3
⊢ (((𝐴 ∩ (0(,]+∞)) ∈
(ordTop‘ ≤ ) ∧ +∞ ∈ (𝐴 ∩ (0(,]+∞))) → ∃𝑦 ∈ ℝ (𝑦(,]+∞) ⊆ (𝐴 ∩
(0(,]+∞))) |
66 | 58, 64, 65 | syl2anc 586 |
. 2
⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → ∃𝑦 ∈ ℝ (𝑦(,]+∞) ⊆ (𝐴 ∩ (0(,]+∞))) |
67 | 28, 66 | r19.29a 3289 |
1
⊢ ((𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴) → ∃𝑥 ∈ ℝ (𝑥(,]+∞) ⊆ 𝐴) |