Theorem ctvonmbl

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

	Ref	Expression
Hypotheses	ctvonmbl.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	ctvonmbl.2	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
	ctvonmbl.3	⊢ ( 𝜑 → 𝐴 ≼ ω )
Assertion	ctvonmbl	⊢ ( 𝜑 → 𝐴 ∈ dom ( voln ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		ctvonmbl.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		ctvonmbl.2	⊢ ( 𝜑 → 𝐴 ⊆ ( ℝ ↑m 𝑋 ) )
3		ctvonmbl.3	⊢ ( 𝜑 → 𝐴 ≼ ω )
4		iunid	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴
5	1	vonmea	⊢ ( 𝜑 → ( voln ‘ 𝑋 ) ∈ Meas )
6		eqid	⊢ dom ( voln ‘ 𝑋 ) = dom ( voln ‘ 𝑋 )
7	5 6	dmmeasal	⊢ ( 𝜑 → dom ( voln ‘ 𝑋 ) ∈ SAlg )
8	1	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑋 ∈ Fin )
9	2	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ( ℝ ↑m 𝑋 ) )
10	8 9	snvonmbl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → { 𝑥 } ∈ dom ( voln ‘ 𝑋 ) )
11	7 3 10	saliuncl	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 { 𝑥 } ∈ dom ( voln ‘ 𝑋 ) )
12	4 11	eqeltrrid	⊢ ( 𝜑 → 𝐴 ∈ dom ( voln ‘ 𝑋 ) )