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 φ X Fin
ctvonmbl.2 φ A X
ctvonmbl.3 φ A ω
Assertion ctvonmbl φ A dom voln X

Proof

Step Hyp Ref Expression
1 ctvonmbl.1 φ X Fin
2 ctvonmbl.2 φ A X
3 ctvonmbl.3 φ A ω
4 iunid x A x = A
5 1 vonmea φ voln X Meas
6 eqid dom voln X = dom voln X
7 5 6 dmmeasal φ dom voln X SAlg
8 1 adantr φ x A X Fin
9 2 sselda φ x A x X
10 8 9 snvonmbl φ x A x dom voln X
11 7 3 10 saliuncl φ x A x dom voln X
12 4 11 eqeltrrid φ A dom voln X