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	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meassre.a	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑀 )
	meassre.r	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ )
	meassre.s	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
	meassre.b	⊢ ( 𝜑 → 𝐵 ∈ dom 𝑀 )
Assertion	meassre	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		meassre.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
2		meassre.a	⊢ ( 𝜑 → 𝐴 ∈ dom 𝑀 )
3		meassre.r	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ )
4		meassre.s	⊢ ( 𝜑 → 𝐵 ⊆ 𝐴 )
5		meassre.b	⊢ ( 𝜑 → 𝐵 ∈ dom 𝑀 )
6		rge0ssre	⊢ ( 0 [,) +∞ ) ⊆ ℝ
7		0xr	⊢ 0 ∈ ℝ*
8	7	a1i	⊢ ( 𝜑 → 0 ∈ ℝ* )
9		pnfxr	⊢ +∞ ∈ ℝ*
10	9	a1i	⊢ ( 𝜑 → +∞ ∈ ℝ* )
11		eqid	⊢ dom 𝑀 = dom 𝑀
12	1 11 5	meaxrcl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ ℝ* )
13	1 5	meage0	⊢ ( 𝜑 → 0 ≤ ( 𝑀 ‘ 𝐵 ) )
14	3	rexrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ* )
15	1 11 5 2 4	meassle	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ≤ ( 𝑀 ‘ 𝐴 ) )
16	3	ltpnfd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) < +∞ )
17	12 14 10 15 16	xrlelttrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) < +∞ )
18	8 10 12 13 17	elicod	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ ( 0 [,) +∞ ) )
19	6 18	sselid	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ ℝ )