Theorem ovolfi

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

	Ref	Expression
Assertion	ovolfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ ℝ ) → ( vol* ‘ 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐴 ⊆ ℝ → 𝐴 ⊆ ℝ )
2		fict	⊢ ( 𝐴 ∈ Fin → 𝐴 ≼ ω )
3		nnenom	⊢ ℕ ≈ ω
4	3	ensymi	⊢ ω ≈ ℕ
5		domentr	⊢ ( ( 𝐴 ≼ ω ∧ ω ≈ ℕ ) → 𝐴 ≼ ℕ )
6	2 4 5	sylancl	⊢ ( 𝐴 ∈ Fin → 𝐴 ≼ ℕ )
7		ovolctb2	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≼ ℕ ) → ( vol* ‘ 𝐴 ) = 0 )
8	1 6 7	syl2anr	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐴 ⊆ ℝ ) → ( vol* ‘ 𝐴 ) = 0 )