Metamath Proof Explorer

Theorem liminfcl

Description: Closure of the inferior limit. (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Assertion liminfcl 
|- ( F e. V -> ( liminf ` F ) e. RR* )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
2 1 liminfval 
 |-  ( F e. V -> ( liminf ` F ) = sup ( ran ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
3 nfv 
 |-  F/ k F e. V
4 inss2 
 |-  ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR*
5 infxrcl 
 |-  ( ( ( F " ( k [,) +oo ) ) i^i RR* ) C_ RR* -> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
6 4 5 ax-mp 
 |-  inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR*
7 6 a1i 
 |-  ( ( F e. V /\ k e. RR ) -> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) e. RR* )
8 3 1 7 rnmptssd 
 |-  ( F e. V -> ran ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) C_ RR* )
9 8 supxrcld 
 |-  ( F e. V -> sup ( ran ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) e. RR* )
10 2 9 eqeltrd 
 |-  ( F e. V -> ( liminf ` F ) e. RR* )