This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsupub2

Description: A extended real valued function, with limsup that is not +oo , is eventually less than +oo . (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Hypotheses limsupub2.1 
|- F/ j ph
limsupub2.2 
|- F/_ j F
limsupub2.3 
|- ( ph -> A C_ RR )
limsupub2.4 
|- ( ph -> F : A --> RR* )
limsupub2.5 
|- ( ph -> ( limsup ` F ) =/= +oo )
Assertion limsupub2 
|- ( ph -> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < +oo ) )

Proof

Step Hyp Ref Expression
1 limsupub2.1 
 |-  F/ j ph
2 limsupub2.2 
 |-  F/_ j F
3 limsupub2.3 
 |-  ( ph -> A C_ RR )
4 limsupub2.4 
 |-  ( ph -> F : A --> RR* )
5 limsupub2.5 
 |-  ( ph -> ( limsup ` F ) =/= +oo )
6 nfv 
 |-  F/ j x e. RR
7 1 6 nfan 
 |-  F/ j ( ph /\ x e. RR )
8 nfv 
 |-  F/ j k e. RR
9 7 8 nfan 
 |-  F/ j ( ( ph /\ x e. RR ) /\ k e. RR )
10 4 ffvelcdmda 
 |-  ( ( ph /\ j e. A ) -> ( F ` j ) e. RR* )
11 10 ad5ant14 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) /\ ( F ` j ) <_ x ) -> ( F ` j ) e. RR* )
12 rexr 
 |-  ( x e. RR -> x e. RR* )
13 12 ad4antlr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) /\ ( F ` j ) <_ x ) -> x e. RR* )
14 pnfxr 
 |-  +oo e. RR*
15 14 a1i 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) /\ ( F ` j ) <_ x ) -> +oo e. RR* )
16 simpr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) /\ ( F ` j ) <_ x ) -> ( F ` j ) <_ x )
17 ltpnf 
 |-  ( x e. RR -> x < +oo )
18 17 ad4antlr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) /\ ( F ` j ) <_ x ) -> x < +oo )
19 11 13 15 16 18 xrlelttrd 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) /\ ( F ` j ) <_ x ) -> ( F ` j ) < +oo )
20 19 ex 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) -> ( ( F ` j ) <_ x -> ( F ` j ) < +oo ) )
21 20 imim2d 
 |-  ( ( ( ( ph /\ x e. RR ) /\ k e. RR ) /\ j e. A ) -> ( ( k <_ j -> ( F ` j ) <_ x ) -> ( k <_ j -> ( F ` j ) < +oo ) ) )
22 9 21 ralimdaa 
 |-  ( ( ( ph /\ x e. RR ) /\ k e. RR ) -> ( A. j e. A ( k <_ j -> ( F ` j ) <_ x ) -> A. j e. A ( k <_ j -> ( F ` j ) < +oo ) ) )
23 22 reximdva 
 |-  ( ( ph /\ x e. RR ) -> ( E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) -> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < +oo ) ) )
24 23 imp 
 |-  ( ( ( ph /\ x e. RR ) /\ E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) ) -> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < +oo ) )
25 1 2 3 4 5 limsupub 
 |-  ( ph -> E. x e. RR E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) <_ x ) )
26 24 25 r19.29a 
 |-  ( ph -> E. k e. RR A. j e. A ( k <_ j -> ( F ` j ) < +oo ) )