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 ⊢ 𝐽 = ( TopOpen ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
Assertion pnfneige0 ( ( 𝐴 ∈ 𝐽 ∧ +∞ ∈ 𝐴 ) → ∃ 𝑥 ∈ ℝ ( 𝑥 (,] +∞ ) ⊆ 𝐴 )

Proof

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