df-sumge0

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

		Ref	Expression
	Assertion	df-sumge0	$⊢ sum^= (x \in V ⟼ if (+∞ \in ran x, +∞, sup (ran (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w)) ℝ^{*} <)))$

Step	Hyp	Ref	Expression
0		csumge0	$class sum^$
1		vx	$setvar x$
2		cvv	$class V$
3		cpnf	$class +∞$
4	1	cv	$setvar x$
5	4	crn	$class ran x$
6	3 5	wcel	$wff +∞ \in ran x$
7		vy	$setvar y$
8	4	cdm	$class dom x$
9	8	cpw	$class 𝒫 dom x$
10		cfn	$class Fin$
11	9 10	cin	$class (𝒫 dom x \cap Fin)$
12		vw	$setvar w$
13	7	cv	$setvar y$
14	12	cv	$setvar w$
15	14 4	cfv	$class x (w)$
16	13 15 12	csu	$class \sum_{w \in y} x (w)$
17	7 11 16	cmpt	$class (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w))$
18	17	crn	$class ran (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w))$
19		cxr	$class ℝ^{*}$
20		clt	$class <$
21	18 19 20	csup	$class sup (ran (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w)) ℝ^{*} <)$
22	6 3 21	cif	$class if (+∞ \in ran x, +∞, sup (ran (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w)) ℝ^{*} <))$
23	1 2 22	cmpt	$class (x \in V ⟼ if (+∞ \in ran x, +∞, sup (ran (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w)) ℝ^{*} <)))$
24	0 23	wceq	$wff sum^= (x \in V ⟼ if (+∞ \in ran x, +∞, sup (ran (y \in (𝒫 dom x \cap Fin) ⟼ \sum_{w \in y} x (w)) ℝ^{*} <)))$

Metamath Proof Explorer