Metamath Proof Explorer

Theorem limsupmnflem

Description: The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to an upper interval of real numbers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupmnflem.a 
|- ( ph -> A C_ RR )
limsupmnflem.f 
|- ( ph -> F : A --> RR* )
limsupmnflem.g 
|- G = ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) )
Assertion limsupmnflem 
|- ( ph -> ( ( limsup ` F ) = -oo <-> A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )

Proof

Step Hyp Ref Expression
1 limsupmnflem.a 
 |-  ( ph -> A C_ RR )
2 limsupmnflem.f 
 |-  ( ph -> F : A --> RR* )
3 limsupmnflem.g 
 |-  G = ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) )
4 nfv 
 |-  F/ k ph
5 reex 
 |-  RR e. _V
6 5 a1i 
 |-  ( ph -> RR e. _V )
7 6 1 ssexd 
 |-  ( ph -> A e. _V )
8 4 7 2 3 limsupval3 
 |-  ( ph -> ( limsup ` F ) = inf ( ran G , RR* , < ) )
9 3 rneqi 
 |-  ran G = ran ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) )
10 9 infeq1i 
 |-  inf ( ran G , RR* , < ) = inf ( ran ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) , RR* , < )
11 10 a1i 
 |-  ( ph -> inf ( ran G , RR* , < ) = inf ( ran ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) , RR* , < ) )
12 8 11 eqtrd 
 |-  ( ph -> ( limsup ` F ) = inf ( ran ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) , RR* , < ) )
13 12 eqeq1d 
 |-  ( ph -> ( ( limsup ` F ) = -oo <-> inf ( ran ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) , RR* , < ) = -oo ) )
14 nfv 
 |-  F/ x ph
15 2 fimassd 
 |-  ( ph -> ( F " ( k [,) +oo ) ) C_ RR* )
16 15 adantr 
 |-  ( ( ph /\ k e. RR ) -> ( F " ( k [,) +oo ) ) C_ RR* )
17 16 supxrcld 
 |-  ( ( ph /\ k e. RR ) -> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) e. RR* )
18 4 14 17 infxrunb3rnmpt 
 |-  ( ph -> ( A. x e. RR E. k e. RR sup ( ( F " ( k [,) +oo ) ) , RR* , < ) <_ x <-> inf ( ran ( k e. RR |-> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) ) , RR* , < ) = -oo ) )
19 15 adantr 
 |-  ( ( ph /\ x e. RR ) -> ( F " ( k [,) +oo ) ) C_ RR* )
20 ressxr 
 |-  RR C_ RR*
21 20 a1i 
 |-  ( ph -> RR C_ RR* )
22 21 sselda 
 |-  ( ( ph /\ x e. RR ) -> x e. RR* )
23 supxrleub 
 |-  ( ( ( F " ( k [,) +oo ) ) C_ RR* /\ x e. RR* ) -> ( sup ( ( F " ( k [,) +oo ) ) , RR* , < ) <_ x <-> A. y e. ( F " ( k [,) +oo ) ) y <_ x ) )
24 19 22 23 syl2anc 
 |-  ( ( ph /\ x e. RR ) -> ( sup ( ( F " ( k [,) +oo ) ) , RR* , < ) <_ x <-> A. y e. ( F " ( k [,) +oo ) ) y <_ x ) )
25 24 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. RR ) -> ( sup ( ( F " ( k [,) +oo ) ) , RR* , < ) <_ x <-> A. y e. ( F " ( k [,) +oo ) ) y <_ x ) )
26 2 ffnd 
 |-  ( ph -> F Fn A )
27 26 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> F Fn A )
28 simplr 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> j e. A )
29 20 sseli 
 |-  ( k e. RR -> k e. RR* )
30 29 ad3antlr 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> k e. RR* )
31 pnfxr 
 |-  +oo e. RR*
32 31 a1i 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> +oo e. RR* )
33 20 a1i 
 |-  ( ( ph /\ j e. A ) -> RR C_ RR* )
34 1 sselda 
 |-  ( ( ph /\ j e. A ) -> j e. RR )
35 33 34 sseldd 
 |-  ( ( ph /\ j e. A ) -> j e. RR* )
36 35 ad4ant13 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> j e. RR* )
37 simpr 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> k <_ j )
38 34 ltpnfd 
 |-  ( ( ph /\ j e. A ) -> j < +oo )
39 38 ad4ant13 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> j < +oo )
40 30 32 36 37 39 elicod 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> j e. ( k [,) +oo ) )
41 27 28 40 fnfvimad 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> ( F ` j ) e. ( F " ( k [,) +oo ) ) )
42 41 adantllr 
 |-  ( ( ( ( ( ph /\ k e. RR ) /\ A. y e. ( F " ( k [,) +oo ) ) y <_ x ) /\ j e. A ) /\ k <_ j ) -> ( F ` j ) e. ( F " ( k [,) +oo ) ) )
43 simpllr 
 |-  ( ( ( ( ( ph /\ k e. RR ) /\ A. y e. ( F " ( k [,) +oo ) ) y <_ x ) /\ j e. A ) /\ k <_ j ) -> A. y e. ( F " ( k [,) +oo ) ) y <_ x )
44 breq1 
 |-  ( y = ( F ` j ) -> ( y <_ x <-> ( F ` j ) <_ x ) )
45 44 rspcva 
 |-  ( ( ( F ` j ) e. ( F " ( k [,) +oo ) ) /\ A. y e. ( F " ( k [,) +oo ) ) y <_ x ) -> ( F ` j ) <_ x )
46 42 43 45 syl2anc 
 |-  ( ( ( ( ( ph /\ k e. RR ) /\ A. y e. ( F " ( k [,) +oo ) ) y <_ x ) /\ j e. A ) /\ k <_ j ) -> ( F ` j ) <_ x )
47 46 adantl4r 
 |-  ( ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ A. y e. ( F " ( k [,) +oo ) ) y <_ x ) /\ j e. A ) /\ k <_ j ) -> ( F ` j ) <_ x )
48 47 ex 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ A. y e. ( F " ( k [,) +oo ) ) y <_ x ) /\ j e. A ) -> ( k <_ j -> ( F ` j ) <_ x ) )
49 48 ralrimiva 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ A. y e. ( F " ( k [,) +oo ) ) y <_ x ) -> A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
50 49 ex 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. RR ) -> ( A. y e. ( F " ( k [,) +oo ) ) y <_ x -> A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
51 nfcv 
 |-  F/_ j F
52 26 adantr 
 |-  ( ( ph /\ y e. ( F " ( k [,) +oo ) ) ) -> F Fn A )
53 simpr 
 |-  ( ( ph /\ y e. ( F " ( k [,) +oo ) ) ) -> y e. ( F " ( k [,) +oo ) ) )
54 51 52 53 fvelimad 
 |-  ( ( ph /\ y e. ( F " ( k [,) +oo ) ) ) -> E. j e. ( A i^i ( k [,) +oo ) ) ( F ` j ) = y )
55 54 ad4ant14 
 |-  ( ( ( ( ph /\ k e. RR ) /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) /\ y e. ( F " ( k [,) +oo ) ) ) -> E. j e. ( A i^i ( k [,) +oo ) ) ( F ` j ) = y )
56 nfv 
 |-  F/ j ( ph /\ k e. RR )
57 nfra1 
 |-  F/ j A. j e. A ( k <_ j -> ( F ` j ) <_ x )
58 56 57 nfan 
 |-  F/ j ( ( ph /\ k e. RR ) /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
59 nfv 
 |-  F/ j y <_ x
60 29 adantr 
 |-  ( ( k e. RR /\ j e. ( A i^i ( k [,) +oo ) ) ) -> k e. RR* )
61 31 a1i 
 |-  ( ( k e. RR /\ j e. ( A i^i ( k [,) +oo ) ) ) -> +oo e. RR* )
62 elinel2 
 |-  ( j e. ( A i^i ( k [,) +oo ) ) -> j e. ( k [,) +oo ) )
63 62 adantl 
 |-  ( ( k e. RR /\ j e. ( A i^i ( k [,) +oo ) ) ) -> j e. ( k [,) +oo ) )
64 60 61 63 icogelbd 
 |-  ( ( k e. RR /\ j e. ( A i^i ( k [,) +oo ) ) ) -> k <_ j )
65 64 adantlr 
 |-  ( ( ( k e. RR /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( A i^i ( k [,) +oo ) ) ) -> k <_ j )
66 elinel1 
 |-  ( j e. ( A i^i ( k [,) +oo ) ) -> j e. A )
67 66 adantl 
 |-  ( ( A. j e. A ( k <_ j -> ( F ` j ) <_ x ) /\ j e. ( A i^i ( k [,) +oo ) ) ) -> j e. A )
68 rspa 
 |-  ( ( A. j e. A ( k <_ j -> ( F ` j ) <_ x ) /\ j e. A ) -> ( k <_ j -> ( F ` j ) <_ x ) )
69 67 68 syldan 
 |-  ( ( A. j e. A ( k <_ j -> ( F ` j ) <_ x ) /\ j e. ( A i^i ( k [,) +oo ) ) ) -> ( k <_ j -> ( F ` j ) <_ x ) )
70 69 adantll 
 |-  ( ( ( k e. RR /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( A i^i ( k [,) +oo ) ) ) -> ( k <_ j -> ( F ` j ) <_ x ) )
71 65 70 mpd 
 |-  ( ( ( k e. RR /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( A i^i ( k [,) +oo ) ) ) -> ( F ` j ) <_ x )
72 id 
 |-  ( ( F ` j ) = y -> ( F ` j ) = y )
73 72 eqcomd 
 |-  ( ( F ` j ) = y -> y = ( F ` j ) )
74 73 adantl 
 |-  ( ( ( F ` j ) <_ x /\ ( F ` j ) = y ) -> y = ( F ` j ) )
75 simpl 
 |-  ( ( ( F ` j ) <_ x /\ ( F ` j ) = y ) -> ( F ` j ) <_ x )
76 74 75 eqbrtrd 
 |-  ( ( ( F ` j ) <_ x /\ ( F ` j ) = y ) -> y <_ x )
77 76 ex 
 |-  ( ( F ` j ) <_ x -> ( ( F ` j ) = y -> y <_ x ) )
78 71 77 syl 
 |-  ( ( ( k e. RR /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( A i^i ( k [,) +oo ) ) ) -> ( ( F ` j ) = y -> y <_ x ) )
79 78 adantlll 
 |-  ( ( ( ( ph /\ k e. RR ) /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( A i^i ( k [,) +oo ) ) ) -> ( ( F ` j ) = y -> y <_ x ) )
80 79 ex 
 |-  ( ( ( ph /\ k e. RR ) /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> ( j e. ( A i^i ( k [,) +oo ) ) -> ( ( F ` j ) = y -> y <_ x ) ) )
81 58 59 80 rexlimd 
 |-  ( ( ( ph /\ k e. RR ) /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> ( E. j e. ( A i^i ( k [,) +oo ) ) ( F ` j ) = y -> y <_ x ) )
82 81 imp 
 |-  ( ( ( ( ph /\ k e. RR ) /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) /\ E. j e. ( A i^i ( k [,) +oo ) ) ( F ` j ) = y ) -> y <_ x )
83 55 82 syldan 
 |-  ( ( ( ( ph /\ k e. RR ) /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) /\ y e. ( F " ( k [,) +oo ) ) ) -> y <_ x )
84 83 ralrimiva 
 |-  ( ( ( ph /\ k e. RR ) /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> A. y e. ( F " ( k [,) +oo ) ) y <_ x )
85 84 adantllr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> A. y e. ( F " ( k [,) +oo ) ) y <_ x )
86 24 ad2antrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> ( sup ( ( F " ( k [,) +oo ) ) , RR* , < ) <_ x <-> A. y e. ( F " ( k [,) +oo ) ) y <_ x ) )
87 85 86 mpbird 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) <_ x )
88 87 ex 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. RR ) -> ( A. j e. A ( k <_ j -> ( F ` j ) <_ x ) -> sup ( ( F " ( k [,) +oo ) ) , RR* , < ) <_ x ) )
89 88 25 sylibd 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. RR ) -> ( A. j e. A ( k <_ j -> ( F ` j ) <_ x ) -> A. y e. ( F " ( k [,) +oo ) ) y <_ x ) )
90 50 89 impbid 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. RR ) -> ( A. y e. ( F " ( k [,) +oo ) ) y <_ x <-> A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
91 25 90 bitrd 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. RR ) -> ( sup ( ( F " ( k [,) +oo ) ) , RR* , < ) <_ x <-> A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
92 91 rexbidva 
 |-  ( ( ph /\ x e. RR ) -> ( E. k e. RR sup ( ( F " ( k [,) +oo ) ) , RR* , < ) <_ x <-> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
93 92 ralbidva 
 |-  ( ph -> ( A. x e. RR E. k e. RR sup ( ( F " ( k [,) +oo ) ) , RR* , < ) <_ x <-> A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )
94 13 18 93 3bitr2d 
 |-  ( ph -> ( ( limsup ` F ) = -oo <-> A. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) )