Metamath Proof Explorer

Theorem pnfnei

Description: A neighborhood of +oo contains an unbounded interval based at a real number. Together with xrtgioo (which describes neighborhoods of RR ) and mnfnei , this gives all "negative" topological information ensuring that it is not too fine (and of course iooordt and similar ensure that it has all the sets we want). (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion pnfnei ⊢ A ∈ ordTop ⁡ ≤ ∧ +∞ ∈ A → ∃ x ∈ ℝ x +∞ ⊆ A

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran ⁡ y ∈ ℝ * ⟼ y +∞ = ran ⁡ y ∈ ℝ * ⟼ y +∞
2 eqid ⊢ ran ⁡ y ∈ ℝ * ⟼ −∞ y = ran ⁡ y ∈ ℝ * ⟼ −∞ y
3 eqid ⊢ ran ⁡ . = ran ⁡ .
4 1 2 3 leordtval ⊢ ordTop ⁡ ≤ = topGen ⁡ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∪ ran ⁡ y ∈ ℝ * ⟼ −∞ y ∪ ran ⁡ .
5 4 eleq2i ⊢ A ∈ ordTop ⁡ ≤ ↔ A ∈ topGen ⁡ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∪ ran ⁡ y ∈ ℝ * ⟼ −∞ y ∪ ran ⁡ .
6 tg2 ⊢ A ∈ topGen ⁡ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∪ ran ⁡ y ∈ ℝ * ⟼ −∞ y ∪ ran ⁡ . ∧ +∞ ∈ A → ∃ u ∈ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∪ ran ⁡ y ∈ ℝ * ⟼ −∞ y ∪ ran ⁡ . +∞ ∈ u ∧ u ⊆ A
7 elun ⊢ u ∈ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∪ ran ⁡ y ∈ ℝ * ⟼ −∞ y ∪ ran ⁡ . ↔ u ∈ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∪ ran ⁡ y ∈ ℝ * ⟼ −∞ y ∨ u ∈ ran ⁡ .
8 elun ⊢ u ∈ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∪ ran ⁡ y ∈ ℝ * ⟼ −∞ y ↔ u ∈ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∨ u ∈ ran ⁡ y ∈ ℝ * ⟼ −∞ y
9 eqid ⊢ y ∈ ℝ * ⟼ y +∞ = y ∈ ℝ * ⟼ y +∞
10 9 elrnmpt ⊢ u ∈ V → u ∈ ran ⁡ y ∈ ℝ * ⟼ y +∞ ↔ ∃ y ∈ ℝ * u = y +∞
11 10 elv ⊢ u ∈ ran ⁡ y ∈ ℝ * ⟼ y +∞ ↔ ∃ y ∈ ℝ * u = y +∞
12 mnfxr ⊢ −∞ ∈ ℝ *
13 12 a1i ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → −∞ ∈ ℝ *
14 simprl ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → y ∈ ℝ *
15 0xr ⊢ 0 ∈ ℝ *
16 ifcl ⊢ y ∈ ℝ * ∧ 0 ∈ ℝ * → if 0 ≤ y y 0 ∈ ℝ *
17 14 15 16 sylancl ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → if 0 ≤ y y 0 ∈ ℝ *
18 pnfxr ⊢ +∞ ∈ ℝ *
19 18 a1i ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → +∞ ∈ ℝ *
20 xrmax1 ⊢ 0 ∈ ℝ * ∧ y ∈ ℝ * → 0 ≤ if 0 ≤ y y 0
21 15 14 20 sylancr ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → 0 ≤ if 0 ≤ y y 0
22 ge0gtmnf ⊢ if 0 ≤ y y 0 ∈ ℝ * ∧ 0 ≤ if 0 ≤ y y 0 → −∞ < if 0 ≤ y y 0
23 17 21 22 syl2anc ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → −∞ < if 0 ≤ y y 0
24 simpll ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → +∞ ∈ u
25 simprr ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → u = y +∞
26 24 25 eleqtrd ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → +∞ ∈ y +∞
27 elioc1 ⊢ y ∈ ℝ * ∧ +∞ ∈ ℝ * → +∞ ∈ y +∞ ↔ +∞ ∈ ℝ * ∧ y < +∞ ∧ +∞ ≤ +∞
28 14 18 27 sylancl ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → +∞ ∈ y +∞ ↔ +∞ ∈ ℝ * ∧ y < +∞ ∧ +∞ ≤ +∞
29 26 28 mpbid ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → +∞ ∈ ℝ * ∧ y < +∞ ∧ +∞ ≤ +∞
30 29 simp2d ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → y < +∞
31 0ltpnf ⊢ 0 < +∞
32 breq1 ⊢ y = if 0 ≤ y y 0 → y < +∞ ↔ if 0 ≤ y y 0 < +∞
33 breq1 ⊢ 0 = if 0 ≤ y y 0 → 0 < +∞ ↔ if 0 ≤ y y 0 < +∞
34 32 33 ifboth ⊢ y < +∞ ∧ 0 < +∞ → if 0 ≤ y y 0 < +∞
35 30 31 34 sylancl ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → if 0 ≤ y y 0 < +∞
36 xrre2 ⊢ −∞ ∈ ℝ * ∧ if 0 ≤ y y 0 ∈ ℝ * ∧ +∞ ∈ ℝ * ∧ −∞ < if 0 ≤ y y 0 ∧ if 0 ≤ y y 0 < +∞ → if 0 ≤ y y 0 ∈ ℝ
37 13 17 19 23 35 36 syl32anc ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → if 0 ≤ y y 0 ∈ ℝ
38 xrmax2 ⊢ 0 ∈ ℝ * ∧ y ∈ ℝ * → y ≤ if 0 ≤ y y 0
39 15 14 38 sylancr ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → y ≤ if 0 ≤ y y 0
40 df-ioc ⊢ . = a ∈ ℝ * , b ∈ ℝ * ⟼ c ∈ ℝ * | a < c ∧ c ≤ b
41 xrlelttr ⊢ y ∈ ℝ * ∧ if 0 ≤ y y 0 ∈ ℝ * ∧ x ∈ ℝ * → y ≤ if 0 ≤ y y 0 ∧ if 0 ≤ y y 0 < x → y < x
42 40 40 41 ixxss1 ⊢ y ∈ ℝ * ∧ y ≤ if 0 ≤ y y 0 → if 0 ≤ y y 0 +∞ ⊆ y +∞
43 14 39 42 syl2anc ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → if 0 ≤ y y 0 +∞ ⊆ y +∞
44 simplr ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → u ⊆ A
45 25 44 eqsstrrd ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → y +∞ ⊆ A
46 43 45 sstrd ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → if 0 ≤ y y 0 +∞ ⊆ A
47 oveq1 ⊢ x = if 0 ≤ y y 0 → x +∞ = if 0 ≤ y y 0 +∞
48 47 sseq1d ⊢ x = if 0 ≤ y y 0 → x +∞ ⊆ A ↔ if 0 ≤ y y 0 +∞ ⊆ A
49 48 rspcev ⊢ if 0 ≤ y y 0 ∈ ℝ ∧ if 0 ≤ y y 0 +∞ ⊆ A → ∃ x ∈ ℝ x +∞ ⊆ A
50 37 46 49 syl2anc ⊢ +∞ ∈ u ∧ u ⊆ A ∧ y ∈ ℝ * ∧ u = y +∞ → ∃ x ∈ ℝ x +∞ ⊆ A
51 50 rexlimdvaa ⊢ +∞ ∈ u ∧ u ⊆ A → ∃ y ∈ ℝ * u = y +∞ → ∃ x ∈ ℝ x +∞ ⊆ A
52 51 com12 ⊢ ∃ y ∈ ℝ * u = y +∞ → +∞ ∈ u ∧ u ⊆ A → ∃ x ∈ ℝ x +∞ ⊆ A
53 11 52 sylbi ⊢ u ∈ ran ⁡ y ∈ ℝ * ⟼ y +∞ → +∞ ∈ u ∧ u ⊆ A → ∃ x ∈ ℝ x +∞ ⊆ A
54 eqid ⊢ y ∈ ℝ * ⟼ −∞ y = y ∈ ℝ * ⟼ −∞ y
55 54 elrnmpt ⊢ u ∈ V → u ∈ ran ⁡ y ∈ ℝ * ⟼ −∞ y ↔ ∃ y ∈ ℝ * u = −∞ y
56 55 elv ⊢ u ∈ ran ⁡ y ∈ ℝ * ⟼ −∞ y ↔ ∃ y ∈ ℝ * u = −∞ y
57 pnfnlt ⊢ y ∈ ℝ * → ¬ +∞ < y
58 elico1 ⊢ −∞ ∈ ℝ * ∧ y ∈ ℝ * → +∞ ∈ −∞ y ↔ +∞ ∈ ℝ * ∧ −∞ ≤ +∞ ∧ +∞ < y
59 12 58 mpan ⊢ y ∈ ℝ * → +∞ ∈ −∞ y ↔ +∞ ∈ ℝ * ∧ −∞ ≤ +∞ ∧ +∞ < y
60 simp3 ⊢ +∞ ∈ ℝ * ∧ −∞ ≤ +∞ ∧ +∞ < y → +∞ < y
61 59 60 biimtrdi ⊢ y ∈ ℝ * → +∞ ∈ −∞ y → +∞ < y
62 57 61 mtod ⊢ y ∈ ℝ * → ¬ +∞ ∈ −∞ y
63 eleq2 ⊢ u = −∞ y → +∞ ∈ u ↔ +∞ ∈ −∞ y
64 63 notbid ⊢ u = −∞ y → ¬ +∞ ∈ u ↔ ¬ +∞ ∈ −∞ y
65 62 64 syl5ibrcom ⊢ y ∈ ℝ * → u = −∞ y → ¬ +∞ ∈ u
66 65 rexlimiv ⊢ ∃ y ∈ ℝ * u = −∞ y → ¬ +∞ ∈ u
67 66 pm2.21d ⊢ ∃ y ∈ ℝ * u = −∞ y → +∞ ∈ u → ∃ x ∈ ℝ x +∞ ⊆ A
68 67 adantrd ⊢ ∃ y ∈ ℝ * u = −∞ y → +∞ ∈ u ∧ u ⊆ A → ∃ x ∈ ℝ x +∞ ⊆ A
69 56 68 sylbi ⊢ u ∈ ran ⁡ y ∈ ℝ * ⟼ −∞ y → +∞ ∈ u ∧ u ⊆ A → ∃ x ∈ ℝ x +∞ ⊆ A
70 53 69 jaoi ⊢ u ∈ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∨ u ∈ ran ⁡ y ∈ ℝ * ⟼ −∞ y → +∞ ∈ u ∧ u ⊆ A → ∃ x ∈ ℝ x +∞ ⊆ A
71 8 70 sylbi ⊢ u ∈ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∪ ran ⁡ y ∈ ℝ * ⟼ −∞ y → +∞ ∈ u ∧ u ⊆ A → ∃ x ∈ ℝ x +∞ ⊆ A
72 pnfnre ⊢ +∞ ∉ ℝ
73 72 neli ⊢ ¬ +∞ ∈ ℝ
74 elssuni ⊢ u ∈ ran ⁡ . → u ⊆ ⋃ ran ⁡ .
75 unirnioo ⊢ ℝ = ⋃ ran ⁡ .
76 74 75 sseqtrrdi ⊢ u ∈ ran ⁡ . → u ⊆ ℝ
77 76 sseld ⊢ u ∈ ran ⁡ . → +∞ ∈ u → +∞ ∈ ℝ
78 73 77 mtoi ⊢ u ∈ ran ⁡ . → ¬ +∞ ∈ u
79 78 pm2.21d ⊢ u ∈ ran ⁡ . → +∞ ∈ u → ∃ x ∈ ℝ x +∞ ⊆ A
80 79 adantrd ⊢ u ∈ ran ⁡ . → +∞ ∈ u ∧ u ⊆ A → ∃ x ∈ ℝ x +∞ ⊆ A
81 71 80 jaoi ⊢ u ∈ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∪ ran ⁡ y ∈ ℝ * ⟼ −∞ y ∨ u ∈ ran ⁡ . → +∞ ∈ u ∧ u ⊆ A → ∃ x ∈ ℝ x +∞ ⊆ A
82 7 81 sylbi ⊢ u ∈ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∪ ran ⁡ y ∈ ℝ * ⟼ −∞ y ∪ ran ⁡ . → +∞ ∈ u ∧ u ⊆ A → ∃ x ∈ ℝ x +∞ ⊆ A
83 82 rexlimiv ⊢ ∃ u ∈ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∪ ran ⁡ y ∈ ℝ * ⟼ −∞ y ∪ ran ⁡ . +∞ ∈ u ∧ u ⊆ A → ∃ x ∈ ℝ x +∞ ⊆ A
84 6 83 syl ⊢ A ∈ topGen ⁡ ran ⁡ y ∈ ℝ * ⟼ y +∞ ∪ ran ⁡ y ∈ ℝ * ⟼ −∞ y ∪ ran ⁡ . ∧ +∞ ∈ A → ∃ x ∈ ℝ x +∞ ⊆ A
85 5 84 sylanb ⊢ A ∈ ordTop ⁡ ≤ ∧ +∞ ∈ A → ∃ x ∈ ℝ x +∞ ⊆ A