Theorem measssd

Description: A measure is monotone with respect to set inclusion. (Contributed by Thierry Arnoux, 28-Dec-2016)

	Ref	Expression
Hypotheses	measssd.1	$$⊢\phi \to M\in \mathrm{measures}\left(S\right)$$
	measssd.2	$$⊢\phi \to A\in S$$
	measssd.3	$$⊢\phi \to B\in S$$
	measssd.4	$$⊢\phi \to A\subseteq B$$
Assertion	measssd	$$⊢\phi \to M\left(A\right)\le M\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		measssd.1	$$⊢\phi \to M\in \mathrm{measures}\left(S\right)$$
2		measssd.2	$$⊢\phi \to A\in S$$
3		measssd.3	$$⊢\phi \to B\in S$$
4		measssd.4	$$⊢\phi \to A\subseteq B$$
5		measbase	$$⊢M\in \mathrm{measures}\left(S\right)\to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
6	1 5	syl	$$⊢\phi \to S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}$$
7		difelsiga	$$⊢\left(S\in \bigcup \mathrm{ran}\mathrm{sigAlgebra}\wedge B\in S\wedge A\in S\right)\to B\setminus A\in S$$
8	6 3 2 7	syl3anc	$$⊢\phi \to B\setminus A\in S$$
9		measvxrge0	$$⊢\left(M\in \mathrm{measures}\left(S\right)\wedge B\setminus A\in S\right)\to M\left(B\setminus A\right)\in \left[0,\mathrm{+\infty }\right]$$
10	1 8 9	syl2anc	$$⊢\phi \to M\left(B\setminus A\right)\in \left[0,\mathrm{+\infty }\right]$$
11		elxrge0	$$⊢M\left(B\setminus A\right)\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(M\left(B\setminus A\right)\in {ℝ}^{*}\wedge 0\le M\left(B\setminus A\right)\right)$$
12	11	simprbi	$$⊢M\left(B\setminus A\right)\in \left[0,\mathrm{+\infty }\right]\to 0\le M\left(B\setminus A\right)$$
13	10 12	syl	$$⊢\phi \to 0\le M\left(B\setminus A\right)$$
14		measvxrge0	$$⊢\left(M\in \mathrm{measures}\left(S\right)\wedge A\in S\right)\to M\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$
15	1 2 14	syl2anc	$$⊢\phi \to M\left(A\right)\in \left[0,\mathrm{+\infty }\right]$$
16		elxrge0	$$⊢M\left(A\right)\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(M\left(A\right)\in {ℝ}^{*}\wedge 0\le M\left(A\right)\right)$$
17	16	simplbi	$$⊢M\left(A\right)\in \left[0,\mathrm{+\infty }\right]\to M\left(A\right)\in {ℝ}^{*}$$
18	15 17	syl	$$⊢\phi \to M\left(A\right)\in {ℝ}^{*}$$
19	11	simplbi	$$⊢M\left(B\setminus A\right)\in \left[0,\mathrm{+\infty }\right]\to M\left(B\setminus A\right)\in {ℝ}^{*}$$
20	10 19	syl	$$⊢\phi \to M\left(B\setminus A\right)\in {ℝ}^{*}$$
21		xraddge02	$$⊢\left(M\left(A\right)\in {ℝ}^{*}\wedge M\left(B\setminus A\right)\in {ℝ}^{*}\right)\to \left(0\le M\left(B\setminus A\right)\to M\left(A\right)\le M\left(A\right){+}_{𝑒}M\left(B\setminus A\right)\right)$$
22	18 20 21	syl2anc	$$⊢\phi \to \left(0\le M\left(B\setminus A\right)\to M\left(A\right)\le M\left(A\right){+}_{𝑒}M\left(B\setminus A\right)\right)$$
23	13 22	mpd	$$⊢\phi \to M\left(A\right)\le M\left(A\right){+}_{𝑒}M\left(B\setminus A\right)$$
24		prssi	$$⊢\left(A\in S\wedge B\setminus A\in S\right)\to \left\{A,B\setminus A\right\}\subseteq S$$
25	2 8 24	syl2anc	$$⊢\phi \to \left\{A,B\setminus A\right\}\subseteq S$$
26		prex	$$⊢\left\{A,B\setminus A\right\}\in \mathrm{V}$$
27	26	elpw	$$⊢\left\{A,B\setminus A\right\}\in 𝒫S\leftrightarrow \left\{A,B\setminus A\right\}\subseteq S$$
28	25 27	sylibr	$$⊢\phi \to \left\{A,B\setminus A\right\}\in 𝒫S$$
29		prct	$$⊢\left(A\in S\wedge B\setminus A\in S\right)\to \left\{A,B\setminus A\right\}\preccurlyeq \mathrm{\omega }$$
30	2 8 29	syl2anc	$$⊢\phi \to \left\{A,B\setminus A\right\}\preccurlyeq \mathrm{\omega }$$
31		disjdifprg	$$⊢\left(A\in S\wedge B\in S\right)\to \underset{y\in \left\{B\setminus A,A\right\}}{Disj}y$$
32	2 3 31	syl2anc	$$⊢\phi \to \underset{y\in \left\{B\setminus A,A\right\}}{Disj}y$$
33		prcom	$$⊢\left\{B\setminus A,A\right\}=\left\{A,B\setminus A\right\}$$
34	33	a1i	$$⊢\phi \to \left\{B\setminus A,A\right\}=\left\{A,B\setminus A\right\}$$
35	34	disjeq1d	$$⊢\phi \to \left(\underset{y\in \left\{B\setminus A,A\right\}}{Disj}y\leftrightarrow \underset{y\in \left\{A,B\setminus A\right\}}{Disj}y\right)$$
36	32 35	mpbid	$$⊢\phi \to \underset{y\in \left\{A,B\setminus A\right\}}{Disj}y$$
37		measvun	$$⊢\left(M\in \mathrm{measures}\left(S\right)\wedge \left\{A,B\setminus A\right\}\in 𝒫S\wedge \left(\left\{A,B\setminus A\right\}\preccurlyeq \mathrm{\omega }\wedge \underset{y\in \left\{A,B\setminus A\right\}}{Disj}y\right)\right)\to M\left(\bigcup \left\{A,B\setminus A\right\}\right)=\underset{y\in \left\{A,B\setminus A\right\}}{{\sum }^{*}}M\left(y\right)$$
38	1 28 30 36 37	syl112anc	$$⊢\phi \to M\left(\bigcup \left\{A,B\setminus A\right\}\right)=\underset{y\in \left\{A,B\setminus A\right\}}{{\sum }^{*}}M\left(y\right)$$
39		uniprg	$$⊢\left(A\in S\wedge B\setminus A\in S\right)\to \bigcup \left\{A,B\setminus A\right\}=A\cup \left(B\setminus A\right)$$
40	2 8 39	syl2anc	$$⊢\phi \to \bigcup \left\{A,B\setminus A\right\}=A\cup \left(B\setminus A\right)$$
41		undif	$$⊢A\subseteq B\leftrightarrow A\cup \left(B\setminus A\right)=B$$
42	4 41	sylib	$$⊢\phi \to A\cup \left(B\setminus A\right)=B$$
43	40 42	eqtrd	$$⊢\phi \to \bigcup \left\{A,B\setminus A\right\}=B$$
44	43	fveq2d	$$⊢\phi \to M\left(\bigcup \left\{A,B\setminus A\right\}\right)=M\left(B\right)$$
45		fveq2	$$⊢y=A\to M\left(y\right)=M\left(A\right)$$
46	45	adantl	$$⊢\left(\phi \wedge y=A\right)\to M\left(y\right)=M\left(A\right)$$
47		fveq2	$$⊢y=B\setminus A\to M\left(y\right)=M\left(B\setminus A\right)$$
48	47	adantl	$$⊢\left(\phi \wedge y=B\setminus A\right)\to M\left(y\right)=M\left(B\setminus A\right)$$
49		eqimss	$$⊢A=B\setminus A\to A\subseteq B\setminus A$$
50		ssdifeq0	$$⊢A\subseteq B\setminus A\leftrightarrow A=\varnothing$$
51	49 50	sylib	$$⊢A=B\setminus A\to A=\varnothing$$
52	51	adantl	$$⊢\left(\phi \wedge A=B\setminus A\right)\to A=\varnothing$$
53	52	fveq2d	$$⊢\left(\phi \wedge A=B\setminus A\right)\to M\left(A\right)=M\left(\varnothing \right)$$
54		measvnul	$$⊢M\in \mathrm{measures}\left(S\right)\to M\left(\varnothing \right)=0$$
55	1 54	syl	$$⊢\phi \to M\left(\varnothing \right)=0$$
56	55	adantr	$$⊢\left(\phi \wedge A=B\setminus A\right)\to M\left(\varnothing \right)=0$$
57	53 56	eqtrd	$$⊢\left(\phi \wedge A=B\setminus A\right)\to M\left(A\right)=0$$
58	57	orcd	$$⊢\left(\phi \wedge A=B\setminus A\right)\to \left(M\left(A\right)=0\vee M\left(A\right)=\mathrm{+\infty }\right)$$
59	58	ex	$$⊢\phi \to \left(A=B\setminus A\to \left(M\left(A\right)=0\vee M\left(A\right)=\mathrm{+\infty }\right)\right)$$
60	46 48 2 8 15 10 59	esumpr2	$$⊢\phi \to \underset{y\in \left\{A,B\setminus A\right\}}{{\sum }^{*}}M\left(y\right)=M\left(A\right){+}_{𝑒}M\left(B\setminus A\right)$$
61	38 44 60	3eqtr3d	$$⊢\phi \to M\left(B\right)=M\left(A\right){+}_{𝑒}M\left(B\setminus A\right)$$
62	23 61	breqtrrd	$$⊢\phi \to M\left(A\right)\le M\left(B\right)$$