Theorem meacl

Description: The measure of a set is a nonnegative extended real. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	meacl.1	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meacl.2	⊢ 𝑆 = dom 𝑀
	meacl.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
Assertion	meacl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		meacl.1	⊢ ( 𝜑 → 𝑀 ∈ Meas )
2		meacl.2	⊢ 𝑆 = dom 𝑀
3		meacl.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
4	1 2	meaf	⊢ ( 𝜑 → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
5	4 3	ffvelrnd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )