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 ) |
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 ) |