Definition df-sumge0 41518

Description: Define the arbitrary sum of nonnegative extended reals. (Contributed by Glauco Siliprandi, 17-Aug-2020.) $.

Assertion

Ref	Expression
df-sumge0	⊢ Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < )))

Distinct variable group:   𝑥,𝑤,𝑦

Detailed syntax breakdown of Definition df-sumge0

Step	Hyp	Ref	Expression
1		csumge0 41517	. 2 class Σ^
2		vx	. . 3 setvar 𝑥
3		cvv 3398	. . 3 class V
4		cpnf 10410	. . . . 5 class +∞
5	2	cv 1600	. . . . . 6 class 𝑥
6	5	crn 5358	. . . . 5 class ran 𝑥
7	4, 6	wcel 2107	. . . 4 wff +∞ ∈ ran 𝑥
8		vy	. . . . . . 7 setvar 𝑦
9	5	cdm 5357	. . . . . . . . 9 class dom 𝑥
10	9	cpw 4379	. . . . . . . 8 class 𝒫 dom 𝑥
11		cfn 8243	. . . . . . . 8 class Fin
12	10, 11	cin 3791	. . . . . . 7 class (𝒫 dom 𝑥 ∩ Fin)
13	8	cv 1600	. . . . . . . 8 class 𝑦
14		vw	. . . . . . . . . 10 setvar 𝑤
15	14	cv 1600	. . . . . . . . 9 class 𝑤
16	15, 5	cfv 6137	. . . . . . . 8 class (𝑥‘𝑤)
17	13, 16, 14	csu 14833	. . . . . . 7 class Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)
18	8, 12, 17	cmpt 4967	. . . . . 6 class (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤))
19	18	crn 5358	. . . . 5 class ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤))
20		cxr 10412	. . . . 5 class ℝ*
21		clt 10413	. . . . 5 class <
22	19, 20, 21	csup 8636	. . . 4 class sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < )
23	7, 4, 22	cif 4307	. . 3 class if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < ))
24	2, 3, 23	cmpt 4967	. 2 class (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < )))
25	1, 24	wceq 1601	1 wff Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < )))

This definition is referenced by:  sge0val  41521