Theorem 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	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	vonct.2	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
	vonct.3	⊢ ( 𝜑 → 𝐴 ≼ ω )
Assertion	vonct	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐴 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		vonct.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		vonct.2	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
3		vonct.3	⊢ ( 𝜑 → 𝐴 ≼ ω )
4		iunid	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴
5	4	eqcomi	⊢ 𝐴 = ∪ 𝑥 ∈ 𝐴 { 𝑥 }
6	5	fveq2i	⊢ ( ( voln ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln ‘ 𝑋 ) ‘ ∪ 𝑥 ∈ 𝐴 { 𝑥 } )
7	6	a1i	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐴 ) = ( ( voln ‘ 𝑋 ) ‘ ∪ 𝑥 ∈ 𝐴 { 𝑥 } ) )
8		nfv	⊢ Ⅎ 𝑥 𝜑
9	1	vonmea	⊢ ( 𝜑 → ( voln ‘ 𝑋 ) ∈ Meas )
10		eqid	⊢ dom ( voln ‘ 𝑋 ) = dom ( voln ‘ 𝑋 )
11	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑋 ∈ Fin )
12	2	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( ℝ ↑m 𝑋 ) )
13	11 12	snvonmbl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 } ∈ dom ( voln ‘ 𝑋 ) )
14		sndisj	⊢ Disj 𝑥 ∈ 𝐴 { 𝑥 }
15	14	a1i	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝐴 { 𝑥 } )
16	8 9 10 13 3 15	meadjiun	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ ∪ 𝑥 ∈ 𝐴 { 𝑥 } ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( ( voln ‘ 𝑋 ) ‘ { 𝑥 } ) ) ) )
17	11 12	vonsn	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( voln ‘ 𝑋 ) ‘ { 𝑥 } ) = 0 )
18	17	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ( voln ‘ 𝑋 ) ‘ { 𝑥 } ) ) = ( 𝑥 ∈ 𝐴 ↦ 0 ) )
19	18	fveq2d	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( ( voln ‘ 𝑋 ) ‘ { 𝑥 } ) ) ) = ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 0 ) ) )
20	9 10	dmmeasal	⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) ∈ SAlg )
21	20 3 13	saliuncl	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 { 𝑥 } ∈ dom ( voln ‘ 𝑋 ) )
22	4 21	eqeltrrid	⊢ ( 𝜑 → 𝐴 ∈ dom ( voln ‘ 𝑋 ) )
23	8 22	sge0z	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ 0 ) ) = 0 )
24	19 23	eqtrd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑥 ∈ 𝐴 ↦ ( ( voln ‘ 𝑋 ) ‘ { 𝑥 } ) ) ) = 0 )
25	7 16 24	3eqtrd	⊢ ( 𝜑 → ( ( voln ‘ 𝑋 ) ‘ 𝐴 ) = 0 )