Theorem sge0xrclmpt

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

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

Proof

Step	Hyp	Ref	Expression
1		sge0xrclmpt.xph	$$⊢Ⅎx\phi$$
2		sge0xrclmpt.a	$$⊢\phi \to A\in V$$
3		sge0xrclmpt.b	$$⊢\left(\phi \wedge x\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
4		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
5	1 2 3	sge0clmpt	$$⊢\phi \to \mathrm{sum^}\left(\left(x\in A⟼B\right)\right)\in \left[0,\mathrm{+\infty }\right]$$
6	4 5	sselid	$$⊢\phi \to \mathrm{sum^}\left(\left(x\in A⟼B\right)\right)\in {ℝ}^{*}$$