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	$$⊢\phi \to M\in \mathrm{Meas}$$
	meacl.2	$$⊢S=\mathrm{dom}M$$
	meacl.3	$$⊢\phi \to A\in S$$
Assertion	meacl	$$⊢\phi \to M\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$

Proof

Step	Hyp	Ref	Expression
1		meacl.1	$$⊢\phi \to M\in \mathrm{Meas}$$
2		meacl.2	$$⊢S=\mathrm{dom}M$$
3		meacl.3	$$⊢\phi \to A\in S$$
4	1 2	meaf	$$⊢\phi \to M:S⟶\left[0,\mathrm{+\infty }\right]$$
5	4 3	ffvelrnd	$$⊢\phi \to M\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$