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	|- ( ph -> X e. Fin )
	ctvonmbl.2	|- ( ph -> A C_ ( RR ^m X ) )
	ctvonmbl.3	|- ( ph -> A ~<_ _om )
Assertion	ctvonmbl	|- ( ph -> A e. dom ( voln ` X ) )

Proof

Step	Hyp	Ref	Expression
1		ctvonmbl.1	|- ( ph -> X e. Fin )
2		ctvonmbl.2	|- ( ph -> A C_ ( RR ^m X ) )
3		ctvonmbl.3	|- ( ph -> A ~<_ _om )
4		iunid	|- U_ x e. A { x } = A
5	1	vonmea	|- ( ph -> ( voln ` X ) e. Meas )
6		eqid	|- dom ( voln ` X ) = dom ( voln ` X )
7	5 6	dmmeasal	|- ( ph -> dom ( voln ` X ) e. SAlg )
8	1	adantr	|- ( ( ph /\ x e. A ) -> X e. Fin )
9	2	sselda	|- ( ( ph /\ x e. A ) -> x e. ( RR ^m X ) )
10	8 9	snvonmbl	|- ( ( ph /\ x e. A ) -> { x } e. dom ( voln ` X ) )
11	7 3 10	saliuncl	|- ( ph -> U_ x e. A { x } e. dom ( voln ` X ) )
12	4 11	eqeltrrid	|- ( ph -> A e. dom ( voln ` X ) )