Theorem measvxrge0

Description: The values of a measure are positive extended reals. (Contributed by Thierry Arnoux, 26-Dec-2016)

	Ref	Expression
Assertion	measvxrge0	⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		measfrge0	⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
2	1	ffvelrnda	⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴 ∈ 𝑆 ) → ( 𝑀 ‘ 𝐴 ) ∈ ( 0 [,] +∞ ) )