Detailed syntax breakdown of Definition df-liminf
Step | Hyp | Ref
| Expression |
1 | | clsi 42393 |
. 2
class lim
inf |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cvv 3441 |
. . 3
class
V |
4 | | vk |
. . . . . 6
setvar 𝑘 |
5 | | cr 10525 |
. . . . . 6
class
ℝ |
6 | 2 | cv 1537 |
. . . . . . . . 9
class 𝑥 |
7 | 4 | cv 1537 |
. . . . . . . . . 10
class 𝑘 |
8 | | cpnf 10661 |
. . . . . . . . . 10
class
+∞ |
9 | | cico 12728 |
. . . . . . . . . 10
class
[,) |
10 | 7, 8, 9 | co 7135 |
. . . . . . . . 9
class (𝑘[,)+∞) |
11 | 6, 10 | cima 5522 |
. . . . . . . 8
class (𝑥 “ (𝑘[,)+∞)) |
12 | | cxr 10663 |
. . . . . . . 8
class
ℝ* |
13 | 11, 12 | cin 3880 |
. . . . . . 7
class ((𝑥 “ (𝑘[,)+∞)) ∩
ℝ*) |
14 | | clt 10664 |
. . . . . . 7
class
< |
15 | 13, 12, 14 | cinf 8889 |
. . . . . 6
class
inf(((𝑥 “
(𝑘[,)+∞)) ∩
ℝ*), ℝ*, < ) |
16 | 4, 5, 15 | cmpt 5110 |
. . . . 5
class (𝑘 ∈ ℝ ↦
inf(((𝑥 “ (𝑘[,)+∞)) ∩
ℝ*), ℝ*, < )) |
17 | 16 | crn 5520 |
. . . 4
class ran
(𝑘 ∈ ℝ ↦
inf(((𝑥 “ (𝑘[,)+∞)) ∩
ℝ*), ℝ*, < )) |
18 | 17, 12, 14 | csup 8888 |
. . 3
class sup(ran
(𝑘 ∈ ℝ ↦
inf(((𝑥 “ (𝑘[,)+∞)) ∩
ℝ*), ℝ*, < )), ℝ*, <
) |
19 | 2, 3, 18 | cmpt 5110 |
. 2
class (𝑥 ∈ V ↦ sup(ran (𝑘 ∈ ℝ ↦
inf(((𝑥 “ (𝑘[,)+∞)) ∩
ℝ*), ℝ*, < )), ℝ*, <
)) |
20 | 1, 19 | wceq 1538 |
1
wff lim inf =
(𝑥 ∈ V ↦ sup(ran
(𝑘 ∈ ℝ ↦
inf(((𝑥 “ (𝑘[,)+∞)) ∩
ℝ*), ℝ*, < )), ℝ*, <
)) |