# Metamath Proof Explorer

## Theorem vitalilem3

Description: Lemma for vitali . (Contributed by Mario Carneiro, 16-Jun-2014)

Ref Expression
Hypotheses vitali.1
vitali.2
vitali.3 ${⊢}{\phi }\to {F}Fn{S}$
vitali.4 ${⊢}{\phi }\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {F}\left({z}\right)\in {z}\right)$
vitali.5 ${⊢}{\phi }\to {G}:ℕ\underset{1-1 onto}{⟶}ℚ\cap \left[-1,1\right]$
vitali.6 ${⊢}{T}=\left({n}\in ℕ⟼\left\{{s}\in ℝ|{s}-{G}\left({n}\right)\in \mathrm{ran}{F}\right\}\right)$
vitali.7 ${⊢}{\phi }\to ¬\mathrm{ran}{F}\in \left(𝒫ℝ\setminus \mathrm{dom}vol\right)$
Assertion vitalilem3 ${⊢}{\phi }\to \underset{{m}\in ℕ}{Disj}{T}\left({m}\right)$

### Proof

Step Hyp Ref Expression
1 vitali.1
2 vitali.2
3 vitali.3 ${⊢}{\phi }\to {F}Fn{S}$
4 vitali.4 ${⊢}{\phi }\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {F}\left({z}\right)\in {z}\right)$
5 vitali.5 ${⊢}{\phi }\to {G}:ℕ\underset{1-1 onto}{⟶}ℚ\cap \left[-1,1\right]$
6 vitali.6 ${⊢}{T}=\left({n}\in ℕ⟼\left\{{s}\in ℝ|{s}-{G}\left({n}\right)\in \mathrm{ran}{F}\right\}\right)$
7 vitali.7 ${⊢}{\phi }\to ¬\mathrm{ran}{F}\in \left(𝒫ℝ\setminus \mathrm{dom}vol\right)$
8 simprlr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {w}\in {T}\left({m}\right)$
9 simprll ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {m}\in ℕ$
10 fveq2 ${⊢}{n}={m}\to {G}\left({n}\right)={G}\left({m}\right)$
11 10 oveq2d ${⊢}{n}={m}\to {s}-{G}\left({n}\right)={s}-{G}\left({m}\right)$
12 11 eleq1d ${⊢}{n}={m}\to \left({s}-{G}\left({n}\right)\in \mathrm{ran}{F}↔{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right)$
13 12 rabbidv ${⊢}{n}={m}\to \left\{{s}\in ℝ|{s}-{G}\left({n}\right)\in \mathrm{ran}{F}\right\}=\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}$
14 reex ${⊢}ℝ\in \mathrm{V}$
15 14 rabex ${⊢}\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}\in \mathrm{V}$
16 13 6 15 fvmpt ${⊢}{m}\in ℕ\to {T}\left({m}\right)=\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}$
17 9 16 syl ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {T}\left({m}\right)=\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}$
18 8 17 eleqtrd ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {w}\in \left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}$
19 oveq1 ${⊢}{s}={w}\to {s}-{G}\left({m}\right)={w}-{G}\left({m}\right)$
20 19 eleq1d ${⊢}{s}={w}\to \left({s}-{G}\left({m}\right)\in \mathrm{ran}{F}↔{w}-{G}\left({m}\right)\in \mathrm{ran}{F}\right)$
21 20 elrab ${⊢}{w}\in \left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}↔\left({w}\in ℝ\wedge {w}-{G}\left({m}\right)\in \mathrm{ran}{F}\right)$
22 18 21 sylib ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to \left({w}\in ℝ\wedge {w}-{G}\left({m}\right)\in \mathrm{ran}{F}\right)$
23 22 simpld ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {w}\in ℝ$
24 23 recnd ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {w}\in ℂ$
25 f1of ${⊢}{G}:ℕ\underset{1-1 onto}{⟶}ℚ\cap \left[-1,1\right]\to {G}:ℕ⟶ℚ\cap \left[-1,1\right]$
26 5 25 syl ${⊢}{\phi }\to {G}:ℕ⟶ℚ\cap \left[-1,1\right]$
27 inss1 ${⊢}ℚ\cap \left[-1,1\right]\subseteq ℚ$
28 fss ${⊢}\left({G}:ℕ⟶ℚ\cap \left[-1,1\right]\wedge ℚ\cap \left[-1,1\right]\subseteq ℚ\right)\to {G}:ℕ⟶ℚ$
29 26 27 28 sylancl ${⊢}{\phi }\to {G}:ℕ⟶ℚ$
30 29 adantr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {G}:ℕ⟶ℚ$
31 30 9 ffvelrnd ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {G}\left({m}\right)\in ℚ$
32 qcn ${⊢}{G}\left({m}\right)\in ℚ\to {G}\left({m}\right)\in ℂ$
33 31 32 syl ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {G}\left({m}\right)\in ℂ$
34 simprrl ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {k}\in ℕ$
35 30 34 ffvelrnd ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {G}\left({k}\right)\in ℚ$
36 qcn ${⊢}{G}\left({k}\right)\in ℚ\to {G}\left({k}\right)\in ℂ$
37 35 36 syl ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {G}\left({k}\right)\in ℂ$
38 1 vitalilem1
39 38 a1i
40 1 2 3 4 5 6 7 vitalilem2 ${⊢}{\phi }\to \left(\mathrm{ran}{F}\subseteq \left[0,1\right]\wedge \left[0,1\right]\subseteq \bigcup _{{m}\in ℕ}{T}\left({m}\right)\wedge \bigcup _{{m}\in ℕ}{T}\left({m}\right)\subseteq \left[-1,2\right]\right)$
41 40 simp1d ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq \left[0,1\right]$
42 41 adantr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to \mathrm{ran}{F}\subseteq \left[0,1\right]$
43 22 simprd ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {w}-{G}\left({m}\right)\in \mathrm{ran}{F}$
44 42 43 sseldd ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {w}-{G}\left({m}\right)\in \left[0,1\right]$
45 simprrr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {w}\in {T}\left({k}\right)$
46 fveq2 ${⊢}{n}={k}\to {G}\left({n}\right)={G}\left({k}\right)$
47 46 oveq2d ${⊢}{n}={k}\to {s}-{G}\left({n}\right)={s}-{G}\left({k}\right)$
48 47 eleq1d ${⊢}{n}={k}\to \left({s}-{G}\left({n}\right)\in \mathrm{ran}{F}↔{s}-{G}\left({k}\right)\in \mathrm{ran}{F}\right)$
49 48 rabbidv ${⊢}{n}={k}\to \left\{{s}\in ℝ|{s}-{G}\left({n}\right)\in \mathrm{ran}{F}\right\}=\left\{{s}\in ℝ|{s}-{G}\left({k}\right)\in \mathrm{ran}{F}\right\}$
50 14 rabex ${⊢}\left\{{s}\in ℝ|{s}-{G}\left({k}\right)\in \mathrm{ran}{F}\right\}\in \mathrm{V}$
51 49 6 50 fvmpt ${⊢}{k}\in ℕ\to {T}\left({k}\right)=\left\{{s}\in ℝ|{s}-{G}\left({k}\right)\in \mathrm{ran}{F}\right\}$
52 34 51 syl ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {T}\left({k}\right)=\left\{{s}\in ℝ|{s}-{G}\left({k}\right)\in \mathrm{ran}{F}\right\}$
53 45 52 eleqtrd ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {w}\in \left\{{s}\in ℝ|{s}-{G}\left({k}\right)\in \mathrm{ran}{F}\right\}$
54 oveq1 ${⊢}{s}={w}\to {s}-{G}\left({k}\right)={w}-{G}\left({k}\right)$
55 54 eleq1d ${⊢}{s}={w}\to \left({s}-{G}\left({k}\right)\in \mathrm{ran}{F}↔{w}-{G}\left({k}\right)\in \mathrm{ran}{F}\right)$
56 55 elrab ${⊢}{w}\in \left\{{s}\in ℝ|{s}-{G}\left({k}\right)\in \mathrm{ran}{F}\right\}↔\left({w}\in ℝ\wedge {w}-{G}\left({k}\right)\in \mathrm{ran}{F}\right)$
57 53 56 sylib ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to \left({w}\in ℝ\wedge {w}-{G}\left({k}\right)\in \mathrm{ran}{F}\right)$
58 57 simprd ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {w}-{G}\left({k}\right)\in \mathrm{ran}{F}$
59 42 58 sseldd ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {w}-{G}\left({k}\right)\in \left[0,1\right]$
60 24 33 37 nnncan1d ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {w}-{G}\left({m}\right)-\left({w}-{G}\left({k}\right)\right)={G}\left({k}\right)-{G}\left({m}\right)$
61 qsubcl ${⊢}\left({G}\left({k}\right)\in ℚ\wedge {G}\left({m}\right)\in ℚ\right)\to {G}\left({k}\right)-{G}\left({m}\right)\in ℚ$
62 35 31 61 syl2anc ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {G}\left({k}\right)-{G}\left({m}\right)\in ℚ$
63 60 62 eqeltrd ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {w}-{G}\left({m}\right)-\left({w}-{G}\left({k}\right)\right)\in ℚ$
64 oveq12 ${⊢}\left({x}={w}-{G}\left({m}\right)\wedge {y}={w}-{G}\left({k}\right)\right)\to {x}-{y}={w}-{G}\left({m}\right)-\left({w}-{G}\left({k}\right)\right)$
65 64 eleq1d ${⊢}\left({x}={w}-{G}\left({m}\right)\wedge {y}={w}-{G}\left({k}\right)\right)\to \left({x}-{y}\in ℚ↔{w}-{G}\left({m}\right)-\left({w}-{G}\left({k}\right)\right)\in ℚ\right)$
66 65 1 brab2a
67 44 59 63 66 syl21anbrc
68 39 67 erthi
69 68 fveq2d
70 eceq1
71 70 fveq2d
72 id ${⊢}{z}={w}-{G}\left({m}\right)\to {z}={w}-{G}\left({m}\right)$
73 71 72 eqeq12d
74 fveq2
75 74 eceq1d
76 75 fveq2d
77 76 74 eqeq12d
78 38 a1i
79 simpr ${⊢}\left({\phi }\wedge {v}\in \left[0,1\right]\right)\to {v}\in \left[0,1\right]$
80 erdm
81 38 80 ax-mp
82 81 eleq2i
83 ecdmn0
84 82 83 bitr3i
85 79 84 sylib
86 neeq1
87 fveq2
88 id
89 87 88 eleq12d
90 86 89 imbi12d
91 4 adantr ${⊢}\left({\phi }\wedge {v}\in \left[0,1\right]\right)\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {F}\left({z}\right)\in {z}\right)$
92 ovex ${⊢}\left[0,1\right]\in \mathrm{V}$
93 erex
94 38 92 93 mp2
95 94 ecelqsi
96 95 2 eleqtrrdi
98 90 91 97 rspcdva
99 85 98 mpd
100 fvex
101 vex ${⊢}{v}\in \mathrm{V}$
102 100 101 elec
103 99 102 sylib
104 78 103 erthi
105 104 eqcomd
106 105 fveq2d
107 2 77 106 ectocld
108 107 ralrimiva
109 eceq1
110 109 fveq2d
111 id ${⊢}{z}={F}\left({w}\right)\to {z}={F}\left({w}\right)$
112 110 111 eqeq12d
113 112 ralrn
114 3 113 syl
115 108 114 mpbird
117 73 116 43 rspcdva
118 eceq1
119 118 fveq2d
120 id ${⊢}{z}={w}-{G}\left({k}\right)\to {z}={w}-{G}\left({k}\right)$
121 119 120 eqeq12d
122 121 116 58 rspcdva
123 69 117 122 3eqtr3d ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {w}-{G}\left({m}\right)={w}-{G}\left({k}\right)$
124 24 33 37 123 subcand ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {G}\left({m}\right)={G}\left({k}\right)$
125 5 adantr ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {G}:ℕ\underset{1-1 onto}{⟶}ℚ\cap \left[-1,1\right]$
126 f1of1 ${⊢}{G}:ℕ\underset{1-1 onto}{⟶}ℚ\cap \left[-1,1\right]\to {G}:ℕ\underset{1-1}{⟶}ℚ\cap \left[-1,1\right]$
127 125 126 syl ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {G}:ℕ\underset{1-1}{⟶}ℚ\cap \left[-1,1\right]$
128 f1fveq ${⊢}\left({G}:ℕ\underset{1-1}{⟶}ℚ\cap \left[-1,1\right]\wedge \left({m}\in ℕ\wedge {k}\in ℕ\right)\right)\to \left({G}\left({m}\right)={G}\left({k}\right)↔{m}={k}\right)$
129 127 9 34 128 syl12anc ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to \left({G}\left({m}\right)={G}\left({k}\right)↔{m}={k}\right)$
130 124 129 mpbid ${⊢}\left({\phi }\wedge \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\right)\to {m}={k}$
131 130 ex ${⊢}{\phi }\to \left(\left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\to {m}={k}\right)$
132 131 alrimivv ${⊢}{\phi }\to \forall {m}\phantom{\rule{.4em}{0ex}}\forall {k}\phantom{\rule{.4em}{0ex}}\left(\left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\to {m}={k}\right)$
133 eleq1w ${⊢}{m}={k}\to \left({m}\in ℕ↔{k}\in ℕ\right)$
134 fveq2 ${⊢}{m}={k}\to {T}\left({m}\right)={T}\left({k}\right)$
135 134 eleq2d ${⊢}{m}={k}\to \left({w}\in {T}\left({m}\right)↔{w}\in {T}\left({k}\right)\right)$
136 133 135 anbi12d ${⊢}{m}={k}\to \left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)↔\left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)$
137 136 mo4 ${⊢}{\exists }^{*}{m}\phantom{\rule{.4em}{0ex}}\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)↔\forall {m}\phantom{\rule{.4em}{0ex}}\forall {k}\phantom{\rule{.4em}{0ex}}\left(\left(\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)\wedge \left({k}\in ℕ\wedge {w}\in {T}\left({k}\right)\right)\right)\to {m}={k}\right)$
138 132 137 sylibr ${⊢}{\phi }\to {\exists }^{*}{m}\phantom{\rule{.4em}{0ex}}\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)$
139 138 alrimiv ${⊢}{\phi }\to \forall {w}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{m}\phantom{\rule{.4em}{0ex}}\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)$
140 dfdisj2 ${⊢}\underset{{m}\in ℕ}{Disj}{T}\left({m}\right)↔\forall {w}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{m}\phantom{\rule{.4em}{0ex}}\left({m}\in ℕ\wedge {w}\in {T}\left({m}\right)\right)$
141 139 140 sylibr ${⊢}{\phi }\to \underset{{m}\in ℕ}{Disj}{T}\left({m}\right)$