This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )