Theorem sge0pnfmpt

Description: If a term in the sum of nonnegative extended reals is +oo , then the value of the sum is +oo . (Contributed by Glauco Siliprandi, 3-Mar-2021)

	Ref	Expression
Hypotheses	sge0pnfmpt.k	$$⊢Ⅎk\phi$$
	sge0pnfmpt.a	$$⊢\phi \to A\in V$$
	sge0pnfmpt.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
	sge0pnfmpt.p	$$⊢\phi \to \exists k\in AB=\mathrm{+\infty }$$
Assertion	sge0pnfmpt	$$⊢\phi \to \mathrm{sum^}\left(\left(k\in A⟼B\right)\right)=\mathrm{+\infty }$$

Proof

Step	Hyp	Ref	Expression
1		sge0pnfmpt.k	$$⊢Ⅎk\phi$$
2		sge0pnfmpt.a	$$⊢\phi \to A\in V$$
3		sge0pnfmpt.b	$$⊢\left(\phi \wedge k\in A\right)\to B\in \left[0,\mathrm{+\infty }\right]$$
4		sge0pnfmpt.p	$$⊢\phi \to \exists k\in AB=\mathrm{+\infty }$$
5		eqid	$$⊢\left(k\in A⟼B\right)=\left(k\in A⟼B\right)$$
6	1 3 5	fmptdf	$$⊢\phi \to \left(k\in A⟼B\right):A⟶\left[0,\mathrm{+\infty }\right]$$
7		eqcom	$$⊢B=\mathrm{+\infty }\leftrightarrow \mathrm{+\infty }=B$$
8	7	rexbii	$$⊢\exists k\in AB=\mathrm{+\infty }\leftrightarrow \exists k\in A\mathrm{+\infty }=B$$
9	4 8	sylib	$$⊢\phi \to \exists k\in A\mathrm{+\infty }=B$$
10		pnfex	$$⊢\mathrm{+\infty }\in \mathrm{V}$$
11	10	a1i	$$⊢\phi \to \mathrm{+\infty }\in \mathrm{V}$$
12	5 9 11	elrnmptd	$$⊢\phi \to \mathrm{+\infty }\in \mathrm{ran}\left(k\in A⟼B\right)$$
13	2 6 12	sge0pnfval	$$⊢\phi \to \mathrm{sum^}\left(\left(k\in A⟼B\right)\right)=\mathrm{+\infty }$$