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

Metamath Proof Explorer

Theorem unmbl

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

Ref Expression
Assertion unmbl ( ( 𝐴 ∈ dom vol ∧ 𝐵 ∈ dom vol ) → ( 𝐴 ∪ 𝐵 ) ∈ dom vol )

Proof

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