Metamath Proof Explorer

Theorem ovolss

Description: The volume of a set is monotone with respect to set inclusion. (Contributed by Mario Carneiro, 16-Mar-2014)

Ref Expression
Assertion ovolss 
|- ( ( A C_ B /\ B C_ RR ) -> ( vol* ` A ) <_ ( vol* ` B ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( A C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
2 eqid 
 |-  { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) } = { y e. RR* | E. f e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) ( B C_ U. ran ( (,) o. f ) /\ y = sup ( ran seq 1 ( + , ( ( abs o. - ) o. f ) ) , RR* , < ) ) }
3 1 2 ovolsslem 
 |-  ( ( A C_ B /\ B C_ RR ) -> ( vol* ` A ) <_ ( vol* ` B ) )