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