Theorem meassle

Description: The measure of a set is greater than or equal to the measure of a subset, Property 112C (b) of Fremlin1 p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	meassle.m	|- ( ph -> M e. Meas )
	meassle.x	|- S = dom M
	meassle.a	|- ( ph -> A e. S )
	meassle.b	|- ( ph -> B e. S )
	meassle.ss	|- ( ph -> A C_ B )
Assertion	meassle	|- ( ph -> ( M ` A ) <_ ( M ` B ) )

Proof

Step	Hyp	Ref	Expression
1		meassle.m	|- ( ph -> M e. Meas )
2		meassle.x	|- S = dom M
3		meassle.a	|- ( ph -> A e. S )
4		meassle.b	|- ( ph -> B e. S )
5		meassle.ss	|- ( ph -> A C_ B )
6	1 2 3	meaxrcl	|- ( ph -> ( M ` A ) e. RR* )
7	1 2	dmmeasal	|- ( ph -> S e. SAlg )
8		saldifcl2	|- ( ( S e. SAlg /\ B e. S /\ A e. S ) -> ( B \ A ) e. S )
9	7 4 3 8	syl3anc	|- ( ph -> ( B \ A ) e. S )
10	1 2 9	meacl	|- ( ph -> ( M ` ( B \ A ) ) e. ( 0 [,] +oo ) )
11	6 10	xadd0ge	|- ( ph -> ( M ` A ) <_ ( ( M ` A ) +e ( M ` ( B \ A ) ) ) )
12		undif	|- ( A C_ B <-> ( A u. ( B \ A ) ) = B )
13	12	biimpi	|- ( A C_ B -> ( A u. ( B \ A ) ) = B )
14	5 13	syl	|- ( ph -> ( A u. ( B \ A ) ) = B )
15	14	fveq2d	|- ( ph -> ( M ` ( A u. ( B \ A ) ) ) = ( M ` B ) )
16	15	eqcomd	|- ( ph -> ( M ` B ) = ( M ` ( A u. ( B \ A ) ) ) )
17		disjdif	|- ( A i^i ( B \ A ) ) = (/)
18	17	a1i	|- ( ph -> ( A i^i ( B \ A ) ) = (/) )
19	1 2 3 9 18	meadjun	|- ( ph -> ( M ` ( A u. ( B \ A ) ) ) = ( ( M ` A ) +e ( M ` ( B \ A ) ) ) )
20	16 19	eqtr2d	|- ( ph -> ( ( M ` A ) +e ( M ` ( B \ A ) ) ) = ( M ` B ) )
21	11 20	breqtrd	|- ( ph -> ( M ` A ) <_ ( M ` B ) )