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 → ∃ 𝑜 𝑜 We ℝ )
3	1 2	ax-mp	⊢ ∃ 𝑜 𝑜 We ℝ
4		vitali	⊢ ( 𝑜 We ℝ → dom vol ⊊ 𝒫 ℝ )
5	4	exlimiv	⊢ ( ∃ 𝑜 𝑜 We ℝ → dom vol ⊊ 𝒫 ℝ )
6	3 5	ax-mp	⊢ dom vol ⊊ 𝒫 ℝ