Theorem sge0nemnf

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

	Ref	Expression
Hypotheses	sge0nemnf.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	sge0nemnf.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
Assertion	sge0nemnf	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ≠ -∞ )

Proof

Step	Hyp	Ref	Expression
1		sge0nemnf.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2		sge0nemnf.2	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ( 0 [,] +∞ ) )
3	1 2	sge0cl	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) )
4		xrge0neqmnf	⊢ ( ( Σ^ ‘ 𝐹 ) ∈ ( 0 [,] +∞ ) → ( Σ^ ‘ 𝐹 ) ≠ -∞ )
5	3 4	syl	⊢ ( 𝜑 → ( Σ^ ‘ 𝐹 ) ≠ -∞ )