Metamath Proof Explorer

Theorem liminfval

Description: The inferior limit of a set F . (Contributed by Glauco Siliprandi, 2-Jan-2022)

Ref Expression
Hypothesis liminfval.1 
|- G = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
Assertion liminfval 
|- ( F e. V -> ( liminf ` F ) = sup ( ran G , RR* , < ) )

Proof

Step Hyp Ref Expression
1 liminfval.1 
 |-  G = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
2 df-liminf 
 |-  liminf = ( x e. _V |-> sup ( ran ( k e. RR |-> inf ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) )
3 imaeq1 
 |-  ( x = F -> ( x " ( k [,) +oo ) ) = ( F " ( k [,) +oo ) ) )
4 3 ineq1d 
 |-  ( x = F -> ( ( x " ( k [,) +oo ) ) i^i RR* ) = ( ( F " ( k [,) +oo ) ) i^i RR* ) )
5 4 infeq1d 
 |-  ( x = F -> inf ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) = inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) )
6 5 mpteq2dv 
 |-  ( x = F -> ( k e. RR |-> inf ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
7 1 a1i 
 |-  ( x = F -> G = ( k e. RR |-> inf ( ( ( F " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) )
8 6 7 eqtr4d 
 |-  ( x = F -> ( k e. RR |-> inf ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = G )
9 8 rneqd 
 |-  ( x = F -> ran ( k e. RR |-> inf ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) = ran G )
10 9 supeq1d 
 |-  ( x = F -> sup ( ran ( k e. RR |-> inf ( ( ( x " ( k [,) +oo ) ) i^i RR* ) , RR* , < ) ) , RR* , < ) = sup ( ran G , RR* , < ) )
11 elex 
 |-  ( F e. V -> F e. _V )
12 xrltso 
 |-  < Or RR*
13 12 supex 
 |-  sup ( ran G , RR* , < ) e. _V
14 13 a1i 
 |-  ( F e. V -> sup ( ran G , RR* , < ) e. _V )
15 2 10 11 14 fvmptd3 
 |-  ( F e. V -> ( liminf ` F ) = sup ( ran G , RR* , < ) )