Metamath Proof Explorer


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 ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 ismbl ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ) ) )
2 elpwi ( 𝑥 ∈ 𝒫 ℝ → 𝑥 ⊆ ℝ )
3 inundif ( ( 𝑥𝐴 ) ∪ ( 𝑥𝐴 ) ) = 𝑥
4 3 fveq2i ( vol* ‘ ( ( 𝑥𝐴 ) ∪ ( 𝑥𝐴 ) ) ) = ( vol* ‘ 𝑥 )
5 inss1 ( 𝑥𝐴 ) ⊆ 𝑥
6 simprl ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → 𝑥 ⊆ ℝ )
7 5 6 sstrid ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( 𝑥𝐴 ) ⊆ ℝ )
8 ovolsscl ( ( ( 𝑥𝐴 ) ⊆ 𝑥𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥𝐴 ) ) ∈ ℝ )
9 5 8 mp3an1 ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥𝐴 ) ) ∈ ℝ )
10 9 adantl ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑥𝐴 ) ) ∈ ℝ )
11 difss ( 𝑥𝐴 ) ⊆ 𝑥
12 11 6 sstrid ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( 𝑥𝐴 ) ⊆ ℝ )
13 ovolsscl ( ( ( 𝑥𝐴 ) ⊆ 𝑥𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥𝐴 ) ) ∈ ℝ )
14 11 13 mp3an1 ( ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) → ( vol* ‘ ( 𝑥𝐴 ) ) ∈ ℝ )
15 14 adantl ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝑥𝐴 ) ) ∈ ℝ )
16 ovolun ( ( ( ( 𝑥𝐴 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑥𝐴 ) ) ∈ ℝ ) ∧ ( ( 𝑥𝐴 ) ⊆ ℝ ∧ ( vol* ‘ ( 𝑥𝐴 ) ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝑥𝐴 ) ∪ ( 𝑥𝐴 ) ) ) ≤ ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) )
17 7 10 12 15 16 syl22anc ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ ( ( 𝑥𝐴 ) ∪ ( 𝑥𝐴 ) ) ) ≤ ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) )
18 4 17 eqbrtrrid ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ 𝑥 ) ≤ ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) )
19 simprr ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( vol* ‘ 𝑥 ) ∈ ℝ )
20 10 15 readdcld ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ∈ ℝ )
21 19 20 letri3d ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ↔ ( ( vol* ‘ 𝑥 ) ≤ ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ∧ ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
22 18 21 mpbirand ( ( 𝐴 ⊆ ℝ ∧ ( 𝑥 ⊆ ℝ ∧ ( vol* ‘ 𝑥 ) ∈ ℝ ) ) → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ↔ ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) )
23 22 expr ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ⊆ ℝ ) → ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ↔ ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
24 23 pm5.74d ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ⊆ ℝ ) → ( ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ) ↔ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
25 2 24 sylan2 ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ 𝒫 ℝ ) → ( ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ) ↔ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
26 25 ralbidva ( 𝐴 ⊆ ℝ → ( ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ) ↔ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
27 26 pm5.32i ( ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( vol* ‘ 𝑥 ) = ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ) ) ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )
28 1 27 bitri ( 𝐴 ∈ dom vol ↔ ( 𝐴 ⊆ ℝ ∧ ∀ 𝑥 ∈ 𝒫 ℝ ( ( vol* ‘ 𝑥 ) ∈ ℝ → ( ( vol* ‘ ( 𝑥𝐴 ) ) + ( vol* ‘ ( 𝑥𝐴 ) ) ) ≤ ( vol* ‘ 𝑥 ) ) ) )