Theorem vonct

Description: The n-dimensional Lebesgue measure of any countable set is zero. This is the second statement in Proposition 115G (e) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	vonct.1	|- ( ph -> X e. Fin )
	vonct.2	|- ( ph -> A C_ ( RR ^m X ) )
	vonct.3	|- ( ph -> A ~<_ _om )
Assertion	vonct	|- ( ph -> ( ( voln ` X ) ` A ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		vonct.1	|- ( ph -> X e. Fin )
2		vonct.2	|- ( ph -> A C_ ( RR ^m X ) )
3		vonct.3	|- ( ph -> A ~<_ _om )
4		iunid	|- U_ x e. A { x } = A
5	4	eqcomi	|- A = U_ x e. A { x }
6	5	fveq2i	|- ( ( voln ` X ) ` A ) = ( ( voln ` X ) ` U_ x e. A { x } )
7	6	a1i	|- ( ph -> ( ( voln ` X ) ` A ) = ( ( voln ` X ) ` U_ x e. A { x } ) )
8		nfv	|- F/ x ph
9	1	vonmea	|- ( ph -> ( voln ` X ) e. Meas )
10		eqid	|- dom ( voln ` X ) = dom ( voln ` X )
11	1	adantr	|- ( ( ph /\ x e. A ) -> X e. Fin )
12	2	sselda	|- ( ( ph /\ x e. A ) -> x e. ( RR ^m X ) )
13	11 12	snvonmbl	|- ( ( ph /\ x e. A ) -> { x } e. dom ( voln ` X ) )
14		sndisj	|- Disj_ x e. A { x }
15	14	a1i	|- ( ph -> Disj_ x e. A { x } )
16	8 9 10 13 3 15	meadjiun	|- ( ph -> ( ( voln ` X ) ` U_ x e. A { x } ) = ( sum^ ` ( x e. A |-> ( ( voln ` X ) ` { x } ) ) ) )
17	11 12	vonsn	|- ( ( ph /\ x e. A ) -> ( ( voln ` X ) ` { x } ) = 0 )
18	17	mpteq2dva	|- ( ph -> ( x e. A |-> ( ( voln ` X ) ` { x } ) ) = ( x e. A |-> 0 ) )
19	18	fveq2d	|- ( ph -> ( sum^ ` ( x e. A |-> ( ( voln ` X ) ` { x } ) ) ) = ( sum^ ` ( x e. A |-> 0 ) ) )
20	9 10	dmmeasal	|- ( ph -> dom ( voln ` X ) e. SAlg )
21	20 3 13	saliuncl	|- ( ph -> U_ x e. A { x } e. dom ( voln ` X ) )
22	4 21	eqeltrrid	|- ( ph -> A e. dom ( voln ` X ) )
23	8 22	sge0z	|- ( ph -> ( sum^ ` ( x e. A |-> 0 ) ) = 0 )
24	19 23	eqtrd	|- ( ph -> ( sum^ ` ( x e. A |-> ( ( voln ` X ) ` { x } ) ) ) = 0 )
25	7 16 24	3eqtrd	|- ( ph -> ( ( voln ` X ) ` A ) = 0 )