This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ovolfi

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

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

Step	Hyp	Ref	Expression
1		id	$⊢ A \subseteq ℝ \to A \subseteq ℝ$
2		fict	$⊢ A \in Fin \to A ≼ ω$
3		nnenom	$⊢ ℕ \approx ω$
4	3	ensymi	$⊢ ω \approx ℕ$
5		domentr	$⊢ (A ≼ ω \land ω \approx ℕ) \to A ≼ ℕ$
6	2 4 5	sylancl	$⊢ A \in Fin \to A ≼ ℕ$
7		ovolctb2	$⊢ (A \subseteq ℝ \land A ≼ ℕ) \to {vol}^{*} (A) = 0$
8	1 6 7	syl2anr	$⊢ (A \in Fin \land A \subseteq ℝ) \to {vol}^{*} (A) = 0$