# Metamath Proof Explorer

## Theorem vitalilem2

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 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)$

### 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 neeq1
9 1 vitalilem1
10 erdm
11 9 10 ax-mp
12 11 eleq2i
13 ecdmn0
14 12 13 bitr3i
15 14 biimpi
16 2 8 15 ectocl ${⊢}{z}\in {S}\to {z}\ne \varnothing$
17 16 adantl ${⊢}\left({\phi }\wedge {z}\in {S}\right)\to {z}\ne \varnothing$
18 sseq1
19 9 a1i
20 19 ecss
21 2 18 20 ectocl ${⊢}{z}\in {S}\to {z}\subseteq \left[0,1\right]$
22 21 adantl ${⊢}\left({\phi }\wedge {z}\in {S}\right)\to {z}\subseteq \left[0,1\right]$
23 22 sseld ${⊢}\left({\phi }\wedge {z}\in {S}\right)\to \left({F}\left({z}\right)\in {z}\to {F}\left({z}\right)\in \left[0,1\right]\right)$
24 17 23 embantd ${⊢}\left({\phi }\wedge {z}\in {S}\right)\to \left(\left({z}\ne \varnothing \to {F}\left({z}\right)\in {z}\right)\to {F}\left({z}\right)\in \left[0,1\right]\right)$
25 24 ralimdva ${⊢}{\phi }\to \left(\forall {z}\in {S}\phantom{\rule{.4em}{0ex}}\left({z}\ne \varnothing \to {F}\left({z}\right)\in {z}\right)\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)\in \left[0,1\right]\right)$
26 4 25 mpd ${⊢}{\phi }\to \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)\in \left[0,1\right]$
27 ffnfv ${⊢}{F}:{S}⟶\left[0,1\right]↔\left({F}Fn{S}\wedge \forall {z}\in {S}\phantom{\rule{.4em}{0ex}}{F}\left({z}\right)\in \left[0,1\right]\right)$
28 3 26 27 sylanbrc ${⊢}{\phi }\to {F}:{S}⟶\left[0,1\right]$
29 28 frnd ${⊢}{\phi }\to \mathrm{ran}{F}\subseteq \left[0,1\right]$
30 5 adantr ${⊢}\left({\phi }\wedge {v}\in \left[0,1\right]\right)\to {G}:ℕ\underset{1-1 onto}{⟶}ℚ\cap \left[-1,1\right]$
31 f1ocnv ${⊢}{G}:ℕ\underset{1-1 onto}{⟶}ℚ\cap \left[-1,1\right]\to {{G}}^{-1}:ℚ\cap \left[-1,1\right]\underset{1-1 onto}{⟶}ℕ$
32 f1of ${⊢}{{G}}^{-1}:ℚ\cap \left[-1,1\right]\underset{1-1 onto}{⟶}ℕ\to {{G}}^{-1}:ℚ\cap \left[-1,1\right]⟶ℕ$
33 30 31 32 3syl ${⊢}\left({\phi }\wedge {v}\in \left[0,1\right]\right)\to {{G}}^{-1}:ℚ\cap \left[-1,1\right]⟶ℕ$
34 simpr ${⊢}\left({\phi }\wedge {v}\in \left[0,1\right]\right)\to {v}\in \left[0,1\right]$
35 34 14 sylib
36 neeq1
37 fveq2
38 id
39 37 38 eleq12d
40 36 39 imbi12d
41 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)$
42 ovex ${⊢}\left[0,1\right]\in \mathrm{V}$
43 erex
44 9 42 43 mp2
45 44 ecelqsi
47 46 2 eleqtrrdi
48 40 41 47 rspcdva
49 35 48 mpd
50 fvex
51 vex ${⊢}{v}\in \mathrm{V}$
52 50 51 elec
53 oveq12
54 53 eleq1d
55 54 1 brab2a
56 52 55 bitri
57 49 56 sylib
58 57 simprd
59 elicc01 ${⊢}{v}\in \left[0,1\right]↔\left({v}\in ℝ\wedge 0\le {v}\wedge {v}\le 1\right)$
60 34 59 sylib ${⊢}\left({\phi }\wedge {v}\in \left[0,1\right]\right)\to \left({v}\in ℝ\wedge 0\le {v}\wedge {v}\le 1\right)$
61 60 simp1d ${⊢}\left({\phi }\wedge {v}\in \left[0,1\right]\right)\to {v}\in ℝ$
62 57 simpld
63 62 simprd
64 elicc01
65 63 64 sylib
66 65 simp1d
67 61 66 resubcld
68 66 61 resubcld
69 1red ${⊢}\left({\phi }\wedge {v}\in \left[0,1\right]\right)\to 1\in ℝ$
70 60 simp2d ${⊢}\left({\phi }\wedge {v}\in \left[0,1\right]\right)\to 0\le {v}$
71 66 61 subge02d
72 70 71 mpbid
73 65 simp3d
74 68 66 69 72 73 letrd
75 68 69 lenegd
76 74 75 mpbid
77 66 recnd
78 61 recnd ${⊢}\left({\phi }\wedge {v}\in \left[0,1\right]\right)\to {v}\in ℂ$
79 77 78 negsubdi2d
80 76 79 breqtrd
81 65 simp2d
82 61 66 subge02d
83 81 82 mpbid
84 60 simp3d ${⊢}\left({\phi }\wedge {v}\in \left[0,1\right]\right)\to {v}\le 1$
85 67 61 69 83 84 letrd
86 neg1rr ${⊢}-1\in ℝ$
87 1re ${⊢}1\in ℝ$
88 86 87 elicc2i
89 67 80 85 88 syl3anbrc
90 58 89 elind
91 33 90 ffvelrnd
92 oveq1
93 92 eleq1d
94 f1ocnvfv2
95 5 90 94 syl2an2r
96 95 oveq2d
97 78 77 nncand
98 96 97 eqtrd
99 fnfvelrn
100 3 47 99 syl2an2r
101 98 100 eqeltrd
102 93 61 101 elrabd
103 fveq2
104 103 oveq2d
105 104 eleq1d
106 105 rabbidv
107 reex ${⊢}ℝ\in \mathrm{V}$
108 107 rabex
109 106 6 108 fvmpt
110 91 109 syl
111 102 110 eleqtrrd
112 fveq2
113 112 eliuni
114 91 111 113 syl2anc ${⊢}\left({\phi }\wedge {v}\in \left[0,1\right]\right)\to {v}\in \bigcup _{{m}\in ℕ}{T}\left({m}\right)$
115 114 ex ${⊢}{\phi }\to \left({v}\in \left[0,1\right]\to {v}\in \bigcup _{{m}\in ℕ}{T}\left({m}\right)\right)$
116 115 ssrdv ${⊢}{\phi }\to \left[0,1\right]\subseteq \bigcup _{{m}\in ℕ}{T}\left({m}\right)$
117 eliun ${⊢}{x}\in \bigcup _{{m}\in ℕ}{T}\left({m}\right)↔\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{x}\in {T}\left({m}\right)$
118 fveq2 ${⊢}{n}={m}\to {G}\left({n}\right)={G}\left({m}\right)$
119 118 oveq2d ${⊢}{n}={m}\to {s}-{G}\left({n}\right)={s}-{G}\left({m}\right)$
120 119 eleq1d ${⊢}{n}={m}\to \left({s}-{G}\left({n}\right)\in \mathrm{ran}{F}↔{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right)$
121 120 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\}$
122 107 rabex ${⊢}\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}\in \mathrm{V}$
123 121 6 122 fvmpt ${⊢}{m}\in ℕ\to {T}\left({m}\right)=\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}$
124 123 adantl ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {T}\left({m}\right)=\left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}$
125 124 eleq2d ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to \left({x}\in {T}\left({m}\right)↔{x}\in \left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}\right)$
126 125 biimpa ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {x}\in \left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}$
127 oveq1 ${⊢}{s}={x}\to {s}-{G}\left({m}\right)={x}-{G}\left({m}\right)$
128 127 eleq1d ${⊢}{s}={x}\to \left({s}-{G}\left({m}\right)\in \mathrm{ran}{F}↔{x}-{G}\left({m}\right)\in \mathrm{ran}{F}\right)$
129 128 elrab ${⊢}{x}\in \left\{{s}\in ℝ|{s}-{G}\left({m}\right)\in \mathrm{ran}{F}\right\}↔\left({x}\in ℝ\wedge {x}-{G}\left({m}\right)\in \mathrm{ran}{F}\right)$
130 126 129 sylib ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to \left({x}\in ℝ\wedge {x}-{G}\left({m}\right)\in \mathrm{ran}{F}\right)$
131 130 simpld ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {x}\in ℝ$
132 86 a1i ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to -1\in ℝ$
133 iccssre ${⊢}\left(-1\in ℝ\wedge 1\in ℝ\right)\to \left[-1,1\right]\subseteq ℝ$
134 86 87 133 mp2an ${⊢}\left[-1,1\right]\subseteq ℝ$
135 f1of ${⊢}{G}:ℕ\underset{1-1 onto}{⟶}ℚ\cap \left[-1,1\right]\to {G}:ℕ⟶ℚ\cap \left[-1,1\right]$
136 5 135 syl ${⊢}{\phi }\to {G}:ℕ⟶ℚ\cap \left[-1,1\right]$
137 136 ffvelrnda ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {G}\left({m}\right)\in \left(ℚ\cap \left[-1,1\right]\right)$
138 137 elin2d ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {G}\left({m}\right)\in \left[-1,1\right]$
139 134 138 sseldi ${⊢}\left({\phi }\wedge {m}\in ℕ\right)\to {G}\left({m}\right)\in ℝ$
140 139 adantr ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {G}\left({m}\right)\in ℝ$
141 138 adantr ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {G}\left({m}\right)\in \left[-1,1\right]$
142 86 87 elicc2i ${⊢}{G}\left({m}\right)\in \left[-1,1\right]↔\left({G}\left({m}\right)\in ℝ\wedge -1\le {G}\left({m}\right)\wedge {G}\left({m}\right)\le 1\right)$
143 141 142 sylib ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to \left({G}\left({m}\right)\in ℝ\wedge -1\le {G}\left({m}\right)\wedge {G}\left({m}\right)\le 1\right)$
144 143 simp2d ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to -1\le {G}\left({m}\right)$
145 29 ad2antrr ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to \mathrm{ran}{F}\subseteq \left[0,1\right]$
146 130 simprd ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {x}-{G}\left({m}\right)\in \mathrm{ran}{F}$
147 145 146 sseldd ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {x}-{G}\left({m}\right)\in \left[0,1\right]$
148 elicc01 ${⊢}{x}-{G}\left({m}\right)\in \left[0,1\right]↔\left({x}-{G}\left({m}\right)\in ℝ\wedge 0\le {x}-{G}\left({m}\right)\wedge {x}-{G}\left({m}\right)\le 1\right)$
149 147 148 sylib ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to \left({x}-{G}\left({m}\right)\in ℝ\wedge 0\le {x}-{G}\left({m}\right)\wedge {x}-{G}\left({m}\right)\le 1\right)$
150 149 simp2d ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to 0\le {x}-{G}\left({m}\right)$
151 131 140 subge0d ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to \left(0\le {x}-{G}\left({m}\right)↔{G}\left({m}\right)\le {x}\right)$
152 150 151 mpbid ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {G}\left({m}\right)\le {x}$
153 132 140 131 144 152 letrd ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to -1\le {x}$
154 peano2re ${⊢}{G}\left({m}\right)\in ℝ\to {G}\left({m}\right)+1\in ℝ$
155 140 154 syl ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {G}\left({m}\right)+1\in ℝ$
156 2re ${⊢}2\in ℝ$
157 156 a1i ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to 2\in ℝ$
158 149 simp3d ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {x}-{G}\left({m}\right)\le 1$
159 1red ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to 1\in ℝ$
160 131 140 159 lesubadd2d ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to \left({x}-{G}\left({m}\right)\le 1↔{x}\le {G}\left({m}\right)+1\right)$
161 158 160 mpbid ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {x}\le {G}\left({m}\right)+1$
162 143 simp3d ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {G}\left({m}\right)\le 1$
163 140 159 159 162 leadd1dd ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {G}\left({m}\right)+1\le 1+1$
164 df-2 ${⊢}2=1+1$
165 163 164 breqtrrdi ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {G}\left({m}\right)+1\le 2$
166 131 155 157 161 165 letrd ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {x}\le 2$
167 86 156 elicc2i ${⊢}{x}\in \left[-1,2\right]↔\left({x}\in ℝ\wedge -1\le {x}\wedge {x}\le 2\right)$
168 131 153 166 167 syl3anbrc ${⊢}\left(\left({\phi }\wedge {m}\in ℕ\right)\wedge {x}\in {T}\left({m}\right)\right)\to {x}\in \left[-1,2\right]$
169 168 rexlimdva2 ${⊢}{\phi }\to \left(\exists {m}\in ℕ\phantom{\rule{.4em}{0ex}}{x}\in {T}\left({m}\right)\to {x}\in \left[-1,2\right]\right)$
170 117 169 syl5bi ${⊢}{\phi }\to \left({x}\in \bigcup _{{m}\in ℕ}{T}\left({m}\right)\to {x}\in \left[-1,2\right]\right)$
171 170 ssrdv ${⊢}{\phi }\to \bigcup _{{m}\in ℕ}{T}\left({m}\right)\subseteq \left[-1,2\right]$
172 29 116 171 3jca ${⊢}{\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)$