Theorem sge0vald

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

	Ref	Expression
Hypotheses	sge0vald.x	$$⊢\phi \to X\in V$$
	sge0vald.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
Assertion	sge0vald	$$⊢\phi \to \mathrm{sum^}\left(F\right)=if\left(\mathrm{+\infty }\in \mathrm{ran}F,\mathrm{+\infty },sup\left(\mathrm{ran}\left(x\in \left(𝒫X\cap \mathrm{Fin}\right)⟼\sum _{y\in x}F\left(y\right)\right),{ℝ}^{*},<\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sge0vald.x	$$⊢\phi \to X\in V$$
2		sge0vald.f	$$⊢\phi \to F:X⟶\left[0,\mathrm{+\infty }\right]$$
3		sge0val	$$⊢\left(X\in V\wedge F:X⟶\left[0,\mathrm{+\infty }\right]\right)\to \mathrm{sum^}\left(F\right)=if\left(\mathrm{+\infty }\in \mathrm{ran}F,\mathrm{+\infty },sup\left(\mathrm{ran}\left(x\in \left(𝒫X\cap \mathrm{Fin}\right)⟼\sum _{y\in x}F\left(y\right)\right),{ℝ}^{*},<\right)\right)$$
4	1 2 3	syl2anc	$$⊢\phi \to \mathrm{sum^}\left(F\right)=if\left(\mathrm{+\infty }\in \mathrm{ran}F,\mathrm{+\infty },sup\left(\mathrm{ran}\left(x\in \left(𝒫X\cap \mathrm{Fin}\right)⟼\sum _{y\in x}F\left(y\right)\right),{ℝ}^{*},<\right)\right)$$