Theorem meaxrcl

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

	Ref	Expression
Hypotheses	meaxrcl.1	$$⊢\phi \to M\in \mathrm{Meas}$$
	meaxrcl.2	$$⊢S=\mathrm{dom}M$$
	meaxrcl.3	$$⊢\phi \to A\in S$$
Assertion	meaxrcl	$$⊢\phi \to M\left(A\right)\in {ℝ}^{*}$$

Proof

Step	Hyp	Ref	Expression
1		meaxrcl.1	$$⊢\phi \to M\in \mathrm{Meas}$$
2		meaxrcl.2	$$⊢S=\mathrm{dom}M$$
3		meaxrcl.3	$$⊢\phi \to A\in S$$
4		iccssxr	$$⊢\left[0,\mathrm{+\infty }\right]\subseteq {ℝ}^{*}$$
5	1 2 3	meacl	$$⊢\phi \to M\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$
6	4 5	sseldi	$$⊢\phi \to M\left(A\right)\in {ℝ}^{*}$$