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

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* ‘ 𝐵 ) ) )