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 e. ( ordTop ` <_ ) /\ -oo e. A ) -> E. x e. RR ( -oo [,) x ) C_ A )

Proof

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