Metamath Proof Explorer

Theorem ovolssnul

Description: A subset of a nullset is null. (Contributed by Mario Carneiro, 19-Mar-2014)

Ref Expression
Assertion ovolssnul 
|- ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( vol* ` A ) = 0 )

Proof

Step Hyp Ref Expression
1 ovolss 
 |-  ( ( A C_ B /\ B C_ RR ) -> ( vol* ` A ) <_ ( vol* ` B ) )
2 1 3adant3 
 |-  ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( vol* ` A ) <_ ( vol* ` B ) )
3 simp3 
 |-  ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( vol* ` B ) = 0 )
4 2 3 breqtrd 
 |-  ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( vol* ` A ) <_ 0 )
5 sstr 
 |-  ( ( A C_ B /\ B C_ RR ) -> A C_ RR )
6 5 3adant3 
 |-  ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> A C_ RR )
7 ovolge0 
 |-  ( A C_ RR -> 0 <_ ( vol* ` A ) )
8 6 7 syl 
 |-  ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> 0 <_ ( vol* ` A ) )
9 ovolcl 
 |-  ( A C_ RR -> ( vol* ` A ) e. RR* )
10 6 9 syl 
 |-  ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( vol* ` A ) e. RR* )
11 0xr 
 |-  0 e. RR*
12 xrletri3 
 |-  ( ( ( vol* ` A ) e. RR* /\ 0 e. RR* ) -> ( ( vol* ` A ) = 0 <-> ( ( vol* ` A ) <_ 0 /\ 0 <_ ( vol* ` A ) ) ) )
13 10 11 12 sylancl 
 |-  ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( ( vol* ` A ) = 0 <-> ( ( vol* ` A ) <_ 0 /\ 0 <_ ( vol* ` A ) ) ) )
14 4 8 13 mpbir2and 
 |-  ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) = 0 ) -> ( vol* ` A ) = 0 )