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

Proof

Step	Hyp	Ref	Expression
1		ctvonmbl.1	$$⊢\phi \to X\in \mathrm{Fin}$$
2		ctvonmbl.2	$$⊢\phi \to A\subseteq {ℝ}^X$$
3		ctvonmbl.3	$$⊢\phi \to A\preccurlyeq \mathrm{\omega }$$
4		iunid	$$⊢\bigcup _{x\in A}\left\{x\right\}=A$$
5	1	vonmea	$$⊢\phi \to \mathrm{voln}\left(X\right)\in \mathrm{Meas}$$
6		eqid	$$⊢\mathrm{dom}\mathrm{voln}\left(X\right)=\mathrm{dom}\mathrm{voln}\left(X\right)$$
7	5 6	dmmeasal	$$⊢\phi \to \mathrm{dom}\mathrm{voln}\left(X\right)\in \mathrm{SAlg}$$
8	1	adantr	$$⊢\left(\phi \wedge x\in A\right)\to X\in \mathrm{Fin}$$
9	2	sselda	$$⊢\left(\phi \wedge x\in A\right)\to x\in \left({ℝ}^X\right)$$
10	8 9	snvonmbl	$$⊢\left(\phi \wedge x\in A\right)\to \left\{x\right\}\in \mathrm{dom}\mathrm{voln}\left(X\right)$$
11	7 3 10	saliuncl	$$⊢\phi \to \bigcup _{x\in A}\left\{x\right\}\in \mathrm{dom}\mathrm{voln}\left(X\right)$$
12	4 11	eqeltrrid	$$⊢\phi \to A\in \mathrm{dom}\mathrm{voln}\left(X\right)$$