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 e. ( ordTop ` <_ ) /\ +oo e. A ) -> E. x e. RR ( x (,] +oo ) 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 mnfxr 
 |-  -oo e. RR*
13 12 a1i 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> -oo e. RR* )
14 simprl 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> y e. RR* )
15 0xr 
 |-  0 e. RR*
16 ifcl 
 |-  ( ( y e. RR* /\ 0 e. RR* ) -> if ( 0 <_ y , y , 0 ) e. RR* )
17 14 15 16 sylancl 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> if ( 0 <_ y , y , 0 ) e. RR* )
18 pnfxr 
 |-  +oo e. RR*
19 18 a1i 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> +oo e. RR* )
20 xrmax1 
 |-  ( ( 0 e. RR* /\ y e. RR* ) -> 0 <_ if ( 0 <_ y , y , 0 ) )
21 15 14 20 sylancr 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> 0 <_ if ( 0 <_ y , y , 0 ) )
22 ge0gtmnf 
 |-  ( ( if ( 0 <_ y , y , 0 ) e. RR* /\ 0 <_ if ( 0 <_ y , y , 0 ) ) -> -oo < if ( 0 <_ y , y , 0 ) )
23 17 21 22 syl2anc 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> -oo < if ( 0 <_ y , y , 0 ) )
24 simpll 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> +oo e. u )
25 simprr 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> u = ( y (,] +oo ) )
26 24 25 eleqtrd 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> +oo e. ( y (,] +oo ) )
27 elioc1 
 |-  ( ( y e. RR* /\ +oo e. RR* ) -> ( +oo e. ( y (,] +oo ) <-> ( +oo e. RR* /\ y < +oo /\ +oo <_ +oo ) ) )
28 14 18 27 sylancl 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> ( +oo e. ( y (,] +oo ) <-> ( +oo e. RR* /\ y < +oo /\ +oo <_ +oo ) ) )
29 26 28 mpbid 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> ( +oo e. RR* /\ y < +oo /\ +oo <_ +oo ) )
30 29 simp2d 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> y < +oo )
31 0ltpnf 
 |-  0 < +oo
32 breq1 
 |-  ( y = if ( 0 <_ y , y , 0 ) -> ( y < +oo <-> if ( 0 <_ y , y , 0 ) < +oo ) )
33 breq1 
 |-  ( 0 = if ( 0 <_ y , y , 0 ) -> ( 0 < +oo <-> if ( 0 <_ y , y , 0 ) < +oo ) )
34 32 33 ifboth 
 |-  ( ( y < +oo /\ 0 < +oo ) -> if ( 0 <_ y , y , 0 ) < +oo )
35 30 31 34 sylancl 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> if ( 0 <_ y , y , 0 ) < +oo )
36 xrre2 
 |-  ( ( ( -oo e. RR* /\ if ( 0 <_ y , y , 0 ) e. RR* /\ +oo e. RR* ) /\ ( -oo < if ( 0 <_ y , y , 0 ) /\ if ( 0 <_ y , y , 0 ) < +oo ) ) -> if ( 0 <_ y , y , 0 ) e. RR )
37 13 17 19 23 35 36 syl32anc 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> if ( 0 <_ y , y , 0 ) e. RR )
38 xrmax2 
 |-  ( ( 0 e. RR* /\ y e. RR* ) -> y <_ if ( 0 <_ y , y , 0 ) )
39 15 14 38 sylancr 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> y <_ if ( 0 <_ y , y , 0 ) )
40 df-ioc 
 |-  (,] = ( a e. RR* , b e. RR* |-> { c e. RR* | ( a < c /\ c <_ b ) } )
41 xrlelttr 
 |-  ( ( y e. RR* /\ if ( 0 <_ y , y , 0 ) e. RR* /\ x e. RR* ) -> ( ( y <_ if ( 0 <_ y , y , 0 ) /\ if ( 0 <_ y , y , 0 ) < x ) -> y < x ) )
42 40 40 41 ixxss1 
 |-  ( ( y e. RR* /\ y <_ if ( 0 <_ y , y , 0 ) ) -> ( if ( 0 <_ y , y , 0 ) (,] +oo ) C_ ( y (,] +oo ) )
43 14 39 42 syl2anc 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> ( if ( 0 <_ y , y , 0 ) (,] +oo ) C_ ( y (,] +oo ) )
44 simplr 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> u C_ A )
45 25 44 eqsstrrd 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> ( y (,] +oo ) C_ A )
46 43 45 sstrd 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> ( if ( 0 <_ y , y , 0 ) (,] +oo ) C_ A )
47 oveq1 
 |-  ( x = if ( 0 <_ y , y , 0 ) -> ( x (,] +oo ) = ( if ( 0 <_ y , y , 0 ) (,] +oo ) )
48 47 sseq1d 
 |-  ( x = if ( 0 <_ y , y , 0 ) -> ( ( x (,] +oo ) C_ A <-> ( if ( 0 <_ y , y , 0 ) (,] +oo ) C_ A ) )
49 48 rspcev 
 |-  ( ( if ( 0 <_ y , y , 0 ) e. RR /\ ( if ( 0 <_ y , y , 0 ) (,] +oo ) C_ A ) -> E. x e. RR ( x (,] +oo ) C_ A )
50 37 46 49 syl2anc 
 |-  ( ( ( +oo e. u /\ u C_ A ) /\ ( y e. RR* /\ u = ( y (,] +oo ) ) ) -> E. x e. RR ( x (,] +oo ) C_ A )
51 50 rexlimdvaa 
 |-  ( ( +oo e. u /\ u C_ A ) -> ( E. y e. RR* u = ( y (,] +oo ) -> E. x e. RR ( x (,] +oo ) C_ A ) )
52 51 com12 
 |-  ( E. y e. RR* u = ( y (,] +oo ) -> ( ( +oo e. u /\ u C_ A ) -> E. x e. RR ( x (,] +oo ) C_ A ) )
53 11 52 sylbi 
 |-  ( u e. ran ( y e. RR* |-> ( y (,] +oo ) ) -> ( ( +oo e. u /\ u C_ A ) -> E. x e. RR ( x (,] +oo ) C_ A ) )
54 eqid 
 |-  ( y e. RR* |-> ( -oo [,) y ) ) = ( y e. RR* |-> ( -oo [,) y ) )
55 54 elrnmpt 
 |-  ( u e. _V -> ( u e. ran ( y e. RR* |-> ( -oo [,) y ) ) <-> E. y e. RR* u = ( -oo [,) y ) ) )
56 55 elv 
 |-  ( u e. ran ( y e. RR* |-> ( -oo [,) y ) ) <-> E. y e. RR* u = ( -oo [,) y ) )
57 pnfnlt 
 |-  ( y e. RR* -> -. +oo < y )
58 elico1 
 |-  ( ( -oo e. RR* /\ y e. RR* ) -> ( +oo e. ( -oo [,) y ) <-> ( +oo e. RR* /\ -oo <_ +oo /\ +oo < y ) ) )
59 12 58 mpan 
 |-  ( y e. RR* -> ( +oo e. ( -oo [,) y ) <-> ( +oo e. RR* /\ -oo <_ +oo /\ +oo < y ) ) )
60 simp3 
 |-  ( ( +oo e. RR* /\ -oo <_ +oo /\ +oo < y ) -> +oo < y )
61 59 60 syl6bi 
 |-  ( y e. RR* -> ( +oo e. ( -oo [,) y ) -> +oo < y ) )
62 57 61 mtod 
 |-  ( y e. RR* -> -. +oo e. ( -oo [,) y ) )
63 eleq2 
 |-  ( u = ( -oo [,) y ) -> ( +oo e. u <-> +oo e. ( -oo [,) y ) ) )
64 63 notbid 
 |-  ( u = ( -oo [,) y ) -> ( -. +oo e. u <-> -. +oo e. ( -oo [,) y ) ) )
65 62 64 syl5ibrcom 
 |-  ( y e. RR* -> ( u = ( -oo [,) y ) -> -. +oo e. u ) )
66 65 rexlimiv 
 |-  ( E. y e. RR* u = ( -oo [,) y ) -> -. +oo e. u )
67 66 pm2.21d 
 |-  ( E. y e. RR* u = ( -oo [,) y ) -> ( +oo e. u -> E. x e. RR ( x (,] +oo ) C_ A ) )
68 67 adantrd 
 |-  ( E. y e. RR* u = ( -oo [,) y ) -> ( ( +oo e. u /\ u C_ A ) -> E. x e. RR ( x (,] +oo ) C_ A ) )
69 56 68 sylbi 
 |-  ( u e. ran ( y e. RR* |-> ( -oo [,) y ) ) -> ( ( +oo e. u /\ u C_ A ) -> E. x e. RR ( x (,] +oo ) C_ A ) )
70 53 69 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 ( x (,] +oo ) C_ A ) )
71 8 70 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 ( x (,] +oo ) C_ A ) )
72 pnfnre 
 |-  +oo e/ RR
73 72 neli 
 |-  -. +oo e. RR
74 elssuni 
 |-  ( u e. ran (,) -> u C_ U. ran (,) )
75 unirnioo 
 |-  RR = U. ran (,)
76 74 75 sseqtrrdi 
 |-  ( u e. ran (,) -> u C_ RR )
77 76 sseld 
 |-  ( u e. ran (,) -> ( +oo e. u -> +oo e. RR ) )
78 73 77 mtoi 
 |-  ( u e. ran (,) -> -. +oo e. u )
79 78 pm2.21d 
 |-  ( u e. ran (,) -> ( +oo e. u -> E. x e. RR ( x (,] +oo ) C_ A ) )
80 79 adantrd 
 |-  ( u e. ran (,) -> ( ( +oo e. u /\ u C_ A ) -> E. x e. RR ( x (,] +oo ) C_ A ) )
81 71 80 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 ( x (,] +oo ) C_ A ) )
82 7 81 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 ( x (,] +oo ) C_ A ) )
83 82 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 ( x (,] +oo ) C_ A )
84 6 83 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 ( x (,] +oo ) C_ A )
85 5 84 sylanb 
 |-  ( ( A e. ( ordTop ` <_ ) /\ +oo e. A ) -> E. x e. RR ( x (,] +oo ) C_ A )