Theorem ovol0

Description: The empty set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 17-Mar-2014)

	Ref	Expression
Assertion	ovol0	$$⊢{vol}^{*}\left(\varnothing \right)=0$$

Proof

Step	Hyp	Ref	Expression
1		0ss	$$⊢\varnothing \subseteq ℝ$$
2		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
3	2	0dom	$$⊢\varnothing \preccurlyeq \mathbb{N}$$
4		ovolctb2	$$⊢\left(\varnothing \subseteq ℝ\wedge \varnothing \preccurlyeq \mathbb{N}\right)\to {vol}^{*}\left(\varnothing \right)=0$$
5	1 3 4	mp2an	$$⊢{vol}^{*}\left(\varnothing \right)=0$$