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 )