Metamath Proof Explorer


Theorem vitali2

Description: There are non-measurable sets (the Axiom of Choice is used, in the invoked weth ). (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Assertion vitali2 dom vol 𝒫

Proof

Step Hyp Ref Expression
1 reex V
2 weth V o o We
3 1 2 ax-mp o o We
4 vitali o We dom vol 𝒫
5 4 exlimiv o o We dom vol 𝒫
6 3 5 ax-mp dom vol 𝒫