Theorem meaunle

Description: The measure of the union of two sets is less than or equal to the sum of the measures, Property 112C (c) of Fremlin1 p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	meaunle.1	⊢ ( 𝜑 → 𝑀 ∈ Meas )
	meaunle.2	⊢ 𝑆 = dom 𝑀
	meaunle.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
	meaunle.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
Assertion	meaunle	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		meaunle.1	⊢ ( 𝜑 → 𝑀 ∈ Meas )
2		meaunle.2	⊢ 𝑆 = dom 𝑀
3		meaunle.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑆 )
4		meaunle.4	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
5		undif2	⊢ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = ( 𝐴 ∪ 𝐵 )
6	5	eqcomi	⊢ ( 𝐴 ∪ 𝐵 ) = ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) )
7	6	fveq2i	⊢ ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( 𝑀 ‘ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) )
8	7	a1i	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( 𝑀 ‘ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ) )
9	1 2	dmmeasal	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
10		saldifcl2	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐵 ∈ 𝑆 ∧ 𝐴 ∈ 𝑆 ) → ( 𝐵 ∖ 𝐴 ) ∈ 𝑆 )
11	9 4 3 10	syl3anc	⊢ ( 𝜑 → ( 𝐵 ∖ 𝐴 ) ∈ 𝑆 )
12		disjdif	⊢ ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅
13	12	a1i	⊢ ( 𝜑 → ( 𝐴 ∩ ( 𝐵 ∖ 𝐴 ) ) = ∅ )
14	1 2 3 11 13	meadjun	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) ) = ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
15	8 14	eqtrd	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) = ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ) )
16	1 2 11	meaxrcl	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ∈ ℝ* )
17	1 2 4	meaxrcl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐵 ) ∈ ℝ* )
18	1 2 3	meaxrcl	⊢ ( 𝜑 → ( 𝑀 ‘ 𝐴 ) ∈ ℝ* )
19		difssd	⊢ ( 𝜑 → ( 𝐵 ∖ 𝐴 ) ⊆ 𝐵 )
20	1 2 11 4 19	meassle	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ≤ ( 𝑀 ‘ 𝐵 ) )
21	16 17 18 20	xleadd2d	⊢ ( 𝜑 → ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ ( 𝐵 ∖ 𝐴 ) ) ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) )
22	15 21	eqbrtrd	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝐴 ∪ 𝐵 ) ) ≤ ( ( 𝑀 ‘ 𝐴 ) +𝑒 ( 𝑀 ‘ 𝐵 ) ) )