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+∞→ify<00y∈ℝ
5 ovif ⊢ify<00y+∞=ify<00+∞y+∞
6 rexr ⊢y∈ℝ→y∈ℝ*
7 0xr ⊢0∈ℝ*
8 7 a1i ⊢y∈ℝ→0∈ℝ*
9 pnfxr ⊢+∞∈ℝ*
10 9 a1i ⊢y∈ℝ→+∞∈ℝ*
11 iocinif ⊢y∈ℝ*∧0∈ℝ*∧+∞∈ℝ*→y+∞∩0+∞=ify<00+∞y+∞
12 6 8 10 11 syl3anc ⊢y∈ℝ→y+∞∩0+∞=ify<00+∞y+∞
13 5 12 eqtr4id ⊢y∈ℝ→ify<00y+∞=y+∞∩0+∞
14 13 ad2antlr ⊢A∈J∧+∞∈A∧y∈ℝ∧y+∞⊆A∩0+∞→ify<00y+∞=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+∞→ify<00y+∞⊆A
26 oveq1 ⊢x=ify<00y→x+∞=ify<00y+∞
27 26 sseq1d ⊢x=ify<00y→x+∞⊆A↔ify<00y+∞⊆A
28 27 rspcev ⊢ify<00y∈ℝ∧ify<00y+∞⊆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 7 9 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