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	$$⊢\phi \to A\in \mathrm{dom}\mathrm{voln}\left(\varnothing \right)$$
Assertion	von0val	$$⊢\phi \to \mathrm{voln}\left(\varnothing \right)\left(A\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		von0val.1	$$⊢\phi \to A\in \mathrm{dom}\mathrm{voln}\left(\varnothing \right)$$
2		0fin	$$⊢\varnothing \in \mathrm{Fin}$$
3	2	a1i	$$⊢\phi \to \varnothing \in \mathrm{Fin}$$
4	3 1	mblvon	$$⊢\phi \to \mathrm{voln}\left(\varnothing \right)\left(A\right)=\mathrm{voln*}\left(\varnothing \right)\left(A\right)$$
5	3 1	vonmblss2	$$⊢\phi \to A\subseteq {ℝ}^{\varnothing }$$
6	5	ovn0val	$$⊢\phi \to \mathrm{voln*}\left(\varnothing \right)\left(A\right)=0$$
7	4 6	eqtrd	$$⊢\phi \to \mathrm{voln}\left(\varnothing \right)\left(A\right)=0$$