vitali

Description: If the reals can be well-ordered, then there are non-measurable sets. The proof uses "Vitali sets", named for Giuseppe Vitali (1905). (Contributed by Mario Carneiro, 16-Jun-2014)

		Ref	Expression
	Assertion	vitali	$⊢ \underset{˙}{<} We ℝ \to dom vol \subset 𝒫 ℝ$

Proof

Step	Hyp	Ref	Expression
1		reex	$⊢ ℝ \in V$
2	1	pwex	$⊢ 𝒫 ℝ \in V$
3		weinxp	$⊢ \underset{˙}{<} We ℝ \leftrightarrow (\underset{˙}{<} \cap ℝ^{2}) We ℝ$
4		unipw	$⊢ ⋃ 𝒫 ℝ = ℝ$
5		weeq2	$⊢ ⋃ 𝒫 ℝ = ℝ \to ((\underset{˙}{<} \cap ℝ^{2}) We ⋃ 𝒫 ℝ \leftrightarrow (\underset{˙}{<} \cap ℝ^{2}) We ℝ)$
6	4 5	ax-mp	$⊢ (\underset{˙}{<} \cap ℝ^{2}) We ⋃ 𝒫 ℝ \leftrightarrow (\underset{˙}{<} \cap ℝ^{2}) We ℝ$
7	3 6	bitr4i	$⊢ \underset{˙}{<} We ℝ \leftrightarrow (\underset{˙}{<} \cap ℝ^{2}) We ⋃ 𝒫 ℝ$
8	1 1	xpex	$⊢ ℝ^{2} \in V$
9	8	inex2	$⊢ \underset{˙}{<} \cap ℝ^{2} \in V$
10		weeq1	$⊢ x = \underset{˙}{<} \cap ℝ^{2} \to (x We ⋃ 𝒫 ℝ \leftrightarrow (\underset{˙}{<} \cap ℝ^{2}) We ⋃ 𝒫 ℝ)$
11	9 10	spcev	$⊢ (\underset{˙}{<} \cap ℝ^{2}) We ⋃ 𝒫 ℝ \to \exists x x We ⋃ 𝒫 ℝ$
12	7 11	sylbi	$⊢ \underset{˙}{<} We ℝ \to \exists x x We ⋃ 𝒫 ℝ$
13		dfac8c	$⊢ 𝒫 ℝ \in V \to (\exists x x We ⋃ 𝒫 ℝ \to \exists f \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z))$
14	2 12 13	mpsyl	$⊢ \underset{˙}{<} We ℝ \to \exists f \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z)$
15		qex	$⊢ ℚ \in V$
16	15	inex1	$⊢ ℚ \cap [- 1, 1] \in V$
17		nnrecq	$⊢ x \in ℕ \to \frac{1}{x} \in ℚ$
18		nnrecre	$⊢ x \in ℕ \to \frac{1}{x} \in ℝ$
19		neg1rr	$⊢ - 1 \in ℝ$
20	19	a1i	$⊢ x \in ℕ \to - 1 \in ℝ$
21		0re	$⊢ 0 \in ℝ$
22	21	a1i	$⊢ x \in ℕ \to 0 \in ℝ$
23		neg1lt0	$⊢ - 1 < 0$
24	19 21 23	ltleii	$⊢ - 1 \leq 0$
25	24	a1i	$⊢ x \in ℕ \to - 1 \leq 0$
26		nnrp	$⊢ x \in ℕ \to x \in ℝ^{+}$
27	26	rpreccld	$⊢ x \in ℕ \to \frac{1}{x} \in ℝ^{+}$
28	27	rpge0d	$⊢ x \in ℕ \to 0 \leq \frac{1}{x}$
29	20 22 18 25 28	letrd	$⊢ x \in ℕ \to - 1 \leq \frac{1}{x}$
30		nnge1	$⊢ x \in ℕ \to 1 \leq x$
31		nnre	$⊢ x \in ℕ \to x \in ℝ$
32		nngt0	$⊢ x \in ℕ \to 0 < x$
33		1re	$⊢ 1 \in ℝ$
34		0lt1	$⊢ 0 < 1$
35		lerec	$⊢ ((1 \in ℝ \land 0 < 1) \land (x \in ℝ \land 0 < x)) \to (1 \leq x \leftrightarrow \frac{1}{x} \leq \frac{1}{1})$
36	33 34 35	mpanl12	$⊢ (x \in ℝ \land 0 < x) \to (1 \leq x \leftrightarrow \frac{1}{x} \leq \frac{1}{1})$
37	31 32 36	syl2anc	$⊢ x \in ℕ \to (1 \leq x \leftrightarrow \frac{1}{x} \leq \frac{1}{1})$
38	30 37	mpbid	$⊢ x \in ℕ \to \frac{1}{x} \leq \frac{1}{1}$
39		1div1e1	$⊢ \frac{1}{1} = 1$
40	38 39	breqtrdi	$⊢ x \in ℕ \to \frac{1}{x} \leq 1$
41	19 33	elicc2i	$⊢ \frac{1}{x} \in [- 1, 1] \leftrightarrow (\frac{1}{x} \in ℝ \land - 1 \leq \frac{1}{x} \land \frac{1}{x} \leq 1)$
42	18 29 40 41	syl3anbrc	$⊢ x \in ℕ \to \frac{1}{x} \in [- 1, 1]$
43	17 42	elind	$⊢ x \in ℕ \to \frac{1}{x} \in (ℚ \cap [- 1, 1])$
44		oveq2	$⊢ \frac{1}{x} = \frac{1}{y} \to \frac{1}{\frac{1}{x}} = \frac{1}{\frac{1}{y}}$
45		nncn	$⊢ x \in ℕ \to x \in ℂ$
46		nnne0	$⊢ x \in ℕ \to x \neq 0$
47	45 46	recrecd	$⊢ x \in ℕ \to \frac{1}{\frac{1}{x}} = x$
48		nncn	$⊢ y \in ℕ \to y \in ℂ$
49		nnne0	$⊢ y \in ℕ \to y \neq 0$
50	48 49	recrecd	$⊢ y \in ℕ \to \frac{1}{\frac{1}{y}} = y$
51	47 50	eqeqan12d	$⊢ (x \in ℕ \land y \in ℕ) \to (\frac{1}{\frac{1}{x}} = \frac{1}{\frac{1}{y}} \leftrightarrow x = y)$
52	44 51	imbitrid	$⊢ (x \in ℕ \land y \in ℕ) \to (\frac{1}{x} = \frac{1}{y} \to x = y)$
53		oveq2	$⊢ x = y \to \frac{1}{x} = \frac{1}{y}$
54	52 53	impbid1	$⊢ (x \in ℕ \land y \in ℕ) \to (\frac{1}{x} = \frac{1}{y} \leftrightarrow x = y)$
55	43 54	dom2	$⊢ ℚ \cap [- 1, 1] \in V \to ℕ ≼ (ℚ \cap [- 1, 1])$
56	16 55	ax-mp	$⊢ ℕ ≼ (ℚ \cap [- 1, 1])$
57		inss1	$⊢ ℚ \cap [- 1, 1] \subseteq ℚ$
58		ssdomg	$⊢ ℚ \in V \to (ℚ \cap [- 1, 1] \subseteq ℚ \to (ℚ \cap [- 1, 1]) ≼ ℚ)$
59	15 57 58	mp2	$⊢ (ℚ \cap [- 1, 1]) ≼ ℚ$
60		qnnen	$⊢ ℚ \approx ℕ$
61		domentr	$⊢ ((ℚ \cap [- 1, 1]) ≼ ℚ \land ℚ \approx ℕ) \to (ℚ \cap [- 1, 1]) ≼ ℕ$
62	59 60 61	mp2an	$⊢ (ℚ \cap [- 1, 1]) ≼ ℕ$
63		sbth	$⊢ (ℕ ≼ (ℚ \cap [- 1, 1]) \land (ℚ \cap [- 1, 1]) ≼ ℕ) \to ℕ \approx (ℚ \cap [- 1, 1])$
64	56 62 63	mp2an	$⊢ ℕ \approx (ℚ \cap [- 1, 1])$
65		bren	$⊢ ℕ \approx (ℚ \cap [- 1, 1]) \leftrightarrow \exists g g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1]$
66	64 65	mpbi	$⊢ \exists g g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1]$
67		eleq1w	$⊢ a = x \to (a \in [0, 1] \leftrightarrow x \in [0, 1])$
68		eleq1w	$⊢ b = y \to (b \in [0, 1] \leftrightarrow y \in [0, 1])$
69	67 68	bi2anan9	$⊢ (a = x \land b = y) \to ((a \in [0, 1] \land b \in [0, 1]) \leftrightarrow (x \in [0, 1] \land y \in [0, 1]))$
70		oveq12	$⊢ (a = x \land b = y) \to a - b = x - y$
71	70	eleq1d	$⊢ (a = x \land b = y) \to (a - b \in ℚ \leftrightarrow x - y \in ℚ)$
72	69 71	anbi12d	$⊢ (a = x \land b = y) \to (((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ) \leftrightarrow ((x \in [0, 1] \land y \in [0, 1]) \land x - y \in ℚ))$
73	72	cbvopabv	$⊢ \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\} = \{⟨x, y⟩ \| ((x \in [0, 1] \land y \in [0, 1]) \land x - y \in ℚ)\}$
74		eqid	$⊢ [0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\} = [0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}$
75		fvex	$⊢ f (c) \in V$
76		eqid	$⊢ (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) = (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c))$
77	75 76	fnmpti	$⊢ (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) Fn ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\})$
78	77	a1i	$⊢ ((\underset{˙}{<} We ℝ \land \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z)) \land (g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \land \neg ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in (𝒫 ℝ ∖ dom vol))) \to (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) Fn ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\})$
79		neeq1	$⊢ z = w \to (z \neq \emptyset \leftrightarrow w \neq \emptyset)$
80		fveq2	$⊢ z = w \to f (z) = f (w)$
81		id	$⊢ z = w \to z = w$
82	80 81	eleq12d	$⊢ z = w \to (f (z) \in z \leftrightarrow f (w) \in w)$
83	79 82	imbi12d	$⊢ z = w \to ((z \neq \emptyset \to f (z) \in z) \leftrightarrow (w \neq \emptyset \to f (w) \in w))$
84	83	cbvralvw	$⊢ \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z) \leftrightarrow \forall w \in 𝒫 ℝ (w \neq \emptyset \to f (w) \in w)$
85	73	vitalilem1	$⊢ \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\} Er [0, 1]$
86	85	a1i	$⊢ ⊤ \to \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\} Er [0, 1]$
87	86	qsss	$⊢ ⊤ \to [0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\} \subseteq 𝒫 [0, 1]$
88	87	mptru	$⊢ [0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\} \subseteq 𝒫 [0, 1]$
89		unitssre	$⊢ [0, 1] \subseteq ℝ$
90	89	sspwi	$⊢ 𝒫 [0, 1] \subseteq 𝒫 ℝ$
91	88 90	sstri	$⊢ [0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\} \subseteq 𝒫 ℝ$
92		ssralv	$⊢ [0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\} \subseteq 𝒫 ℝ \to (\forall w \in 𝒫 ℝ (w \neq \emptyset \to f (w) \in w) \to \forall w \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) (w \neq \emptyset \to f (w) \in w))$
93	91 92	ax-mp	$⊢ \forall w \in 𝒫 ℝ (w \neq \emptyset \to f (w) \in w) \to \forall w \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) (w \neq \emptyset \to f (w) \in w)$
94	84 93	sylbi	$⊢ \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z) \to \forall w \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) (w \neq \emptyset \to f (w) \in w)$
95		fveq2	$⊢ c = w \to f (c) = f (w)$
96		fvex	$⊢ f (w) \in V$
97	95 76 96	fvmpt	$⊢ w \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) \to (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) (w) = f (w)$
98	97	eleq1d	$⊢ w \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) \to ((c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) (w) \in w \leftrightarrow f (w) \in w)$
99	98	imbi2d	$⊢ w \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) \to ((w \neq \emptyset \to (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) (w) \in w) \leftrightarrow (w \neq \emptyset \to f (w) \in w))$
100	99	ralbiia	$⊢ \forall w \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) (w \neq \emptyset \to (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) (w) \in w) \leftrightarrow \forall w \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) (w \neq \emptyset \to f (w) \in w)$
101	94 100	sylibr	$⊢ \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z) \to \forall w \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) (w \neq \emptyset \to (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) (w) \in w)$
102	101	ad2antlr	$⊢ ((\underset{˙}{<} We ℝ \land \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z)) \land (g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \land \neg ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in (𝒫 ℝ ∖ dom vol))) \to \forall w \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) (w \neq \emptyset \to (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) (w) \in w)$
103		simprl	$⊢ ((\underset{˙}{<} We ℝ \land \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z)) \land (g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \land \neg ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in (𝒫 ℝ ∖ dom vol))) \to g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1]$
104		oveq1	$⊢ t = s \to t - g (m) = s - g (m)$
105	104	eleq1d	$⊢ t = s \to (t - g (m) \in ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \leftrightarrow s - g (m) \in ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)))$
106	105	cbvrabv	$⊢ \{t \in ℝ \| t - g (m) \in ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c))\} = \{s \in ℝ \| s - g (m) \in ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c))\}$
107		fveq2	$⊢ m = n \to g (m) = g (n)$
108	107	oveq2d	$⊢ m = n \to s - g (m) = s - g (n)$
109	108	eleq1d	$⊢ m = n \to (s - g (m) \in ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \leftrightarrow s - g (n) \in ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)))$
110	109	rabbidv	$⊢ m = n \to \{s \in ℝ \| s - g (m) \in ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c))\} = \{s \in ℝ \| s - g (n) \in ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c))\}$
111	106 110	eqtrid	$⊢ m = n \to \{t \in ℝ \| t - g (m) \in ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c))\} = \{s \in ℝ \| s - g (n) \in ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c))\}$
112	111	cbvmptv	$⊢ (m \in ℕ ⟼ \{t \in ℝ \| t - g (m) \in ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c))\}) = (n \in ℕ ⟼ \{s \in ℝ \| s - g (n) \in ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c))\})$
113		simprr	$⊢ ((\underset{˙}{<} We ℝ \land \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z)) \land (g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \land \neg ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in (𝒫 ℝ ∖ dom vol))) \to \neg ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in (𝒫 ℝ ∖ dom vol)$
114	73 74 78 102 103 112 113	vitalilem5	$⊢ \neg ((\underset{˙}{<} We ℝ \land \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z)) \land (g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \land \neg ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in (𝒫 ℝ ∖ dom vol)))$
115	114	pm2.21i	$⊢ ((\underset{˙}{<} We ℝ \land \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z)) \land (g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \land \neg ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in (𝒫 ℝ ∖ dom vol))) \to ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in (𝒫 ℝ ∖ dom vol)$
116	115	expr	$⊢ ((\underset{˙}{<} We ℝ \land \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z)) \land g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1]) \to (\neg ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in (𝒫 ℝ ∖ dom vol) \to ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in (𝒫 ℝ ∖ dom vol))$
117	116	pm2.18d	$⊢ ((\underset{˙}{<} We ℝ \land \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z)) \land g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1]) \to ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in (𝒫 ℝ ∖ dom vol)$
118		eldif	$⊢ ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in (𝒫 ℝ ∖ dom vol) \leftrightarrow (ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in 𝒫 ℝ \land \neg ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in dom vol)$
119		mblss	$⊢ x \in dom vol \to x \subseteq ℝ$
120		velpw	$⊢ x \in 𝒫 ℝ \leftrightarrow x \subseteq ℝ$
121	119 120	sylibr	$⊢ x \in dom vol \to x \in 𝒫 ℝ$
122	121	ssriv	$⊢ dom vol \subseteq 𝒫 ℝ$
123		ssnelpss	$⊢ dom vol \subseteq 𝒫 ℝ \to ((ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in 𝒫 ℝ \land \neg ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in dom vol) \to dom vol \subset 𝒫 ℝ)$
124	122 123	ax-mp	$⊢ (ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in 𝒫 ℝ \land \neg ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in dom vol) \to dom vol \subset 𝒫 ℝ$
125	118 124	sylbi	$⊢ ran (c \in ([0, 1] / \{⟨a, b⟩ \| ((a \in [0, 1] \land b \in [0, 1]) \land a - b \in ℚ)\}) ⟼ f (c)) \in (𝒫 ℝ ∖ dom vol) \to dom vol \subset 𝒫 ℝ$
126	117 125	syl	$⊢ ((\underset{˙}{<} We ℝ \land \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z)) \land g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1]) \to dom vol \subset 𝒫 ℝ$
127	126	ex	$⊢ (\underset{˙}{<} We ℝ \land \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z)) \to (g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \to dom vol \subset 𝒫 ℝ)$
128	127	exlimdv	$⊢ (\underset{˙}{<} We ℝ \land \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z)) \to (\exists g g : ℕ \underset{1-1 onto}{⟶} ℚ \cap [- 1, 1] \to dom vol \subset 𝒫 ℝ)$
129	66 128	mpi	$⊢ (\underset{˙}{<} We ℝ \land \forall z \in 𝒫 ℝ (z \neq \emptyset \to f (z) \in z)) \to dom vol \subset 𝒫 ℝ$
130	14 129	exlimddv	$⊢ \underset{˙}{<} We ℝ \to dom vol \subset 𝒫 ℝ$

Metamath Proof Explorer

Theorem vitali

Proof