vonct

Description: The n-dimensional Lebesgue measure of any countable set is zero. This is the second statement in Proposition 115G (e) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	vonct.1	$⊢ φ \to X \in Fin$
	vonct.2	$⊢ φ \to A \subseteq ℝ^{X}$
	vonct.3	$⊢ φ \to A ≼ ω$
Assertion	vonct	$⊢ φ \to voln (X) (A) = 0$

Proof

Step	Hyp	Ref	Expression
1		vonct.1	$⊢ φ \to X \in Fin$
2		vonct.2	$⊢ φ \to A \subseteq ℝ^{X}$
3		vonct.3	$⊢ φ \to A ≼ ω$
4		iunid	$⊢ ⋃_{x \in A} \{x\} = A$
5	4	eqcomi	$⊢ A = ⋃_{x \in A} \{x\}$
6	5	fveq2i	$⊢ voln (X) (A) = voln (X) (⋃_{x \in A} \{x\})$
7	6	a1i	$⊢ φ \to voln (X) (A) = voln (X) (⋃_{x \in A} \{x\})$
8		nfv	$⊢ Ⅎ x φ$
9	1	vonmea	$⊢ φ \to voln (X) \in Meas$
10		eqid	$⊢ dom voln (X) = dom voln (X)$
11	1	adantr	$⊢ (φ \land x \in A) \to X \in Fin$
12	2	sselda	$⊢ (φ \land x \in A) \to x \in (ℝ^{X})$
13	11 12	snvonmbl	$⊢ (φ \land x \in A) \to \{x\} \in dom voln (X)$
14		sndisj	$⊢ \underset{x \in A}{Disj} \{x\}$
15	14	a1i	$⊢ φ \to \underset{x \in A}{Disj} \{x\}$
16	8 9 10 13 3 15	meadjiun	$⊢ φ \to voln (X) (⋃_{x \in A} \{x\}) = sum^((x \in A ⟼ voln (X) (\{x\})))$
17	11 12	vonsn	$⊢ (φ \land x \in A) \to voln (X) (\{x\}) = 0$
18	17	mpteq2dva	$⊢ φ \to (x \in A ⟼ voln (X) (\{x\})) = (x \in A ⟼ 0)$
19	18	fveq2d	$⊢ φ \to sum^((x \in A ⟼ voln (X) (\{x\}))) = sum^((x \in A ⟼ 0))$
20	9 10	dmmeasal	$⊢ φ \to dom voln (X) \in SAlg$
21	20 3 13	saliuncl	$⊢ φ \to ⋃_{x \in A} \{x\} \in dom voln (X)$
22	4 21	eqeltrrid	$⊢ φ \to A \in dom voln (X)$
23	8 22	sge0z	$⊢ φ \to sum^((x \in A ⟼ 0)) = 0$
24	19 23	eqtrd	$⊢ φ \to sum^((x \in A ⟼ voln (X) (\{x\}))) = 0$
25	7 16 24	3eqtrd	$⊢ φ \to voln (X) (A) = 0$

Metamath Proof Explorer

Theorem vonct

Proof