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	|- ( ph -> M e. Meas )
	meassre.a	|- ( ph -> A e. dom M )
	meassre.r	|- ( ph -> ( M ` A ) e. RR )
	meassre.s	|- ( ph -> B C_ A )
	meassre.b	|- ( ph -> B e. dom M )
Assertion	meassre	|- ( ph -> ( M ` B ) e. RR )

Proof

Step	Hyp	Ref	Expression
1		meassre.m	|- ( ph -> M e. Meas )
2		meassre.a	|- ( ph -> A e. dom M )
3		meassre.r	|- ( ph -> ( M ` A ) e. RR )
4		meassre.s	|- ( ph -> B C_ A )
5		meassre.b	|- ( ph -> B e. dom M )
6		rge0ssre	|- ( 0 [,) +oo ) C_ RR
7		0xr	|- 0 e. RR*
8	7	a1i	|- ( ph -> 0 e. RR* )
9		pnfxr	|- +oo e. RR*
10	9	a1i	|- ( ph -> +oo e. RR* )
11		eqid	|- dom M = dom M
12	1 11 5	meaxrcl	|- ( ph -> ( M ` B ) e. RR* )
13	1 5	meage0	|- ( ph -> 0 <_ ( M ` B ) )
14	3	rexrd	|- ( ph -> ( M ` A ) e. RR* )
15	1 11 5 2 4	meassle	|- ( ph -> ( M ` B ) <_ ( M ` A ) )
16	3	ltpnfd	|- ( ph -> ( M ` A ) < +oo )
17	12 14 10 15 16	xrlelttrd	|- ( ph -> ( M ` B ) < +oo )
18	8 10 12 13 17	elicod	|- ( ph -> ( M ` B ) e. ( 0 [,) +oo ) )
19	6 18	sselid	|- ( ph -> ( M ` B ) e. RR )