# Metamath Proof Explorer

## Theorem 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

### Proof

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