Metamath Proof Explorer


Theorem snvonmbl

Description: A n-dimensional singleton is Lebesgue measurable. This is the first statement in Proposition 115G (e) of Fremlin1 p. 32. (Contributed by Glauco Siliprandi, 8-Apr-2021)

Ref Expression
Hypotheses snvonmbl.1 φ X Fin
snvonmbl.2 φ A X
Assertion snvonmbl φ A dom voln X

Proof

Step Hyp Ref Expression
1 snvonmbl.1 φ X Fin
2 snvonmbl.2 φ A X
3 2 rrxsnicc φ k X A k A k = A
4 3 eqcomd φ A = k X A k A k
5 eqid dom voln X = dom voln X
6 elmapi A X A : X
7 2 6 syl φ A : X
8 1 5 7 7 iccvonmbl φ k X A k A k dom voln X
9 4 8 eqeltrd φ A dom voln X