Detailed syntax breakdown of Definition df-sumge0
Step | Hyp | Ref
| Expression |
1 | | csumge0 43881 |
. 2
class
Σ^ |
2 | | vx |
. . 3
setvar 𝑥 |
3 | | cvv 3429 |
. . 3
class
V |
4 | | cpnf 11016 |
. . . . 5
class
+∞ |
5 | 2 | cv 1538 |
. . . . . 6
class 𝑥 |
6 | 5 | crn 5585 |
. . . . 5
class ran 𝑥 |
7 | 4, 6 | wcel 2106 |
. . . 4
wff +∞
∈ ran 𝑥 |
8 | | vy |
. . . . . . 7
setvar 𝑦 |
9 | 5 | cdm 5584 |
. . . . . . . . 9
class dom 𝑥 |
10 | 9 | cpw 4533 |
. . . . . . . 8
class 𝒫
dom 𝑥 |
11 | | cfn 8720 |
. . . . . . . 8
class
Fin |
12 | 10, 11 | cin 3885 |
. . . . . . 7
class
(𝒫 dom 𝑥
∩ Fin) |
13 | 8 | cv 1538 |
. . . . . . . 8
class 𝑦 |
14 | | vw |
. . . . . . . . . 10
setvar 𝑤 |
15 | 14 | cv 1538 |
. . . . . . . . 9
class 𝑤 |
16 | 15, 5 | cfv 6426 |
. . . . . . . 8
class (𝑥‘𝑤) |
17 | 13, 16, 14 | csu 15407 |
. . . . . . 7
class
Σ𝑤 ∈
𝑦 (𝑥‘𝑤) |
18 | 8, 12, 17 | cmpt 5156 |
. . . . . 6
class (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) |
19 | 18 | crn 5585 |
. . . . 5
class ran
(𝑦 ∈ (𝒫 dom
𝑥 ∩ Fin) ↦
Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)) |
20 | | cxr 11018 |
. . . . 5
class
ℝ* |
21 | | clt 11019 |
. . . . 5
class
< |
22 | 19, 20, 21 | csup 9186 |
. . . 4
class sup(ran
(𝑦 ∈ (𝒫 dom
𝑥 ∩ Fin) ↦
Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, <
) |
23 | 7, 4, 22 | cif 4459 |
. . 3
class
if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, <
)) |
24 | 2, 3, 23 | cmpt 5156 |
. 2
class (𝑥 ∈ V ↦ if(+∞
∈ ran 𝑥, +∞,
sup(ran (𝑦 ∈
(𝒫 dom 𝑥 ∩ Fin)
↦ Σ𝑤 ∈
𝑦 (𝑥‘𝑤)), ℝ*, <
))) |
25 | 1, 24 | wceq 1539 |
1
wff
Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran
𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, <
))) |