Definition df-sumge0 43791

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 43790	. 2 class Σ^
2		vx	. . 3 setvar 𝑥
3		cvv 3422	. . 3 class V
4		cpnf 10937	. . . . 5 class +∞
5	2	cv 1538	. . . . . 6 class 𝑥
6	5	crn 5581	. . . . 5 class ran 𝑥
7	4, 6	wcel 2108	. . . 4 wff +∞ ∈ ran 𝑥
8		vy	. . . . . . 7 setvar 𝑦
9	5	cdm 5580	. . . . . . . . 9 class dom 𝑥
10	9	cpw 4530	. . . . . . . 8 class 𝒫 dom 𝑥
11		cfn 8691	. . . . . . . 8 class Fin
12	10, 11	cin 3882	. . . . . . 7 class (𝒫 dom 𝑥 ∩ Fin)
13	8	cv 1538	. . . . . . . 8 class 𝑦
14		vw	. . . . . . . . . 10 setvar 𝑤
15	14	cv 1538	. . . . . . . . 9 class 𝑤
16	15, 5	cfv 6418	. . . . . . . 8 class (𝑥‘𝑤)
17	13, 16, 14	csu 15325	. . . . . . 7 class Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)
18	8, 12, 17	cmpt 5153	. . . . . 6 class (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤))
19	18	crn 5581	. . . . 5 class ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤))
20		cxr 10939	. . . . 5 class ℝ*
21		clt 10940	. . . . 5 class <
22	19, 20, 21	csup 9129	. . . 4 class sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < )
23	7, 4, 22	cif 4456	. . 3 class if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < ))
24	2, 3, 23	cmpt 5153	. 2 class (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < )))
25	1, 24	wceq 1539	1 wff Σ^ = (𝑥 ∈ V ↦ if(+∞ ∈ ran 𝑥, +∞, sup(ran (𝑦 ∈ (𝒫 dom 𝑥 ∩ Fin) ↦ Σ𝑤 ∈ 𝑦 (𝑥‘𝑤)), ℝ*, < )))

This definition is referenced by:  sge0val  43794