Metamath Proof Explorer


Theorem ovolfi

Description: A finite set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 13-Aug-2014)

Ref Expression
Assertion ovolfi
|- ( ( A e. Fin /\ A C_ RR ) -> ( vol* ` A ) = 0 )

Proof

Step Hyp Ref Expression
1 id
 |-  ( A C_ RR -> A C_ RR )
2 fict
 |-  ( A e. Fin -> A ~<_ _om )
3 nnenom
 |-  NN ~~ _om
4 3 ensymi
 |-  _om ~~ NN
5 domentr
 |-  ( ( A ~<_ _om /\ _om ~~ NN ) -> A ~<_ NN )
6 2 4 5 sylancl
 |-  ( A e. Fin -> A ~<_ NN )
7 ovolctb2
 |-  ( ( A C_ RR /\ A ~<_ NN ) -> ( vol* ` A ) = 0 )
8 1 6 7 syl2anr
 |-  ( ( A e. Fin /\ A C_ RR ) -> ( vol* ` A ) = 0 )