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∈ℝ*→if0≤yy0∈ℝ*
17 14 15 16 sylancl ⊢+∞∈u∧u⊆A∧y∈ℝ*∧u=y+∞→if0≤yy0∈ℝ*
18 pnfxr ⊢+∞∈ℝ*
19 18 a1i ⊢+∞∈u∧u⊆A∧y∈ℝ*∧u=y+∞→+∞∈ℝ*
20 xrmax1 ⊢0∈ℝ*∧y∈ℝ*→0≤if0≤yy0
21 15 14 20 sylancr ⊢+∞∈u∧u⊆A∧y∈ℝ*∧u=y+∞→0≤if0≤yy0
22 ge0gtmnf ⊢if0≤yy0∈ℝ*∧0≤if0≤yy0→−∞<if0≤yy0
23 17 21 22 syl2anc ⊢+∞∈u∧u⊆A∧y∈ℝ*∧u=y+∞→−∞<if0≤yy0
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=if0≤yy0→y<+∞↔if0≤yy0<+∞
33 breq1 ⊢0=if0≤yy0→0<+∞↔if0≤yy0<+∞
34 32 33 ifboth ⊢y<+∞∧0<+∞→if0≤yy0<+∞
35 30 31 34 sylancl ⊢+∞∈u∧u⊆A∧y∈ℝ*∧u=y+∞→if0≤yy0<+∞
36 xrre2 ⊢−∞∈ℝ*∧if0≤yy0∈ℝ*∧+∞∈ℝ*∧−∞<if0≤yy0∧if0≤yy0<+∞→if0≤yy0∈ℝ
37 13 17 19 23 35 36 syl32anc ⊢+∞∈u∧u⊆A∧y∈ℝ*∧u=y+∞→if0≤yy0∈ℝ
38 xrmax2 ⊢0∈ℝ*∧y∈ℝ*→y≤if0≤yy0
39 15 14 38 sylancr ⊢+∞∈u∧u⊆A∧y∈ℝ*∧u=y+∞→y≤if0≤yy0
40 df-ioc ⊢.=a∈ℝ*,b∈ℝ*⟼c∈ℝ*|a<c∧c≤b
41 xrlelttr ⊢y∈ℝ*∧if0≤yy0∈ℝ*∧x∈ℝ*→y≤if0≤yy0∧if0≤yy0<x→y<x
42 40 40 41 ixxss1 ⊢y∈ℝ*∧y≤if0≤yy0→if0≤yy0+∞⊆y+∞
43 14 39 42 syl2anc ⊢+∞∈u∧u⊆A∧y∈ℝ*∧u=y+∞→if0≤yy0+∞⊆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+∞→if0≤yy0+∞⊆A
47 oveq1 ⊢x=if0≤yy0→x+∞=if0≤yy0+∞
48 47 sseq1d ⊢x=if0≤yy0→x+∞⊆A↔if0≤yy0+∞⊆A
49 48 rspcev ⊢if0≤yy0∈ℝ∧if0≤yy0+∞⊆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 syl6bi ⊢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