Theorem ovolfi

Description: A finite set has 0 outer Lebesgue measure. (Contributed by Mario Carneiro, 13-Aug-2014)

	Ref	Expression
Assertion	ovolfi	$$⊢\left(A\in \mathrm{Fin}\wedge A\subseteq ℝ\right)\to {vol}^{*}\left(A\right)=0$$

Proof

Step	Hyp	Ref	Expression
1		id	$$⊢A\subseteq ℝ\to A\subseteq ℝ$$
2		fict	$$⊢A\in \mathrm{Fin}\to A\preccurlyeq \mathrm{\omega }$$
3		nnenom	$$⊢\mathbb{N}\approx \mathrm{\omega }$$
4	3	ensymi	$$⊢\mathrm{\omega }\approx \mathbb{N}$$
5		domentr	$$⊢\left(A\preccurlyeq \mathrm{\omega }\wedge \mathrm{\omega }\approx \mathbb{N}\right)\to A\preccurlyeq \mathbb{N}$$
6	2 4 5	sylancl	$$⊢A\in \mathrm{Fin}\to A\preccurlyeq \mathbb{N}$$
7		ovolctb2	$$⊢\left(A\subseteq ℝ\wedge A\preccurlyeq \mathbb{N}\right)\to {vol}^{*}\left(A\right)=0$$
8	1 6 7	syl2anr	$$⊢\left(A\in \mathrm{Fin}\wedge A\subseteq ℝ\right)\to {vol}^{*}\left(A\right)=0$$