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	$$⊢\mathrm{dom}vol\subset 𝒫ℝ$$

Proof

Step	Hyp	Ref	Expression
1		reex	$$⊢ℝ\in \mathrm{V}$$
2		weth	$$⊢ℝ\in \mathrm{V}\to \exists oo\mathrm{We}ℝ$$
3	1 2	ax-mp	$$⊢\exists oo\mathrm{We}ℝ$$
4		vitali	$$⊢o\mathrm{We}ℝ\to \mathrm{dom}vol\subset 𝒫ℝ$$
5	4	exlimiv	$$⊢\exists oo\mathrm{We}ℝ\to \mathrm{dom}vol\subset 𝒫ℝ$$
6	3 5	ax-mp	$$⊢\mathrm{dom}vol\subset 𝒫ℝ$$