Metamath Proof Explorer

Theorem ovolsscl

Description: If a set is contained in another of bounded measure, it too is bounded. (Contributed by Mario Carneiro, 18-Mar-2014)

Ref Expression
Assertion ovolsscl 
|- ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` A ) e. RR )

Proof

Step Hyp Ref Expression
1 sstr 
 |-  ( ( A C_ B /\ B C_ RR ) -> A C_ RR )
2 1 3adant3 
 |-  ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) e. RR ) -> A C_ RR )
3 simp3 
 |-  ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` B ) e. RR )
4 ovolss 
 |-  ( ( A C_ B /\ B C_ RR ) -> ( vol* ` A ) <_ ( vol* ` B ) )
5 4 3adant3 
 |-  ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` A ) <_ ( vol* ` B ) )
6 ovollecl 
 |-  ( ( A C_ RR /\ ( vol* ` B ) e. RR /\ ( vol* ` A ) <_ ( vol* ` B ) ) -> ( vol* ` A ) e. RR )
7 2 3 5 6 syl3anc 
 |-  ( ( A C_ B /\ B C_ RR /\ ( vol* ` B ) e. RR ) -> ( vol* ` A ) e. RR )