Theorem inmbl

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

	Ref	Expression
Assertion	inmbl	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∩ 𝐵 ) ∈ dom vol )

Proof

Step	Hyp	Ref	Expression
1		difundi	⊢ ( ℝ ∖ ( ( ℝ ∖ 𝐴 ) ∪ ( ℝ ∖ 𝐵 ) ) ) = ( ( ℝ ∖ ( ℝ ∖ 𝐴 ) ) ∩ ( ℝ ∖ ( ℝ ∖ 𝐵 ) ) )
2		mblss	⊢ ( 𝐴 ∈ dom vol → 𝐴 ⊆ ℝ )
3		dfss4	⊢ ( 𝐴 ⊆ ℝ ↔ ( ℝ ∖ ( ℝ ∖ 𝐴 ) ) = 𝐴 )
4	2 3	sylib	⊢ ( 𝐴 ∈ dom vol → ( ℝ ∖ ( ℝ ∖ 𝐴 ) ) = 𝐴 )
5		mblss	⊢ ( 𝐵 ∈ dom vol → 𝐵 ⊆ ℝ )
6		dfss4	⊢ ( 𝐵 ⊆ ℝ ↔ ( ℝ ∖ ( ℝ ∖ 𝐵 ) ) = 𝐵 )
7	5 6	sylib	⊢ ( 𝐵 ∈ dom vol → ( ℝ ∖ ( ℝ ∖ 𝐵 ) ) = 𝐵 )
8	4 7	ineqan12d	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( ( ℝ ∖ ( ℝ ∖ 𝐴 ) ) ∩ ( ℝ ∖ ( ℝ ∖ 𝐵 ) ) ) = ( 𝐴 ∩ 𝐵 ) )
9	1 8	eqtrid	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( ℝ ∖ ( ( ℝ ∖ 𝐴 ) ∪ ( ℝ ∖ 𝐵 ) ) ) = ( 𝐴 ∩ 𝐵 ) )
10		cmmbl	⊢ ( 𝐴 ∈ dom vol → ( ℝ ∖ 𝐴 ) ∈ dom vol )
11		cmmbl	⊢ ( 𝐵 ∈ dom vol → ( ℝ ∖ 𝐵 ) ∈ dom vol )
12		unmbl	⊢ ( ( ( ℝ ∖ 𝐴 ) ∈ dom vol ∧ ( ℝ ∖ 𝐵 ) ∈ dom vol ) → ( ( ℝ ∖ 𝐴 ) ∪ ( ℝ ∖ 𝐵 ) ) ∈ dom vol )
13	10 11 12	syl2an	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( ( ℝ ∖ 𝐴 ) ∪ ( ℝ ∖ 𝐵 ) ) ∈ dom vol )
14		cmmbl	⊢ ( ( ( ℝ ∖ 𝐴 ) ∪ ( ℝ ∖ 𝐵 ) ) ∈ dom vol → ( ℝ ∖ ( ( ℝ ∖ 𝐴 ) ∪ ( ℝ ∖ 𝐵 ) ) ) ∈ dom vol )
15	13 14	syl	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( ℝ ∖ ( ( ℝ ∖ 𝐴 ) ∪ ( ℝ ∖ 𝐵 ) ) ) ∈ dom vol )
16	9 15	eqeltrrd	⊢ ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∩ 𝐵 ) ∈ dom vol )