Metamath Proof Explorer


Theorem unidmovn

Description: Base set of the n-dimensional Lebesgue outer measure. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypothesis unidmovn.1 φ X Fin
Assertion unidmovn φ dom voln* X = X

Proof

Step Hyp Ref Expression
1 unidmovn.1 φ X Fin
2 1 dmovn φ dom voln* X = 𝒫 X
3 2 unieqd φ dom voln* X = 𝒫 X
4 unipw 𝒫 X = X
5 4 a1i φ 𝒫 X = X
6 3 5 eqtrd φ dom voln* X = X