MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ovolss Structured version   Unicode version

Theorem ovolss 21631
Description: The volume of a set is monotone with respect to set inclusion. (Contributed by Mario Carneiro, 16-Mar-2014.)
Assertion
Ref Expression
ovolss  |-  ( ( A  C_  B  /\  B  C_  RR )  -> 
( vol* `  A )  <_  ( vol* `  B ) )

Proof of Theorem ovolss
Dummy variables  f 
y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2467 . 2  |-  { y  e.  RR*  |  E. f  e.  ( (  <_  i^i  ( RR  X.  RR ) )  ^m  NN ) ( A  C_  U.