Metamath Proof Explorer

Theorem vitalilem2

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

Ref Expression
Hypotheses vitali.1 ⊢∼˙=xy|x∈01∧y∈01∧x−y∈ℚ
vitali.2 ⊢S=01/∼˙
vitali.3 ⊢φ→FFnS
vitali.4 ⊢φ→∀z∈Sz≠∅→F⁡z∈z
vitali.5 ⊢φ→G:ℕ⟶1-1 ontoℚ∩−11
vitali.6 ⊢T=n∈ℕ⟼s∈ℝ|s−G⁡n∈ran⁡F
vitali.7 ⊢φ→¬ran⁡F∈𝒫ℝ∖dom⁡vol
Assertion vitalilem2 ⊢φ→ran⁡F⊆01∧01⊆⋃m∈ℕT⁡m∧⋃m∈ℕT⁡m⊆−12

Proof

Step Hyp Ref Expression
1 vitali.1 ⊢∼˙=xy|x∈01∧y∈01∧x−y∈ℚ
2 vitali.2 ⊢S=01/∼˙
3 vitali.3 ⊢φ→FFnS
4 vitali.4 ⊢φ→∀z∈Sz≠∅→F⁡z∈z
5 vitali.5 ⊢φ→G:ℕ⟶1-1 ontoℚ∩−11
6 vitali.6 ⊢T=n∈ℕ⟼s∈ℝ|s−G⁡n∈ran⁡F
7 vitali.7 ⊢φ→¬ran⁡F∈𝒫ℝ∖dom⁡vol
8 neeq1 ⊢v∼˙=z→v∼˙≠∅↔z≠∅
9 1 vitalilem1 ⊢∼˙Er01
10 erdm ⊢∼˙Er01→dom⁡∼˙=01
11 9 10 ax-mp ⊢dom⁡∼˙=01
12 11 eleq2i ⊢v∈dom⁡∼˙↔v∈01
13 ecdmn0 ⊢v∈dom⁡∼˙↔v∼˙≠∅
14 12 13 bitr3i ⊢v∈01↔v∼˙≠∅
15 14 biimpi ⊢v∈01→v∼˙≠∅
16 2 8 15 ectocl ⊢z∈S→z≠∅
17 16 adantl ⊢φ∧z∈S→z≠∅
18 sseq1 ⊢w∼˙=z→w∼˙⊆01↔z⊆01
19 9 a1i ⊢w∈01→∼˙Er01
20 19 ecss ⊢w∈01→w∼˙⊆01
21 2 18 20 ectocl ⊢z∈S→z⊆01
22 21 adantl ⊢φ∧z∈S→z⊆01
23 22 sseld ⊢φ∧z∈S→F⁡z∈z→F⁡z∈01
24 17 23 embantd ⊢φ∧z∈S→z≠∅→F⁡z∈z→F⁡z∈01
25 24 ralimdva ⊢φ→∀z∈Sz≠∅→F⁡z∈z→∀z∈SF⁡z∈01
26 4 25 mpd ⊢φ→∀z∈SF⁡z∈01
27 ffnfv ⊢F:S⟶01↔FFnS∧∀z∈SF⁡z∈01
28 3 26 27 sylanbrc ⊢φ→F:S⟶01
29 28 frnd ⊢φ→ran⁡F⊆01
30 5 adantr ⊢φ∧v∈01→G:ℕ⟶1-1 ontoℚ∩−11
31 f1ocnv ⊢G:ℕ⟶1-1 ontoℚ∩−11→G-1:ℚ∩−11⟶1-1 ontoℕ
32 f1of ⊢G-1:ℚ∩−11⟶1-1 ontoℕ→G-1:ℚ∩−11⟶ℕ
33 30 31 32 3syl ⊢φ∧v∈01→G-1:ℚ∩−11⟶ℕ
34 simpr ⊢φ∧v∈01→v∈01
35 34 14 sylib ⊢φ∧v∈01→v∼˙≠∅
36 neeq1 ⊢z=v∼˙→z≠∅↔v∼˙≠∅
37 fveq2 ⊢z=v∼˙→F⁡z=F⁡v∼˙
38 id ⊢z=v∼˙→z=v∼˙
39 37 38 eleq12d ⊢z=v∼˙→F⁡z∈z↔F⁡v∼˙∈v∼˙
40 36 39 imbi12d ⊢z=v∼˙→z≠∅→F⁡z∈z↔v∼˙≠∅→F⁡v∼˙∈v∼˙
41 4 adantr ⊢φ∧v∈01→∀z∈Sz≠∅→F⁡z∈z
42 ovex ⊢01∈V
43 erex ⊢∼˙Er01→01∈V→∼˙∈V
44 9 42 43 mp2 ⊢∼˙∈V
45 44 ecelqsi ⊢v∈01→v∼˙∈01/∼˙
46 45 adantl ⊢φ∧v∈01→v∼˙∈01/∼˙
47 46 2 eleqtrrdi ⊢φ∧v∈01→v∼˙∈S
48 40 41 47 rspcdva ⊢φ∧v∈01→v∼˙≠∅→F⁡v∼˙∈v∼˙
49 35 48 mpd ⊢φ∧v∈01→F⁡v∼˙∈v∼˙
50 fvex ⊢F⁡v∼˙∈V
51 vex ⊢v∈V
52 50 51 elec ⊢F⁡v∼˙∈v∼˙↔v∼˙F⁡v∼˙
53 oveq12 ⊢x=v∧y=F⁡v∼˙→x−y=v−F⁡v∼˙
54 53 eleq1d ⊢x=v∧y=F⁡v∼˙→x−y∈ℚ↔v−F⁡v∼˙∈ℚ
55 54 1 brab2a ⊢v∼˙F⁡v∼˙↔v∈01∧F⁡v∼˙∈01∧v−F⁡v∼˙∈ℚ
56 52 55 bitri ⊢F⁡v∼˙∈v∼˙↔v∈01∧F⁡v∼˙∈01∧v−F⁡v∼˙∈ℚ
57 49 56 sylib ⊢φ∧v∈01→v∈01∧F⁡v∼˙∈01∧v−F⁡v∼˙∈ℚ
58 57 simprd ⊢φ∧v∈01→v−F⁡v∼˙∈ℚ
59 elicc01 ⊢v∈01↔v∈ℝ∧0≤v∧v≤1
60 34 59 sylib ⊢φ∧v∈01→v∈ℝ∧0≤v∧v≤1
61 60 simp1d ⊢φ∧v∈01→v∈ℝ
62 57 simpld ⊢φ∧v∈01→v∈01∧F⁡v∼˙∈01
63 62 simprd ⊢φ∧v∈01→F⁡v∼˙∈01
64 elicc01 ⊢F⁡v∼˙∈01↔F⁡v∼˙∈ℝ∧0≤F⁡v∼˙∧F⁡v∼˙≤1
65 63 64 sylib ⊢φ∧v∈01→F⁡v∼˙∈ℝ∧0≤F⁡v∼˙∧F⁡v∼˙≤1
66 65 simp1d ⊢φ∧v∈01→F⁡v∼˙∈ℝ
67 61 66 resubcld ⊢φ∧v∈01→v−F⁡v∼˙∈ℝ
68 66 61 resubcld ⊢φ∧v∈01→F⁡v∼˙−v∈ℝ
69 1red ⊢φ∧v∈01→1∈ℝ
70 60 simp2d ⊢φ∧v∈01→0≤v
71 66 61 subge02d ⊢φ∧v∈01→0≤v↔F⁡v∼˙−v≤F⁡v∼˙
72 70 71 mpbid ⊢φ∧v∈01→F⁡v∼˙−v≤F⁡v∼˙
73 65 simp3d ⊢φ∧v∈01→F⁡v∼˙≤1
74 68 66 69 72 73 letrd ⊢φ∧v∈01→F⁡v∼˙−v≤1
75 68 69 lenegd ⊢φ∧v∈01→F⁡v∼˙−v≤1↔−1≤−F⁡v∼˙−v
76 74 75 mpbid ⊢φ∧v∈01→−1≤−F⁡v∼˙−v
77 66 recnd ⊢φ∧v∈01→F⁡v∼˙∈ℂ
78 61 recnd ⊢φ∧v∈01→v∈ℂ
79 77 78 negsubdi2d ⊢φ∧v∈01→−F⁡v∼˙−v=v−F⁡v∼˙
80 76 79 breqtrd ⊢φ∧v∈01→−1≤v−F⁡v∼˙
81 65 simp2d ⊢φ∧v∈01→0≤F⁡v∼˙
82 61 66 subge02d ⊢φ∧v∈01→0≤F⁡v∼˙↔v−F⁡v∼˙≤v
83 81 82 mpbid ⊢φ∧v∈01→v−F⁡v∼˙≤v
84 60 simp3d ⊢φ∧v∈01→v≤1
85 67 61 69 83 84 letrd ⊢φ∧v∈01→v−F⁡v∼˙≤1
86 neg1rr ⊢−1∈ℝ
87 1re ⊢1∈ℝ
88 86 87 elicc2i ⊢v−F⁡v∼˙∈−11↔v−F⁡v∼˙∈ℝ∧−1≤v−F⁡v∼˙∧v−F⁡v∼˙≤1
89 67 80 85 88 syl3anbrc ⊢φ∧v∈01→v−F⁡v∼˙∈−11
90 58 89 elind ⊢φ∧v∈01→v−F⁡v∼˙∈ℚ∩−11
91 33 90 ffvelcdmd ⊢φ∧v∈01→G-1⁡v−F⁡v∼˙∈ℕ
92 oveq1 ⊢s=v→s−G⁡G-1⁡v−F⁡v∼˙=v−G⁡G-1⁡v−F⁡v∼˙
93 92 eleq1d ⊢s=v→s−G⁡G-1⁡v−F⁡v∼˙∈ran⁡F↔v−G⁡G-1⁡v−F⁡v∼˙∈ran⁡F
94 f1ocnvfv2 ⊢G:ℕ⟶1-1 ontoℚ∩−11∧v−F⁡v∼˙∈ℚ∩−11→G⁡G-1⁡v−F⁡v∼˙=v−F⁡v∼˙
95 5 90 94 syl2an2r ⊢φ∧v∈01→G⁡G-1⁡v−F⁡v∼˙=v−F⁡v∼˙
96 95 oveq2d ⊢φ∧v∈01→v−G⁡G-1⁡v−F⁡v∼˙=v−v−F⁡v∼˙
97 78 77 nncand ⊢φ∧v∈01→v−v−F⁡v∼˙=F⁡v∼˙
98 96 97 eqtrd ⊢φ∧v∈01→v−G⁡G-1⁡v−F⁡v∼˙=F⁡v∼˙
99 fnfvelrn ⊢FFnS∧v∼˙∈S→F⁡v∼˙∈ran⁡F
100 3 47 99 syl2an2r ⊢φ∧v∈01→F⁡v∼˙∈ran⁡F
101 98 100 eqeltrd ⊢φ∧v∈01→v−G⁡G-1⁡v−F⁡v∼˙∈ran⁡F
102 93 61 101 elrabd ⊢φ∧v∈01→v∈s∈ℝ|s−G⁡G-1⁡v−F⁡v∼˙∈ran⁡F
103 fveq2 ⊢n=G-1⁡v−F⁡v∼˙→G⁡n=G⁡G-1⁡v−F⁡v∼˙
104 103 oveq2d ⊢n=G-1⁡v−F⁡v∼˙→s−G⁡n=s−G⁡G-1⁡v−F⁡v∼˙
105 104 eleq1d ⊢n=G-1⁡v−F⁡v∼˙→s−G⁡n∈ran⁡F↔s−G⁡G-1⁡v−F⁡v∼˙∈ran⁡F
106 105 rabbidv ⊢n=G-1⁡v−F⁡v∼˙→s∈ℝ|s−G⁡n∈ran⁡F=s∈ℝ|s−G⁡G-1⁡v−F⁡v∼˙∈ran⁡F
107 reex ⊢ℝ∈V
108 107 rabex ⊢s∈ℝ|s−G⁡G-1⁡v−F⁡v∼˙∈ran⁡F∈V
109 106 6 108 fvmpt ⊢G-1⁡v−F⁡v∼˙∈ℕ→T⁡G-1⁡v−F⁡v∼˙=s∈ℝ|s−G⁡G-1⁡v−F⁡v∼˙∈ran⁡F
110 91 109 syl ⊢φ∧v∈01→T⁡G-1⁡v−F⁡v∼˙=s∈ℝ|s−G⁡G-1⁡v−F⁡v∼˙∈ran⁡F
111 102 110 eleqtrrd ⊢φ∧v∈01→v∈T⁡G-1⁡v−F⁡v∼˙
112 fveq2 ⊢m=G-1⁡v−F⁡v∼˙→T⁡m=T⁡G-1⁡v−F⁡v∼˙
113 112 eliuni ⊢G-1⁡v−F⁡v∼˙∈ℕ∧v∈T⁡G-1⁡v−F⁡v∼˙→v∈⋃m∈ℕT⁡m
114 91 111 113 syl2anc ⊢φ∧v∈01→v∈⋃m∈ℕT⁡m
115 114 ex ⊢φ→v∈01→v∈⋃m∈ℕT⁡m
116 115 ssrdv ⊢φ→01⊆⋃m∈ℕT⁡m
117 eliun ⊢x∈⋃m∈ℕT⁡m↔∃m∈ℕx∈T⁡m
118 fveq2 ⊢n=m→G⁡n=G⁡m
119 118 oveq2d ⊢n=m→s−G⁡n=s−G⁡m
120 119 eleq1d ⊢n=m→s−G⁡n∈ran⁡F↔s−G⁡m∈ran⁡F
121 120 rabbidv ⊢n=m→s∈ℝ|s−G⁡n∈ran⁡F=s∈ℝ|s−G⁡m∈ran⁡F
122 107 rabex ⊢s∈ℝ|s−G⁡m∈ran⁡F∈V
123 121 6 122 fvmpt ⊢m∈ℕ→T⁡m=s∈ℝ|s−G⁡m∈ran⁡F
124 123 adantl ⊢φ∧m∈ℕ→T⁡m=s∈ℝ|s−G⁡m∈ran⁡F
125 124 eleq2d ⊢φ∧m∈ℕ→x∈T⁡m↔x∈s∈ℝ|s−G⁡m∈ran⁡F
126 125 biimpa ⊢φ∧m∈ℕ∧x∈T⁡m→x∈s∈ℝ|s−G⁡m∈ran⁡F
127 oveq1 ⊢s=x→s−G⁡m=x−G⁡m
128 127 eleq1d ⊢s=x→s−G⁡m∈ran⁡F↔x−G⁡m∈ran⁡F
129 128 elrab ⊢x∈s∈ℝ|s−G⁡m∈ran⁡F↔x∈ℝ∧x−G⁡m∈ran⁡F
130 126 129 sylib ⊢φ∧m∈ℕ∧x∈T⁡m→x∈ℝ∧x−G⁡m∈ran⁡F
131 130 simpld ⊢φ∧m∈ℕ∧x∈T⁡m→x∈ℝ
132 86 a1i ⊢φ∧m∈ℕ∧x∈T⁡m→−1∈ℝ
133 iccssre ⊢−1∈ℝ∧1∈ℝ→−11⊆ℝ
134 86 87 133 mp2an ⊢−11⊆ℝ
135 f1of ⊢G:ℕ⟶1-1 ontoℚ∩−11→G:ℕ⟶ℚ∩−11
136 5 135 syl ⊢φ→G:ℕ⟶ℚ∩−11
137 136 ffvelcdmda ⊢φ∧m∈ℕ→G⁡m∈ℚ∩−11
138 137 elin2d ⊢φ∧m∈ℕ→G⁡m∈−11
139 134 138 sselid ⊢φ∧m∈ℕ→G⁡m∈ℝ
140 139 adantr ⊢φ∧m∈ℕ∧x∈T⁡m→G⁡m∈ℝ
141 138 adantr ⊢φ∧m∈ℕ∧x∈T⁡m→G⁡m∈−11
142 86 87 elicc2i ⊢G⁡m∈−11↔G⁡m∈ℝ∧−1≤G⁡m∧G⁡m≤1
143 141 142 sylib ⊢φ∧m∈ℕ∧x∈T⁡m→G⁡m∈ℝ∧−1≤G⁡m∧G⁡m≤1
144 143 simp2d ⊢φ∧m∈ℕ∧x∈T⁡m→−1≤G⁡m
145 29 ad2antrr ⊢φ∧m∈ℕ∧x∈T⁡m→ran⁡F⊆01
146 130 simprd ⊢φ∧m∈ℕ∧x∈T⁡m→x−G⁡m∈ran⁡F
147 145 146 sseldd ⊢φ∧m∈ℕ∧x∈T⁡m→x−G⁡m∈01
148 elicc01 ⊢x−G⁡m∈01↔x−G⁡m∈ℝ∧0≤x−G⁡m∧x−G⁡m≤1
149 147 148 sylib ⊢φ∧m∈ℕ∧x∈T⁡m→x−G⁡m∈ℝ∧0≤x−G⁡m∧x−G⁡m≤1
150 149 simp2d ⊢φ∧m∈ℕ∧x∈T⁡m→0≤x−G⁡m
151 131 140 subge0d ⊢φ∧m∈ℕ∧x∈T⁡m→0≤x−G⁡m↔G⁡m≤x
152 150 151 mpbid ⊢φ∧m∈ℕ∧x∈T⁡m→G⁡m≤x
153 132 140 131 144 152 letrd ⊢φ∧m∈ℕ∧x∈T⁡m→−1≤x
154 peano2re ⊢G⁡m∈ℝ→G⁡m+1∈ℝ
155 140 154 syl ⊢φ∧m∈ℕ∧x∈T⁡m→G⁡m+1∈ℝ
156 2re ⊢2∈ℝ
157 156 a1i ⊢φ∧m∈ℕ∧x∈T⁡m→2∈ℝ
158 149 simp3d ⊢φ∧m∈ℕ∧x∈T⁡m→x−G⁡m≤1
159 1red ⊢φ∧m∈ℕ∧x∈T⁡m→1∈ℝ
160 131 140 159 lesubadd2d ⊢φ∧m∈ℕ∧x∈T⁡m→x−G⁡m≤1↔x≤G⁡m+1
161 158 160 mpbid ⊢φ∧m∈ℕ∧x∈T⁡m→x≤G⁡m+1
162 143 simp3d ⊢φ∧m∈ℕ∧x∈T⁡m→G⁡m≤1
163 140 159 159 162 leadd1dd ⊢φ∧m∈ℕ∧x∈T⁡m→G⁡m+1≤1+1
164 df-2 ⊢2=1+1
165 163 164 breqtrrdi ⊢φ∧m∈ℕ∧x∈T⁡m→G⁡m+1≤2
166 131 155 157 161 165 letrd ⊢φ∧m∈ℕ∧x∈T⁡m→x≤2
167 86 156 elicc2i ⊢x∈−12↔x∈ℝ∧−1≤x∧x≤2
168 131 153 166 167 syl3anbrc ⊢φ∧m∈ℕ∧x∈T⁡m→x∈−12
169 168 rexlimdva2 ⊢φ→∃m∈ℕx∈T⁡m→x∈−12
170 117 169 biimtrid ⊢φ→x∈⋃m∈ℕT⁡m→x∈−12
171 170 ssrdv ⊢φ→⋃m∈ℕT⁡m⊆−12
172 29 116 171 3jca ⊢φ→ran⁡F⊆01∧01⊆⋃m∈ℕT⁡m∧⋃m∈ℕT⁡m⊆−12