# 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}=\mathrm{TopOpen}\left({ℝ}_{𝑠}^{*}{↾}_{𝑠}\left[0,\mathrm{+\infty }\right]\right)$
Assertion pnfneige0 ${⊢}\left({A}\in {J}\wedge \mathrm{+\infty }\in {A}\right)\to \exists {x}\in ℝ\phantom{\rule{.4em}{0ex}}\left({x},\mathrm{+\infty }\right]\subseteq {A}$

### Proof

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