Metamath Proof Explorer


Theorem von0val

Description: The Lebesgue measure (for the zero dimensional space of reals) of every measurable set is zero. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypothesis von0val.1
|- ( ph -> A e. dom ( voln ` (/) ) )
Assertion von0val
|- ( ph -> ( ( voln ` (/) ) ` A ) = 0 )

Proof

Step Hyp Ref Expression
1 von0val.1
 |-  ( ph -> A e. dom ( voln ` (/) ) )
2 0fin
 |-  (/) e. Fin
3 2 a1i
 |-  ( ph -> (/) e. Fin )
4 3 1 mblvon
 |-  ( ph -> ( ( voln ` (/) ) ` A ) = ( ( voln* ` (/) ) ` A ) )
5 3 1 vonmblss2
 |-  ( ph -> A C_ ( RR ^m (/) ) )
6 5 ovn0val
 |-  ( ph -> ( ( voln* ` (/) ) ` A ) = 0 )
7 4 6 eqtrd
 |-  ( ph -> ( ( voln ` (/) ) ` A ) = 0 )