Metamath Proof Explorer


Theorem mnfnei

Description: A neighborhood of -oo contains an unbounded interval based at a real number. (Contributed by Mario Carneiro, 3-Sep-2015)

Ref Expression
Assertion mnfnei 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 nltmnf y * ¬ y < −∞
13 pnfxr +∞ *
14 elioc1 y * +∞ * −∞ y +∞ −∞ * y < −∞ −∞ +∞
15 13 14 mpan2 y * −∞ y +∞ −∞ * y < −∞ −∞ +∞
16 simp2 −∞ * y < −∞ −∞ +∞ y < −∞
17 15 16 syl6bi y * −∞ y +∞ y < −∞
18 12 17 mtod y * ¬ −∞ y +∞
19 eleq2 u = y +∞ −∞ u −∞ y +∞
20 19 notbid u = y +∞ ¬ −∞ u ¬ −∞ y +∞
21 18 20 syl5ibrcom y * u = y +∞ ¬ −∞ u
22 21 rexlimiv y * u = y +∞ ¬ −∞ u
23 22 pm2.21d y * u = y +∞ −∞ u x −∞ x A
24 23 adantrd y * u = y +∞ −∞ u u A x −∞ x A
25 11 24 sylbi u ran y * y +∞ −∞ u u A x −∞ x A
26 eqid y * −∞ y = y * −∞ y
27 26 elrnmpt u V u ran y * −∞ y y * u = −∞ y
28 27 elv u ran y * −∞ y y * u = −∞ y
29 mnfxr −∞ *
30 29 a1i −∞ u u A y * u = −∞ y −∞ *
31 0xr 0 *
32 simprl −∞ u u A y * u = −∞ y y *
33 ifcl 0 * y * if 0 y 0 y *
34 31 32 33 sylancr −∞ u u A y * u = −∞ y if 0 y 0 y *
35 13 a1i −∞ u u A y * u = −∞ y +∞ *
36 mnflt0 −∞ < 0
37 simpll −∞ u u A y * u = −∞ y −∞ u
38 simprr −∞ u u A y * u = −∞ y u = −∞ y
39 37 38 eleqtrd −∞ u u A y * u = −∞ y −∞ −∞ y
40 elico1 −∞ * y * −∞ −∞ y −∞ * −∞ −∞ −∞ < y
41 29 32 40 sylancr −∞ u u A y * u = −∞ y −∞ −∞ y −∞ * −∞ −∞ −∞ < y
42 39 41 mpbid −∞ u u A y * u = −∞ y −∞ * −∞ −∞ −∞ < y
43 42 simp3d −∞ u u A y * u = −∞ y −∞ < y
44 breq2 0 = if 0 y 0 y −∞ < 0 −∞ < if 0 y 0 y
45 breq2 y = if 0 y 0 y −∞ < y −∞ < if 0 y 0 y
46 44 45 ifboth −∞ < 0 −∞ < y −∞ < if 0 y 0 y
47 36 43 46 sylancr −∞ u u A y * u = −∞ y −∞ < if 0 y 0 y
48 31 a1i −∞ u u A y * u = −∞ y 0 *
49 xrmin1 0 * y * if 0 y 0 y 0
50 31 32 49 sylancr −∞ u u A y * u = −∞ y if 0 y 0 y 0
51 0re 0
52 ltpnf 0 0 < +∞
53 51 52 mp1i −∞ u u A y * u = −∞ y 0 < +∞
54 34 48 35 50 53 xrlelttrd −∞ u u A y * u = −∞ y if 0 y 0 y < +∞
55 xrre2 −∞ * if 0 y 0 y * +∞ * −∞ < if 0 y 0 y if 0 y 0 y < +∞ if 0 y 0 y
56 30 34 35 47 54 55 syl32anc −∞ u u A y * u = −∞ y if 0 y 0 y
57 xrmin2 0 * y * if 0 y 0 y y
58 31 32 57 sylancr −∞ u u A y * u = −∞ y if 0 y 0 y y
59 df-ico . = a * , b * c * | a c c < b
60 xrltletr x * if 0 y 0 y * y * x < if 0 y 0 y if 0 y 0 y y x < y
61 59 59 60 ixxss2 y * if 0 y 0 y y −∞ if 0 y 0 y −∞ y
62 32 58 61 syl2anc −∞ u u A y * u = −∞ y −∞ if 0 y 0 y −∞ y
63 simplr −∞ u u A y * u = −∞ y u A
64 38 63 eqsstrrd −∞ u u A y * u = −∞ y −∞ y A
65 62 64 sstrd −∞ u u A y * u = −∞ y −∞ if 0 y 0 y A
66 oveq2 x = if 0 y 0 y −∞ x = −∞ if 0 y 0 y
67 66 sseq1d x = if 0 y 0 y −∞ x A −∞ if 0 y 0 y A
68 67 rspcev if 0 y 0 y −∞ if 0 y 0 y A x −∞ x A
69 56 65 68 syl2anc −∞ u u A y * u = −∞ y x −∞ x A
70 69 rexlimdvaa −∞ u u A y * u = −∞ y x −∞ x A
71 70 com12 y * u = −∞ y −∞ u u A x −∞ x A
72 28 71 sylbi u ran y * −∞ y −∞ u u A x −∞ x A
73 25 72 jaoi u ran y * y +∞ u ran y * −∞ y −∞ u u A x −∞ x A
74 8 73 sylbi u ran y * y +∞ ran y * −∞ y −∞ u u A x −∞ x A
75 mnfnre −∞
76 75 neli ¬ −∞
77 elssuni u ran . u ran .
78 unirnioo = ran .
79 77 78 sseqtrrdi u ran . u
80 79 sseld u ran . −∞ u −∞
81 76 80 mtoi u ran . ¬ −∞ u
82 81 pm2.21d u ran . −∞ u x −∞ x A
83 82 adantrd u ran . −∞ u u A x −∞ x A
84 74 83 jaoi u ran y * y +∞ ran y * −∞ y u ran . −∞ u u A x −∞ x A
85 7 84 sylbi u ran y * y +∞ ran y * −∞ y ran . −∞ u u A x −∞ x A
86 85 rexlimiv u ran y * y +∞ ran y * −∞ y ran . −∞ u u A x −∞ x A
87 6 86 syl A topGen ran y * y +∞ ran y * −∞ y ran . −∞ A x −∞ x A
88 5 87 sylanb A ordTop −∞ A x −∞ x A