Theorem ovolsn

Description: A singleton has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 15-Aug-2014)

	Ref	Expression
Assertion	ovolsn	⊢ ( 𝐴 ∈ ℝ → ( vol* ‘ { 𝐴 } ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		snfi	⊢ { 𝐴 } ∈ Fin
2		snssi	⊢ ( 𝐴 ∈ ℝ → { 𝐴 } ⊆ ℝ )
3		ovolfi	⊢ ( ( { 𝐴 } ∈ Fin ∧ { 𝐴 } ⊆ ℝ ) → ( vol* ‘ { 𝐴 } ) = 0 )
4	1 2 3	sylancr	⊢ ( 𝐴 ∈ ℝ → ( vol* ‘ { 𝐴 } ) = 0 )