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 ovif ⊢ if y < 0 0 y +∞ = if y < 0 0 +∞ 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 +∞ = if y < 0 0 +∞ y +∞
12 6 8 10 11 syl3anc ⊢ y ∈ ℝ → y +∞ ∩ 0 +∞ = if y < 0 0 +∞ y +∞
13 5 12 eqtr4id ⊢ 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 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