Description: The inferior limit of a set F . (Contributed by Glauco Siliprandi, 2-Jan-2022)
Ref | Expression | ||
---|---|---|---|
Hypothesis | liminfval.1 | |
|
Assertion | liminfval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | liminfval.1 | |
|
2 | df-liminf | |
|
3 | imaeq1 | |
|
4 | 3 | ineq1d | |
5 | 4 | infeq1d | |
6 | 5 | mpteq2dv | |
7 | 1 | a1i | |
8 | 6 7 | eqtr4d | |
9 | 8 | rneqd | |
10 | 9 | supeq1d | |
11 | elex | |
|
12 | xrltso | |
|
13 | 12 | supex | |
14 | 13 | a1i | |
15 | 2 10 11 14 | fvmptd3 | |