Definition df-sumge0 40580

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

Assertion

Ref	Expression
df-sumge0	|- Σ^ = ( x e. _V |-> if ( +oo e. ran x , +oo , sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) ) )

Distinct variable group:   x, w, y

Detailed syntax breakdown of Definition df-sumge0

Step	Hyp	Ref	Expression
1		csumge0 40579	. 2 class Σ^
2		vx	. . 3 setvar x
3		cvv 3200	. . 3 class _V
4		cpnf 10071	. . . . 5 class +oo
5	2	cv 1482	. . . . . 6 class x
6	5	crn 5115	. . . . 5 class ran x
7	4, 6	wcel 1990	. . . 4 wff +oo e. ran x
8		vy	. . . . . . 7 setvar y
9	5	cdm 5114	. . . . . . . . 9 class dom x
10	9	cpw 4158	. . . . . . . 8 class ~P dom x
11		cfn 7955	. . . . . . . 8 class Fin
12	10, 11	cin 3573	. . . . . . 7 class ( ~P dom x i^i Fin )
13	8	cv 1482	. . . . . . . 8 class y
14		vw	. . . . . . . . . 10 setvar w
15	14	cv 1482	. . . . . . . . 9 class w
16	15, 5	cfv 5888	. . . . . . . 8 class ( x ` w )
17	13, 16, 14	csu 14416	. . . . . . 7 class sum_ w e. y ( x ` w )
18	8, 12, 17	cmpt 4729	. . . . . 6 class ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) )
19	18	crn 5115	. . . . 5 class ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) )
20		cxr 10073	. . . . 5 class RR*
21		clt 10074	. . . . 5 class <
22	19, 20, 21	csup 8346	. . . 4 class sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < )
23	7, 4, 22	cif 4086	. . 3 class if ( +oo e. ran x , +oo , sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) )
24	2, 3, 23	cmpt 4729	. 2 class ( x e. _V |-> if ( +oo e. ran x , +oo , sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) ) )
25	1, 24	wceq 1483	1 wff Σ^ = ( x e. _V |-> if ( +oo e. ran x , +oo , sup ( ran ( y e. ( ~P dom x i^i Fin ) |-> sum_ w e. y ( x ` w ) ) , RR* , < ) ) )

This definition is referenced by:  sge0val  40583