Theorem ismbl2

Description: From ovolun , it suffices to show that the measure of x is at least the sum of the measures of x i^i A and x \ A . (Contributed by Mario Carneiro, 15-Jun-2014)

	Ref	Expression
Assertion	ismbl2	$$⊢A\in \mathrm{dom}vol\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ismbl	$$⊢A\in \mathrm{dom}vol\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\right)\right)$$
2		elpwi	$$⊢x\in 𝒫ℝ\to x\subseteq ℝ$$
3		inundif	$$⊢\left(x\cap A\right)\cup \left(x\setminus A\right)=x$$
4	3	fveq2i	$$⊢{vol}^{*}\left(\left(x\cap A\right)\cup \left(x\setminus A\right)\right)={vol}^{*}\left(x\right)$$
5		inss1	$$⊢x\cap A\subseteq x$$
6		simprl	$$⊢\left(A\subseteq ℝ\wedge \left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\right)\to x\subseteq ℝ$$
7	5 6	sstrid	$$⊢\left(A\subseteq ℝ\wedge \left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\right)\to x\cap A\subseteq ℝ$$
8		ovolsscl	$$⊢\left(x\cap A\subseteq x\wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right)\in ℝ$$
9	5 8	mp3an1	$$⊢\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\cap A\right)\in ℝ$$
10	9	adantl	$$⊢\left(A\subseteq ℝ\wedge \left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\right)\to {vol}^{*}\left(x\cap A\right)\in ℝ$$
11		difss	$$⊢x\setminus A\subseteq x$$
12	11 6	sstrid	$$⊢\left(A\subseteq ℝ\wedge \left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\right)\to x\setminus A\subseteq ℝ$$
13		ovolsscl	$$⊢\left(x\setminus A\subseteq x\wedge x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\setminus A\right)\in ℝ$$
14	11 13	mp3an1	$$⊢\left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\to {vol}^{*}\left(x\setminus A\right)\in ℝ$$
15	14	adantl	$$⊢\left(A\subseteq ℝ\wedge \left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\right)\to {vol}^{*}\left(x\setminus A\right)\in ℝ$$
16		ovolun	$$⊢\left(\left(x\cap A\subseteq ℝ\wedge {vol}^{*}\left(x\cap A\right)\in ℝ\right)\wedge \left(x\setminus A\subseteq ℝ\wedge {vol}^{*}\left(x\setminus A\right)\in ℝ\right)\right)\to {vol}^{*}\left(\left(x\cap A\right)\cup \left(x\setminus A\right)\right)\le {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)$$
17	7 10 12 15 16	syl22anc	$$⊢\left(A\subseteq ℝ\wedge \left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\right)\to {vol}^{*}\left(\left(x\cap A\right)\cup \left(x\setminus A\right)\right)\le {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)$$
18	4 17	eqbrtrrid	$$⊢\left(A\subseteq ℝ\wedge \left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\right)\to {vol}^{*}\left(x\right)\le {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)$$
19		simprr	$$⊢\left(A\subseteq ℝ\wedge \left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\right)\to {vol}^{*}\left(x\right)\in ℝ$$
20	10 15	readdcld	$$⊢\left(A\subseteq ℝ\wedge \left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\right)\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\in ℝ$$
21	19 20	letri3d	$$⊢\left(A\subseteq ℝ\wedge \left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\right)\to \left({vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\leftrightarrow \left({vol}^{*}\left(x\right)\le {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\wedge {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)$$
22	18 21	mpbirand	$$⊢\left(A\subseteq ℝ\wedge \left(x\subseteq ℝ\wedge {vol}^{*}\left(x\right)\in ℝ\right)\right)\to \left({vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\leftrightarrow {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)$$
23	22	expr	$$⊢\left(A\subseteq ℝ\wedge x\subseteq ℝ\right)\to \left({vol}^{*}\left(x\right)\in ℝ\to \left({vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\leftrightarrow {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)$$
24	23	pm5.74d	$$⊢\left(A\subseteq ℝ\wedge x\subseteq ℝ\right)\to \left(\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\right)\leftrightarrow \left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)$$
25	2 24	sylan2	$$⊢\left(A\subseteq ℝ\wedge x\in 𝒫ℝ\right)\to \left(\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\right)\leftrightarrow \left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)$$
26	25	ralbidva	$$⊢A\subseteq ℝ\to \left(\forall x\in 𝒫ℝ\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\right)\leftrightarrow \forall x\in 𝒫ℝ\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)$$
27	26	pm5.32i	$$⊢\left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\right)={vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\right)\right)\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)$$
28	1 27	bitri	$$⊢A\in \mathrm{dom}vol\leftrightarrow \left(A\subseteq ℝ\wedge \forall x\in 𝒫ℝ\left({vol}^{*}\left(x\right)\in ℝ\to {vol}^{*}\left(x\cap A\right)+{vol}^{*}\left(x\setminus A\right)\le {vol}^{*}\left(x\right)\right)\right)$$