Metamath Proof Explorer

Theorem liminfval5

Description: The inferior limit of an infinite sequence F of extended real numbers. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypotheses limsupval5.1 
|- F/ k ph
limsupval5.2 
|- ( ph -> A e. V )
limsupval5.3 
|- ( ph -> F : A --> RR* )
limsupval5.4 
|- G = ( k e. RR |-> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) )
Assertion liminfval5 
|- ( ph -> ( liminf ` F ) = sup ( ran G , RR* , < ) )

Proof

Step Hyp Ref Expression
1 limsupval5.1 
 |-  F/ k ph
2 limsupval5.2 
 |-  ( ph -> A e. V )
3 limsupval5.3 
 |-  ( ph -> F : A --> RR* )
4 limsupval5.4 
 |-  G = ( k e. RR |-> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) )
5 3 2 fexd 
 |-  ( ph -> F e. _V )
6 eqid 
 |-  ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
7 6 liminfval 
 |-  ( F e. _V -> ( liminf ` F ) = sup ( ran ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
8 5 7 syl 
 |-  ( ph -> ( liminf ` F ) = sup ( ran ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
9 4 a1i 
 |-  ( ph -> G = ( k e. RR |-> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) ) )
10 3 fimassd 
 |-  ( ph -> ( F " ( k [,) +oo ) ) C_ RR* )
11 df-ss 
 |-  ( ( F " ( k [,) +oo ) ) C_ RR* <-> ( ( F " ( k [,) +oo ) ) i^i RR* ) = ( F " ( k [,) +oo ) ) )
12 10 11 sylib 
 |-  ( ph -> ( ( F " ( k [,) +oo ) ) i^i RR* ) = ( F " ( k [,) +oo ) ) )
13 12 eqcomd 
 |-  ( ph -> ( F " ( k [,) +oo ) ) = ( ( F " ( k [,) +oo ) ) i^i RR* ) )
14 13 adantr 
 |-  ( ( ph /\ k e. RR ) -> ( F " ( k [,) +oo ) ) = ( ( F " ( k [,) +oo ) ) i^i RR* ) )
15 14 infeq1d 
 |-  ( ( ph /\ k e. RR ) -> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) = inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
16 1 15 mpteq2da 
 |-  ( ph -> ( k e. RR |-> inf ( ( F " ( k [,) +oo ) ) , RR* , < ) ) = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
17 9 16 eqtr2d 
 |-  ( ph -> ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = G )
18 17 rneqd 
 |-  ( ph -> ran ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ran G )
19 18 supeq1d 
 |-  ( ph -> sup ( ran ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) = sup ( ran G , RR* , < ) )
20 8 19 eqtrd 
 |-  ( ph -> ( liminf ` F ) = sup ( ran G , RR* , < ) )