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 ${⊢}\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge \left({B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {vol}^{*}\left({A}\cup {B}\right)\le {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)$

Proof

Step Hyp Ref Expression
1 simpll ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge \left({B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to \left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)$
2 simplr ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge \left({B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to \left({B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)$
3 simpr ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge \left({B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to {x}\in {ℝ}^{+}$
4 1 2 3 ovolunlem2 ${⊢}\left(\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge \left({B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\wedge {x}\in {ℝ}^{+}\right)\to {vol}^{*}\left({A}\cup {B}\right)\le {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)+{x}$
5 4 ralrimiva ${⊢}\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge \left({B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\cup {B}\right)\le {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)+{x}$
6 unss ${⊢}\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)↔{A}\cup {B}\subseteq ℝ$
7 6 biimpi ${⊢}\left({A}\subseteq ℝ\wedge {B}\subseteq ℝ\right)\to {A}\cup {B}\subseteq ℝ$
8 7 ad2ant2r ${⊢}\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge \left({B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {A}\cup {B}\subseteq ℝ$
9 ovolcl ${⊢}{A}\cup {B}\subseteq ℝ\to {vol}^{*}\left({A}\cup {B}\right)\in {ℝ}^{*}$
10 8 9 syl ${⊢}\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge \left({B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {vol}^{*}\left({A}\cup {B}\right)\in {ℝ}^{*}$
11 readdcl ${⊢}\left({vol}^{*}\left({A}\right)\in ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\to {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)\in ℝ$
12 11 ad2ant2l ${⊢}\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge \left({B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)\in ℝ$
13 xralrple ${⊢}\left({vol}^{*}\left({A}\cup {B}\right)\in {ℝ}^{*}\wedge {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)\in ℝ\right)\to \left({vol}^{*}\left({A}\cup {B}\right)\le {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\cup {B}\right)\le {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)+{x}\right)$
14 10 12 13 syl2anc ${⊢}\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge \left({B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to \left({vol}^{*}\left({A}\cup {B}\right)\le {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}{vol}^{*}\left({A}\cup {B}\right)\le {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)+{x}\right)$
15 5 14 mpbird ${⊢}\left(\left({A}\subseteq ℝ\wedge {vol}^{*}\left({A}\right)\in ℝ\right)\wedge \left({B}\subseteq ℝ\wedge {vol}^{*}\left({B}\right)\in ℝ\right)\right)\to {vol}^{*}\left({A}\cup {B}\right)\le {vol}^{*}\left({A}\right)+{vol}^{*}\left({B}\right)$