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 C. ~P RR

Proof

Step Hyp Ref Expression
1 reex 
 |-  RR e. _V
2 weth 
 |-  ( RR e. _V -> E. o o We RR )
3 1 2 ax-mp 
 |-  E. o o We RR
4 vitali 
 |-  ( o We RR -> dom vol C. ~P RR )
5 4 exlimiv 
 |-  ( E. o o We RR -> dom vol C. ~P RR )
6 3 5 ax-mp 
 |-  dom vol C. ~P RR