Theorem ovol0

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

	Ref	Expression
Assertion	ovol0	⊢ ( vol* ‘ ∅ ) = 0

Proof

Step	Hyp	Ref	Expression
1		0ss	⊢ ∅ ⊆ ℝ
2		nnex	⊢ ℕ ∈ V
3	2	0dom	⊢ ∅ ≼ ℕ
4		ovolctb2	⊢ ( ( ∅ ⊆ ℝ ∧ ∅ ≼ ℕ ) → ( vol* ‘ ∅ ) = 0 )
5	1 3 4	mp2an	⊢ ( vol* ‘ ∅ ) = 0