Theorem sge0clmpt

Description: The generalized sum of nonnegative extended reals is a nonnegative extended real. (Contributed by Glauco Siliprandi, 11-Oct-2020)

	Ref	Expression
Hypotheses	sge0clmpt.xph	$$⊢Ⅎx\phi$$
	sge0clmpt.a	$$⊢\phi \to A\in V$$
	sge0clmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
Assertion	sge0clmpt	$$⊢\phi \to \mathrm{sum^}\left(\left(x\in A⟼B\right)\right)\in \left[0,\mathrm{+\infty }\right]$$

Proof

Step	Hyp	Ref	Expression
1		sge0clmpt.xph	$$⊢Ⅎx\phi$$
2		sge0clmpt.a	$$⊢\phi \to A\in V$$
3		sge0clmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
4		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
5	1 3 4	fmptdf	$$⊢\phi \to \left(x\in A⟼B\right):A⟶\left[0,\mathrm{+\infty }\right]$$
6	2 5	sge0cl	$$⊢\phi \to \mathrm{sum^}\left(\left(x\in A⟼B\right)\right)\in \left[0,\mathrm{+\infty }\right]$$