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	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meassle.x	⊢ 𝑆 = dom 𝑀
	meassle.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	meassle.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
	meassle.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
Assertion	meassle	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		meassle.m	⊢ ( 𝜑 → 𝑀 ∈ Meas )
2		meassle.x	⊢ 𝑆 = dom 𝑀
3		meassle.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
4		meassle.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
5		meassle.ss	⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
6	1 2 3	meaxrcl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ* )
7	1 2	dmmeasal	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
8		saldifcl2	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( 𝐵 ∖ 𝐴 ) ∈ 𝑆 )
9	7 4 3 8	syl3anc	⊢ ( 𝜑 → ( 𝐵 ∖ 𝐴 ) ∈ 𝑆 )
10	1 2 9	meacl	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ∈ ( 0 [,] +∞ ) )
11	6 10	xadd0ge	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
12		undif	⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
13	12	biimpi	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
14	5 13	syl	⊢ ( 𝜑 → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
15	14	fveq2d	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝐵 ) )
16	15	eqcomd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) = ( 𝑀 ‘ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ) )
17		disjdif	⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
18	17	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅ )
19	1 2 3 9 18	meadjun	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
20	16 19	eqtr2d	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ) = ( 𝑀 ‘ 𝐵 ) )
21	11 20	breqtrd	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ≤ ( 𝑀 ‘ 𝐵 ) )