Metamath Proof Explorer


Theorem ovolun

Description: The Lebesgue outer measure function is finitely sub-additive. (Unlike the stronger ovoliun , this does not require any choice principles.) (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Assertion ovolun ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simpll ( ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) )
2 simplr ( ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) ∧ 𝑥 ∈ ℝ+ ) → ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) )
3 simpr ( ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
4 1 2 3 ovolunlem2 ( ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) ∧ 𝑥 ∈ ℝ+ ) → ( vol* ‘ ( 𝐴𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝑥 ) )
5 4 ralrimiva ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ∀ 𝑥 ∈ ℝ+ ( vol* ‘ ( 𝐴𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝑥 ) )
6 unss ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) ↔ ( 𝐴𝐵 ) ⊆ ℝ )
7 6 biimpi ( ( 𝐴 ⊆ ℝ ∧ 𝐵 ⊆ ℝ ) → ( 𝐴𝐵 ) ⊆ ℝ )
8 7 ad2ant2r ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( 𝐴𝐵 ) ⊆ ℝ )
9 ovolcl ( ( 𝐴𝐵 ) ⊆ ℝ → ( vol* ‘ ( 𝐴𝐵 ) ) ∈ ℝ* )
10 8 9 syl ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴𝐵 ) ) ∈ ℝ* )
11 readdcl ( ( ( vol* ‘ 𝐴 ) ∈ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) → ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ )
12 11 ad2ant2l ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ )
13 xralrple ( ( ( vol* ‘ ( 𝐴𝐵 ) ) ∈ ℝ* ∧ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ∈ ℝ ) → ( ( vol* ‘ ( 𝐴𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ↔ ∀ 𝑥 ∈ ℝ+ ( vol* ‘ ( 𝐴𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝑥 ) ) )
14 10 12 13 syl2anc ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( ( vol* ‘ ( 𝐴𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) ↔ ∀ 𝑥 ∈ ℝ+ ( vol* ‘ ( 𝐴𝐵 ) ) ≤ ( ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) + 𝑥 ) ) )
15 5 14 mpbird ( ( ( 𝐴 ⊆ ℝ ∧ ( vol* ‘ 𝐴 ) ∈ ℝ ) ∧ ( 𝐵 ⊆ ℝ ∧ ( vol* ‘ 𝐵 ) ∈ ℝ ) ) → ( vol* ‘ ( 𝐴𝐵 ) ) ≤ ( ( vol* ‘ 𝐴 ) + ( vol* ‘ 𝐵 ) ) )