Metamath Proof Explorer

Theorem limsuppnfdlem

Description: If the restriction of a function to every upper interval is unbounded above, its limsup is +oo . (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 limsuppnfdlem.a 
 |-  ( ph -> A C_ RR )
2 limsuppnfdlem.f 
 |-  ( ph -> F : A --> RR* )
3 limsuppnfdlem.u 
 |-  ( ph -> A. x e. RR A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
4 limsuppnfdlem.g 
 |-  G = ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
5 reex 
 |-  RR e. _V
6 5 a1i 
 |-  ( ph -> RR e. _V )
7 6 1 ssexd 
 |-  ( ph -> A e. _V )
8 2 7 fexd 
 |-  ( ph -> F e. _V )
9 4 limsupval 
 |-  ( F e. _V -> ( limsup ` F ) = inf ( ran G , RR* , < ) )
10 8 9 syl 
 |-  ( ph -> ( limsup ` F ) = inf ( ran G , RR* , < ) )
11 2 ffund 
 |-  ( ph -> Fun F )
12 11 adantr 
 |-  ( ( ph /\ j e. A ) -> Fun F )
13 simpr 
 |-  ( ( ph /\ j e. A ) -> j e. A )
14 2 fdmd 
 |-  ( ph -> dom F = A )
15 14 adantr 
 |-  ( ( ph /\ j e. A ) -> dom F = A )
16 13 15 eleqtrrd 
 |-  ( ( ph /\ j e. A ) -> j e. dom F )
17 12 16 jca 
 |-  ( ( ph /\ j e. A ) -> ( Fun F /\ j e. dom F ) )
18 17 ad4ant13 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> ( Fun F /\ j e. dom F ) )
19 simpllr 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> k e. RR )
20 19 rexrd 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> k e. RR* )
21 pnfxr 
 |-  +oo e. RR*
22 21 a1i 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> +oo e. RR* )
23 1 ssrexr 
 |-  ( ph -> A C_ RR* )
24 23 sselda 
 |-  ( ( ph /\ j e. A ) -> j e. RR* )
25 24 ad4ant13 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> j e. RR* )
26 simpr 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> k <_ j )
27 1 sselda 
 |-  ( ( ph /\ j e. A ) -> j e. RR )
28 27 ltpnfd 
 |-  ( ( ph /\ j e. A ) -> j < +oo )
29 28 ad4ant13 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> j < +oo )
30 20 22 25 26 29 elicod 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> j e. ( k [,) +oo ) )
31 funfvima 
 |-  ( ( Fun F /\ j e. dom F ) -> ( j e. ( k [,) +oo ) -> ( F ` j ) e. ( F " ( k [,) +oo ) ) ) )
32 18 30 31 sylc 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> ( F ` j ) e. ( F " ( k [,) +oo ) ) )
33 2 ffvelrnda 
 |-  ( ( ph /\ j e. A ) -> ( F ` j ) e. RR* )
34 33 ad4ant13 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> ( F ` j ) e. RR* )
35 32 34 elind 
 |-  ( ( ( ( ph /\ k e. RR ) /\ j e. A ) /\ k <_ j ) -> ( F ` j ) e. ( ( F " ( k [,) +oo ) ) i^i RR* ) )
36 35 adantllr 
 |-  ( ( ( ( ( ph /\ k e. RR ) /\ x e. RR ) /\ j e. A ) /\ k <_ j ) -> ( F ` j ) e. ( ( F " ( k [,) +oo ) ) i^i RR* ) )
37 36 adantrr 
 |-  ( ( ( ( ( ph /\ k e. RR ) /\ x e. RR ) /\ j e. A ) /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> ( F ` j ) e. ( ( F " ( k [,) +oo ) ) i^i RR* ) )
38 simprr 
 |-  ( ( ( ( ( ph /\ k e. RR ) /\ x e. RR ) /\ j e. A ) /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> x <_ ( F ` j ) )
39 breq2 
 |-  ( y = ( F ` j ) -> ( x <_ y <-> x <_ ( F ` j ) ) )
40 39 rspcev 
 |-  ( ( ( F ` j ) e. ( ( F " ( k [,) +oo ) ) i^i RR* ) /\ x <_ ( F ` j ) ) -> E. y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) x <_ y )
41 37 38 40 syl2anc 
 |-  ( ( ( ( ( ph /\ k e. RR ) /\ x e. RR ) /\ j e. A ) /\ ( k <_ j /\ x <_ ( F ` j ) ) ) -> E. y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) x <_ y )
42 3 r19.21bi 
 |-  ( ( ph /\ x e. RR ) -> A. k e. RR E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
43 42 r19.21bi 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. RR ) -> E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
44 43 an32s 
 |-  ( ( ( ph /\ k e. RR ) /\ x e. RR ) -> E. j e. A ( k <_ j /\ x <_ ( F ` j ) ) )
45 41 44 r19.29a 
 |-  ( ( ( ph /\ k e. RR ) /\ x e. RR ) -> E. y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) x <_ y )
46 45 ralrimiva 
 |-  ( ( ph /\ k e. RR ) -> A. x e. RR E. y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) x <_ y )
47 inss2 
 |-  ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR*
48 supxrunb3 
 |-  ( ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR* -> ( A. x e. RR E. y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) x <_ y <-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = +oo ) )
49 47 48 mp1i 
 |-  ( ( ph /\ k e. RR ) -> ( A. x e. RR E. y e. ( ( F " ( k [,) +oo ) ) i^i RR* ) x <_ y <-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = +oo ) )
50 46 49 mpbid 
 |-  ( ( ph /\ k e. RR ) -> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = +oo )
51 50 mpteq2dva 
 |-  ( ph -> ( k e. RR |-> sup ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> +oo ) )
52 4 51 syl5eq 
 |-  ( ph -> G = ( k e. RR |-> +oo ) )
53 52 rneqd 
 |-  ( ph -> ran G = ran ( k e. RR |-> +oo ) )
54 eqid 
 |-  ( k e. RR |-> +oo ) = ( k e. RR |-> +oo )
55 ren0 
 |-  RR =/= (/)
56 55 a1i 
 |-  ( ph -> RR =/= (/) )
57 54 56 rnmptc 
 |-  ( ph -> ran ( k e. RR |-> +oo ) = { +oo } )
58 53 57 eqtrd 
 |-  ( ph -> ran G = { +oo } )
59 58 infeq1d 
 |-  ( ph -> inf ( ran G , RR* , < ) = inf ( { +oo } , RR* , < ) )
60 xrltso 
 |-  < Or RR*
61 infsn 
 |-  ( ( < Or RR* /\ +oo e. RR* ) -> inf ( { +oo } , RR* , < ) = +oo )
62 60 21 61 mp2an 
 |-  inf ( { +oo } , RR* , < ) = +oo
63 62 a1i 
 |-  ( ph -> inf ( { +oo } , RR* , < ) = +oo )
64 10 59 63 3eqtrd 
 |-  ( ph -> ( limsup ` F ) = +oo )