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	|- ( ph -> X e. Fin )
	snvonmbl.2	|- ( ph -> A e. ( RR ^m X ) )
Assertion	snvonmbl	|- ( ph -> { A } e. dom ( voln ` X ) )

Proof

Step	Hyp	Ref	Expression
1		snvonmbl.1	|- ( ph -> X e. Fin )
2		snvonmbl.2	|- ( ph -> A e. ( RR ^m X ) )
3	2	rrxsnicc	|- ( ph -> X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) = { A } )
4	3	eqcomd	|- ( ph -> { A } = X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) )
5		eqid	|- dom ( voln ` X ) = dom ( voln ` X )
6		elmapi	|- ( A e. ( RR ^m X ) -> A : X --> RR )
7	2 6	syl	|- ( ph -> A : X --> RR )
8	1 5 7 7	iccvonmbl	|- ( ph -> X_ k e. X ( ( A ` k ) [,] ( A ` k ) ) e. dom ( voln ` X ) )
9	4 8	eqeltrd	|- ( ph -> { A } e. dom ( voln ` X ) )