Theorem snvonmbl

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

	Ref	Expression
Hypotheses	snvonmbl.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	snvonmbl.2	⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m 𝑋 ) )
Assertion	snvonmbl	⊢ ( 𝜑 → { 𝐴 } ∈ dom ( voln ‘ 𝑋 ) )

Proof

Step	Hyp	Ref	Expression
1		snvonmbl.1	⊢ ( 𝜑 → 𝑋 ∈ Fin )
2		snvonmbl.2	⊢ ( 𝜑 → 𝐴 ∈ ( ℝ ↑m 𝑋 ) )
3	2	rrxsnicc	⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) = { 𝐴 } )
4	3	eqcomd	⊢ ( 𝜑 → { 𝐴 } = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) )
5		eqid	⊢ dom ( voln ‘ 𝑋 ) = dom ( voln ‘ 𝑋 )
6		elmapi	⊢ ( 𝐴 ∈ ( ℝ ↑m 𝑋 ) → 𝐴 : 𝑋 ⟶ ℝ )
7	2 6	syl	⊢ ( 𝜑 → 𝐴 : 𝑋 ⟶ ℝ )
8	1 5 7 7	iccvonmbl	⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,] ( 𝐴 ‘ 𝑘 ) ) ∈ dom ( voln ‘ 𝑋 ) )
9	4 8	eqeltrd	⊢ ( 𝜑 → { 𝐴 } ∈ dom ( voln ‘ 𝑋 ) )