Metamath Proof Explorer


Theorem pnfneige0

Description: A neighborhood of +oo contains an unbounded interval based at a real number. See pnfnei . (Contributed by Thierry Arnoux, 31-Jul-2017)

Ref Expression
Hypothesis pnfneige0.j J = TopOpen 𝑠 * 𝑠 0 +∞
Assertion pnfneige0 A J +∞ A x x +∞ A

Proof

Step Hyp Ref Expression
1 pnfneige0.j J = TopOpen 𝑠 * 𝑠 0 +∞
2 0red A J +∞ A y y +∞ A 0 +∞ y < 0 0
3 simpllr A J +∞ A y y +∞ A 0 +∞ ¬ y < 0 y
4 2 3 ifclda A J +∞ A y y +∞ A 0 +∞ if y < 0 0 y
5 rexr y y *
6 0xr 0 *
7 6 a1i y 0 *
8 pnfxr +∞ *
9 8 a1i y +∞ *
10 iocinif y * 0 * +∞ * y +∞ 0 +∞ = if y < 0 0 +∞ y +∞
11 5 7 9 10 syl3anc y y +∞ 0 +∞ = if y < 0 0 +∞ y +∞
12 ovif if y < 0 0 y +∞ = if y < 0 0 +∞ y +∞
13 11 12 syl6reqr y if y < 0 0 y +∞ = y +∞ 0 +∞
14 13 ad2antlr A J +∞ A y y +∞ A 0 +∞ if y < 0 0 y +∞ = y +∞ 0 +∞
15 iocssicc 0 +∞ 0 +∞
16 sslin 0 +∞ 0 +∞ y +∞ 0 +∞ y +∞ 0 +∞
17 15 16 mp1i A J +∞ A y y +∞ A 0 +∞ y +∞ 0 +∞ y +∞ 0 +∞
18 simpr A J +∞ A y y +∞ A 0 +∞ y +∞ A 0 +∞
19 ssin y +∞ A y +∞ 0 +∞ y +∞ A 0 +∞
20 19 biimpri y +∞ A 0 +∞ y +∞ A y +∞ 0 +∞
21 20 simpld y +∞ A 0 +∞ y +∞ A
22 ssinss1 y +∞ A y +∞ 0 +∞ A
23 18 21 22 3syl A J +∞ A y y +∞ A 0 +∞ y +∞ 0 +∞ A
24 17 23 sstrd A J +∞ A y y +∞ A 0 +∞ y +∞ 0 +∞ A
25 14 24 eqsstrd A J +∞ A y y +∞ A 0 +∞ if y < 0 0 y +∞ A
26 oveq1 x = if y < 0 0 y x +∞ = if y < 0 0 y +∞
27 26 sseq1d x = if y < 0 0 y x +∞ A if y < 0 0 y +∞ A
28 27 rspcev if y < 0 0 y if y < 0 0 y +∞ A x x +∞ A
29 4 25 28 syl2anc A J +∞ A y y +∞ A 0 +∞ x x +∞ A
30 letopon ordTop TopOn *
31 iccssxr 0 +∞ *
32 resttopon ordTop TopOn * 0 +∞ * ordTop 𝑡 0 +∞ TopOn 0 +∞
33 30 31 32 mp2an ordTop 𝑡 0 +∞ TopOn 0 +∞
34 33 topontopi ordTop 𝑡 0 +∞ Top
35 34 a1i A J ordTop 𝑡 0 +∞ Top
36 ovex 0 +∞ V
37 36 a1i A J 0 +∞ V
38 xrge0topn TopOpen 𝑠 * 𝑠 0 +∞ = ordTop 𝑡 0 +∞
39 1 38 eqtri J = ordTop 𝑡 0 +∞
40 39 eleq2i A J A ordTop 𝑡 0 +∞
41 40 biimpi A J A ordTop 𝑡 0 +∞
42 elrestr ordTop 𝑡 0 +∞ Top 0 +∞ V A ordTop 𝑡 0 +∞ A 0 +∞ ordTop 𝑡 0 +∞ 𝑡 0 +∞
43 35 37 41 42 syl3anc A J A 0 +∞ ordTop 𝑡 0 +∞ 𝑡 0 +∞
44 letop ordTop Top
45 ovex 0 +∞ V
46 restabs ordTop Top 0 +∞ 0 +∞ 0 +∞ V ordTop 𝑡 0 +∞ 𝑡 0 +∞ = ordTop 𝑡 0 +∞
47 44 15 45 46 mp3an ordTop 𝑡 0 +∞ 𝑡 0 +∞ = ordTop 𝑡 0 +∞
48 43 47 eleqtrdi A J A 0 +∞ ordTop 𝑡 0 +∞
49 44 a1i A J ordTop Top
50 iocpnfordt 0 +∞ ordTop
51 50 a1i A J 0 +∞ ordTop
52 ssidd A J 0 +∞ 0 +∞
53 inss2 A 0 +∞ 0 +∞
54 53 a1i A J A 0 +∞ 0 +∞
55 restopnb ordTop Top 0 +∞ V 0 +∞ ordTop 0 +∞ 0 +∞ A 0 +∞ 0 +∞ A 0 +∞ ordTop A 0 +∞ ordTop 𝑡 0 +∞
56 49 37 51 52 54 55 syl23anc A J A 0 +∞ ordTop A 0 +∞ ordTop 𝑡 0 +∞
57 48 56 mpbird A J A 0 +∞ ordTop
58 57 adantr A J +∞ A A 0 +∞ ordTop
59 simpr A J +∞ A +∞ A
60 0ltpnf 0 < +∞
61 ubioc1 0 * +∞ * 0 < +∞ +∞ 0 +∞
62 6 8 60 61 mp3an +∞ 0 +∞
63 62 a1i A J +∞ A +∞ 0 +∞
64 59 63 elind A J +∞ A +∞ A 0 +∞
65 pnfnei A 0 +∞ ordTop +∞ A 0 +∞ y y +∞ A 0 +∞
66 58 64 65 syl2anc A J +∞ A y y +∞ A 0 +∞
67 29 66 r19.29a A J +∞ A x x +∞ A