Theorem meassre

Description: If the measure of a measurable set is real, then the measure of any of its measurable subsets is real. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	meassre.m	$$⊢\phi \to M\in \mathrm{Meas}$$
	meassre.a	$$⊢\phi \to A\in \mathrm{dom}M$$
	meassre.r	$$⊢\phi \to M\left(A\right)\in ℝ$$
	meassre.s	$$⊢\phi \to B\subseteq A$$
	meassre.b	$$⊢\phi \to B\in \mathrm{dom}M$$
Assertion	meassre	$$⊢\phi \to M\left(B\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		meassre.m	$$⊢\phi \to M\in \mathrm{Meas}$$
2		meassre.a	$$⊢\phi \to A\in \mathrm{dom}M$$
3		meassre.r	$$⊢\phi \to M\left(A\right)\in ℝ$$
4		meassre.s	$$⊢\phi \to B\subseteq A$$
5		meassre.b	$$⊢\phi \to B\in \mathrm{dom}M$$
6		rge0ssre	$$⊢\left[0,\mathrm{+\infty }\right)\subseteq ℝ$$
7		0xr	$$⊢0\in {ℝ}^{*}$$
8	7	a1i	$$⊢\phi \to 0\in {ℝ}^{*}$$
9		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
10	9	a1i	$$⊢\phi \to \mathrm{+\infty }\in {ℝ}^{*}$$
11		eqid	$$⊢\mathrm{dom}M=\mathrm{dom}M$$
12	1 11 5	meaxrcl	$$⊢\phi \to M\left(B\right)\in {ℝ}^{*}$$
13	1 5	meage0	$$⊢\phi \to 0\le M\left(B\right)$$
14	3	rexrd	$$⊢\phi \to M\left(A\right)\in {ℝ}^{*}$$
15	1 11 5 2 4	meassle	$$⊢\phi \to M\left(B\right)\le M\left(A\right)$$
16	3	ltpnfd	$$⊢\phi \to M\left(A\right)<\mathrm{+\infty }$$
17	12 14 10 15 16	xrlelttrd	$$⊢\phi \to M\left(B\right)<\mathrm{+\infty }$$
18	8 10 12 13 17	elicod	$$⊢\phi \to M\left(B\right)\in \left[0,\mathrm{+\infty }\right)$$
19	6 18	sseldi	$$⊢\phi \to M\left(B\right)\in ℝ$$