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	⊢ ( 𝜑 → 𝐴 ∈ dom ( voln ‘ ∅ ) )
Assertion	von0val	⊢ ( 𝜑 → ( ( voln ‘ ∅ ) ‘ 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		von0val.1	⊢ ( 𝜑 → 𝐴 ∈ dom ( voln ‘ ∅ ) )
2		0fin	⊢ ∅ ∈ Fin
3	2	a1i	⊢ ( 𝜑 → ∅ ∈ Fin )
4	3 1	mblvon	⊢ ( 𝜑 → ( ( voln ‘ ∅ ) ‘ 𝐴 ) = ( ( voln* ‘ ∅ ) ‘ 𝐴 ) )
5	3 1	vonmblss2	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m ∅ ) )
6	5	ovn0val	⊢ ( 𝜑 → ( ( voln* ‘ ∅ ) ‘ 𝐴 ) = 0 )
7	4 6	eqtrd	⊢ ( 𝜑 → ( ( voln ‘ ∅ ) ‘ 𝐴 ) = 0 )