unmbl

Description: A union of measurable sets is measurable. (Contributed by Mario Carneiro, 18-Mar-2014)

		Ref	Expression
	Assertion	unmbl	$⊢ (A \in dom vol \land B \in dom vol) \to A \cup B \in dom vol$

Proof

Step	Hyp	Ref	Expression
1		mblss	$⊢ A \in dom vol \to A \subseteq ℝ$
2		mblss	$⊢ B \in dom vol \to B \subseteq ℝ$
3	1 2	anim12i	$⊢ (A \in dom vol \land B \in dom vol) \to (A \subseteq ℝ \land B \subseteq ℝ)$
4		unss	$⊢ (A \subseteq ℝ \land B \subseteq ℝ) \leftrightarrow A \cup B \subseteq ℝ$
5	3 4	sylib	$⊢ (A \in dom vol \land B \in dom vol) \to A \cup B \subseteq ℝ$
6		elpwi	$⊢ x \in 𝒫 ℝ \to x \subseteq ℝ$
7		inss1	$⊢ x \cap (A \cup B) \subseteq x$
8		ovolsscl	$⊢ (x \cap (A \cup B) \subseteq x \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap (A \cup B)) \in ℝ$
9	7 8	mp3an1	$⊢ (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap (A \cup B)) \in ℝ$
10	9	adantl	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap (A \cup B)) \in ℝ$
11		inss1	$⊢ x \cap A \subseteq x$
12		ovolsscl	$⊢ (x \cap A \subseteq x \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap A) \in ℝ$
13	11 12	mp3an1	$⊢ (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x \cap A) \in ℝ$
14	13	adantl	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap A) \in ℝ$
15		inss1	$⊢ (x ∖ A) \cap B \subseteq x ∖ A$
16		difss	$⊢ x ∖ A \subseteq x$
17		simprl	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{*} (x) \in ℝ)) \to x \subseteq ℝ$
18	16 17	sstrid	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{*} (x) \in ℝ)) \to x ∖ A \subseteq ℝ$
19		ovolsscl	$⊢ (x ∖ A \subseteq x \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ A) \in ℝ$
20	16 19	mp3an1	$⊢ (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ A) \in ℝ$
21	20	adantl	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x ∖ A) \in ℝ$
22		ovolsscl	$⊢ ((x ∖ A) \cap B \subseteq x ∖ A \land x ∖ A \subseteq ℝ \land {vol}^{} (x ∖ A) \in ℝ) \to {vol}^{} ((x ∖ A) \cap B) \in ℝ$
23	15 18 21 22	mp3an2i	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} ((x ∖ A) \cap B) \in ℝ$
24	14 23	readdcld	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap A) + {vol}^{*} ((x ∖ A) \cap B) \in ℝ$
25		difss	$⊢ x ∖ (A \cup B) \subseteq x$
26		ovolsscl	$⊢ (x ∖ (A \cup B) \subseteq x \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ (A \cup B)) \in ℝ$
27	25 26	mp3an1	$⊢ (x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x ∖ (A \cup B)) \in ℝ$
28	27	adantl	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x ∖ (A \cup B)) \in ℝ$
29		incom	$⊢ (x ∖ A) \cap B = B \cap (x ∖ A)$
30		indifcom	$⊢ B \cap (x ∖ A) = x \cap (B ∖ A)$
31	29 30	eqtri	$⊢ (x ∖ A) \cap B = x \cap (B ∖ A)$
32	31	uneq2i	$⊢ (x \cap A) \cup ((x ∖ A) \cap B) = (x \cap A) \cup (x \cap (B ∖ A))$
33		indi	$⊢ x \cap (A \cup (B ∖ A)) = (x \cap A) \cup (x \cap (B ∖ A))$
34		undif2	$⊢ A \cup (B ∖ A) = A \cup B$
35	34	ineq2i	$⊢ x \cap (A \cup (B ∖ A)) = x \cap (A \cup B)$
36	32 33 35	3eqtr2ri	$⊢ x \cap (A \cup B) = (x \cap A) \cup ((x ∖ A) \cap B)$
37	36	fveq2i	$⊢ {vol}^{} (x \cap (A \cup B)) = {vol}^{} ((x \cap A) \cup ((x ∖ A) \cap B))$
38	11 17	sstrid	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{*} (x) \in ℝ)) \to x \cap A \subseteq ℝ$
39	15 18	sstrid	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{*} (x) \in ℝ)) \to (x ∖ A) \cap B \subseteq ℝ$
40		ovolun	$⊢ ((x \cap A \subseteq ℝ \land {vol}^{} (x \cap A) \in ℝ) \land ((x ∖ A) \cap B \subseteq ℝ \land {vol}^{} ((x ∖ A) \cap B) \in ℝ)) \to {vol}^{} ((x \cap A) \cup ((x ∖ A) \cap B)) \leq {vol}^{} (x \cap A) + {vol}^{*} ((x ∖ A) \cap B)$
41	38 14 39 23 40	syl22anc	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} ((x \cap A) \cup ((x ∖ A) \cap B)) \leq {vol}^{} (x \cap A) + {vol}^{} ((x ∖ A) \cap B)$
42	37 41	eqbrtrid	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap (A \cup B)) \leq {vol}^{} (x \cap A) + {vol}^{} ((x ∖ A) \cap B)$
43	10 24 28 42	leadd1dd	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap (A \cup B)) + {vol}^{} (x ∖ (A \cup B)) \leq {vol}^{} (x \cap A) + {vol}^{} ((x ∖ A) \cap B) + {vol}^{} (x ∖ (A \cup B))$
44		simplr	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{*} (x) \in ℝ)) \to B \in dom vol$
45		mblsplit	$⊢ (B \in dom vol \land x ∖ A \subseteq ℝ \land {vol}^{} (x ∖ A) \in ℝ) \to {vol}^{} (x ∖ A) = {vol}^{} ((x ∖ A) \cap B) + {vol}^{} ((x ∖ A) ∖ B)$
46	44 18 21 45	syl3anc	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x ∖ A) = {vol}^{} ((x ∖ A) \cap B) + {vol}^{} ((x ∖ A) ∖ B)$
47		difun1	$⊢ x ∖ (A \cup B) = (x ∖ A) ∖ B$
48	47	fveq2i	$⊢ {vol}^{} (x ∖ (A \cup B)) = {vol}^{} ((x ∖ A) ∖ B)$
49	48	oveq2i	$⊢ {vol}^{} ((x ∖ A) \cap B) + {vol}^{} (x ∖ (A \cup B)) = {vol}^{} ((x ∖ A) \cap B) + {vol}^{} ((x ∖ A) ∖ B)$
50	46 49	eqtr4di	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x ∖ A) = {vol}^{} ((x ∖ A) \cap B) + {vol}^{} (x ∖ (A \cup B))$
51	50	oveq2d	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap A) + {vol}^{} (x ∖ A) = {vol}^{} (x \cap A) + {vol}^{} ((x ∖ A) \cap B) + {vol}^{} (x ∖ (A \cup B))$
52		simpll	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{*} (x) \in ℝ)) \to A \in dom vol$
53		simprr	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x) \in ℝ$
54		mblsplit	$⊢ (A \in dom vol \land x \subseteq ℝ \land {vol}^{} (x) \in ℝ) \to {vol}^{} (x) = {vol}^{} (x \cap A) + {vol}^{} (x ∖ A)$
55	52 17 53 54	syl3anc	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x) = {vol}^{} (x \cap A) + {vol}^{} (x ∖ A)$
56	14	recnd	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap A) \in ℂ$
57	23	recnd	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} ((x ∖ A) \cap B) \in ℂ$
58	28	recnd	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x ∖ (A \cup B)) \in ℂ$
59	56 57 58	addassd	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap A) + {vol}^{} ((x ∖ A) \cap B) + {vol}^{} (x ∖ (A \cup B)) = {vol}^{} (x \cap A) + {vol}^{} ((x ∖ A) \cap B) + {vol}^{*} (x ∖ (A \cup B))$
60	51 55 59	3eqtr4d	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x) = {vol}^{} (x \cap A) + {vol}^{} ((x ∖ A) \cap B) + {vol}^{*} (x ∖ (A \cup B))$
61	43 60	breqtrrd	$⊢ ((A \in dom vol \land B \in dom vol) \land (x \subseteq ℝ \land {vol}^{} (x) \in ℝ)) \to {vol}^{} (x \cap (A \cup B)) + {vol}^{} (x ∖ (A \cup B)) \leq {vol}^{} (x)$
62	61	expr	$⊢ ((A \in dom vol \land B \in dom vol) \land x \subseteq ℝ) \to ({vol}^{} (x) \in ℝ \to {vol}^{} (x \cap (A \cup B)) + {vol}^{} (x ∖ (A \cup B)) \leq {vol}^{} (x))$
63	6 62	sylan2	$⊢ ((A \in dom vol \land B \in dom vol) \land x \in 𝒫 ℝ) \to ({vol}^{} (x) \in ℝ \to {vol}^{} (x \cap (A \cup B)) + {vol}^{} (x ∖ (A \cup B)) \leq {vol}^{} (x))$
64	63	ralrimiva	$⊢ (A \in dom vol \land B \in dom vol) \to \forall x \in 𝒫 ℝ ({vol}^{} (x) \in ℝ \to {vol}^{} (x \cap (A \cup B)) + {vol}^{} (x ∖ (A \cup B)) \leq {vol}^{} (x))$
65		ismbl2	$⊢ A \cup B \in dom vol \leftrightarrow (A \cup B \subseteq ℝ \land \forall x \in 𝒫 ℝ ({vol}^{} (x) \in ℝ \to {vol}^{} (x \cap (A \cup B)) + {vol}^{} (x ∖ (A \cup B)) \leq {vol}^{} (x)))$
66	5 64 65	sylanbrc	$⊢ (A \in dom vol \land B \in dom vol) \to A \cup B \in dom vol$

Metamath Proof Explorer

Theorem unmbl

Proof