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	$$⊢\phi \to M\in \mathrm{Meas}$$
	meassle.x	$$⊢S=\mathrm{dom}M$$
	meassle.a	$$⊢\phi \to A\in S$$
	meassle.b	$$⊢\phi \to B\in S$$
	meassle.ss	$$⊢\phi \to A\subseteq B$$
Assertion	meassle	$$⊢\phi \to M\left(A\right)\le M\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		meassle.m	$$⊢\phi \to M\in \mathrm{Meas}$$
2		meassle.x	$$⊢S=\mathrm{dom}M$$
3		meassle.a	$$⊢\phi \to A\in S$$
4		meassle.b	$$⊢\phi \to B\in S$$
5		meassle.ss	$$⊢\phi \to A\subseteq B$$
6	1 2 3	meaxrcl	$$⊢\phi \to M\left(A\right)\in {ℝ}^{*}$$
7	1 2	dmmeasal	$$⊢\phi \to S\in \mathrm{SAlg}$$
8		saldifcl2	$$⊢\left(S\in \mathrm{SAlg}\wedge B\in S\wedge A\in S\right)\to B\setminus A\in S$$
9	7 4 3 8	syl3anc	$$⊢\phi \to B\setminus A\in S$$
10	1 2 9	meacl	$$⊢\phi \to M\left(B\setminus A\right)\in \left[0,\mathrm{+\infty }\right]$$
11	6 10	xadd0ge	$$⊢\phi \to M\left(A\right)\le M\left(A\right){+}_{𝑒}M\left(B\setminus A\right)$$
12		undif	$$⊢A\subseteq B\leftrightarrow A\cup \left(B\setminus A\right)=B$$
13	12	biimpi	$$⊢A\subseteq B\to A\cup \left(B\setminus A\right)=B$$
14	5 13	syl	$$⊢\phi \to A\cup \left(B\setminus A\right)=B$$
15	14	fveq2d	$$⊢\phi \to M\left(A\cup \left(B\setminus A\right)\right)=M\left(B\right)$$
16	15	eqcomd	$$⊢\phi \to M\left(B\right)=M\left(A\cup \left(B\setminus A\right)\right)$$
17		disjdif	$$⊢A\cap \left(B\setminus A\right)=\varnothing$$
18	17	a1i	$$⊢\phi \to A\cap \left(B\setminus A\right)=\varnothing$$
19	1 2 3 9 18	meadjun	$$⊢\phi \to M\left(A\cup \left(B\setminus A\right)\right)=M\left(A\right){+}_{𝑒}M\left(B\setminus A\right)$$
20	16 19	eqtr2d	$$⊢\phi \to M\left(A\right){+}_{𝑒}M\left(B\setminus A\right)=M\left(B\right)$$
21	11 20	breqtrd	$$⊢\phi \to M\left(A\right)\le M\left(B\right)$$