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=ksupFk+∞**<
Assertion liminfval FVlim infF=supranG*<

Proof

Step Hyp Ref Expression
1 liminfval.1 G=ksupFk+∞**<
2 df-liminf lim inf=xVsupranksupxk+∞**<*<
3 imaeq1 x=Fxk+∞=Fk+∞
4 3 ineq1d x=Fxk+∞*=Fk+∞*
5 4 infeq1d x=Fsupxk+∞**<=supFk+∞**<
6 5 mpteq2dv x=Fksupxk+∞**<=ksupFk+∞**<
7 1 a1i x=FG=ksupFk+∞**<
8 6 7 eqtr4d x=Fksupxk+∞**<=G
9 8 rneqd x=Franksupxk+∞**<=ranG
10 9 supeq1d x=Fsupranksupxk+∞**<*<=supranG*<
11 elex FVFV
12 xrltso <Or*
13 12 supex supranG*<V
14 13 a1i FVsupranG*<V
15 2 10 11 14 fvmptd3 FVlim infF=supranG*<