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 ) ) )