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	$$⊢\phi \to X\in \mathrm{Fin}$$
	snvonmbl.2	$$⊢\phi \to A\in \left({ℝ}^X\right)$$
Assertion	snvonmbl	$$⊢\phi \to \left\{A\right\}\in \mathrm{dom}\mathrm{voln}\left(X\right)$$

Proof

Step	Hyp	Ref	Expression
1		snvonmbl.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2		snvonmbl.2	$$⊢\phi \to A\in \left({ℝ}^X\right)$$
3	2	rrxsnicc	$$⊢\phi \to \underset{k\in X}{⨉}\left[A\left(k\right),A\left(k\right)\right]=\left\{A\right\}$$
4	3	eqcomd	$$⊢\phi \to \left\{A\right\}=\underset{k\in X}{⨉}\left[A\left(k\right),A\left(k\right)\right]$$
5		eqid	$$⊢\mathrm{dom}\mathrm{voln}\left(X\right)=\mathrm{dom}\mathrm{voln}\left(X\right)$$
6		elmapi	$$⊢A\in \left({ℝ}^X\right)\to A:X⟶ℝ$$
7	2 6	syl	$$⊢\phi \to A:X⟶ℝ$$
8	1 5 7 7	iccvonmbl	$$⊢\phi \to \underset{k\in X}{⨉}\left[A\left(k\right),A\left(k\right)\right]\in \mathrm{dom}\mathrm{voln}\left(X\right)$$
9	4 8	eqeltrd	$$⊢\phi \to \left\{A\right\}\in \mathrm{dom}\mathrm{voln}\left(X\right)$$