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
|- ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) <_ ( ( vol* ` A ) + ( vol* ` B ) ) )

Proof

Step Hyp Ref Expression
1 simpll
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ x e. RR+ ) -> ( A C_ RR /\ ( vol* ` A ) e. RR ) )
2 simplr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ x e. RR+ ) -> ( B C_ RR /\ ( vol* ` B ) e. RR ) )
3 simpr
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ x e. RR+ ) -> x e. RR+ )
4 1 2 3 ovolunlem2
 |-  ( ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) /\ x e. RR+ ) -> ( vol* ` ( A u. B ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + x ) )
5 4 ralrimiva
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> A. x e. RR+ ( vol* ` ( A u. B ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + x ) )
6 unss
 |-  ( ( A C_ RR /\ B C_ RR ) <-> ( A u. B ) C_ RR )
7 6 biimpi
 |-  ( ( A C_ RR /\ B C_ RR ) -> ( A u. B ) C_ RR )
8 7 ad2ant2r
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( A u. B ) C_ RR )
9 ovolcl
 |-  ( ( A u. B ) C_ RR -> ( vol* ` ( A u. B ) ) e. RR* )
10 8 9 syl
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) e. RR* )
11 readdcl
 |-  ( ( ( vol* ` A ) e. RR /\ ( vol* ` B ) e. RR ) -> ( ( vol* ` A ) + ( vol* ` B ) ) e. RR )
12 11 ad2ant2l
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( ( vol* ` A ) + ( vol* ` B ) ) e. RR )
13 xralrple
 |-  ( ( ( vol* ` ( A u. B ) ) e. RR* /\ ( ( vol* ` A ) + ( vol* ` B ) ) e. RR ) -> ( ( vol* ` ( A u. B ) ) <_ ( ( vol* ` A ) + ( vol* ` B ) ) <-> A. x e. RR+ ( vol* ` ( A u. B ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + x ) ) )
14 10 12 13 syl2anc
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( ( vol* ` ( A u. B ) ) <_ ( ( vol* ` A ) + ( vol* ` B ) ) <-> A. x e. RR+ ( vol* ` ( A u. B ) ) <_ ( ( ( vol* ` A ) + ( vol* ` B ) ) + x ) ) )
15 5 14 mpbird
 |-  ( ( ( A C_ RR /\ ( vol* ` A ) e. RR ) /\ ( B C_ RR /\ ( vol* ` B ) e. RR ) ) -> ( vol* ` ( A u. B ) ) <_ ( ( vol* ` A ) + ( vol* ` B ) ) )