Metamath Proof Explorer


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 φXFin
ctvonmbl.2 φAX
ctvonmbl.3 φAω
Assertion ctvonmbl φAdomvolnX

Proof

Step Hyp Ref Expression
1 ctvonmbl.1 φXFin
2 ctvonmbl.2 φAX
3 ctvonmbl.3 φAω
4 iunid xAx=A
5 1 vonmea φvolnXMeas
6 eqid domvolnX=domvolnX
7 5 6 dmmeasal φdomvolnXSAlg
8 1 adantr φxAXFin
9 2 sselda φxAxX
10 8 9 snvonmbl φxAxdomvolnX
11 7 3 10 saliuncl φxAxdomvolnX
12 4 11 eqeltrrid φAdomvolnX