Metamath Proof Explorer


Theorem vitalilem2

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

Ref Expression
Hypotheses vitali.1 ˙ = x y | x 0 1 y 0 1 x y
vitali.2 S = 0 1 / ˙
vitali.3 φ F Fn S
vitali.4 φ z S z F z z
vitali.5 φ G : 1-1 onto 1 1
vitali.6 T = n s | s G n ran F
vitali.7 φ ¬ ran F 𝒫 dom vol
Assertion vitalilem2 φ ran F 0 1 0 1 m T m m T m 1 2

Proof

Step Hyp Ref Expression
1 vitali.1 ˙ = x y | x 0 1 y 0 1 x y
2 vitali.2 S = 0 1 / ˙
3 vitali.3 φ F Fn S
4 vitali.4 φ z S z F z z
5 vitali.5 φ G : 1-1 onto 1 1
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 ˙ Er 0 1
10 erdm ˙ Er 0 1 dom ˙ = 0 1
11 9 10 ax-mp dom ˙ = 0 1
12 11 eleq2i v dom ˙ v 0 1
13 ecdmn0 v dom ˙ v ˙
14 12 13 bitr3i v 0 1 v ˙
15 14 biimpi v 0 1 v ˙
16 2 8 15 ectocl z S z
17 16 adantl φ z S z
18 sseq1 w ˙ = z w ˙ 0 1 z 0 1
19 9 a1i w 0 1 ˙ Er 0 1
20 19 ecss w 0 1 w ˙ 0 1
21 2 18 20 ectocl z S z 0 1
22 21 adantl φ z S z 0 1
23 22 sseld φ z S F z z F z 0 1
24 17 23 embantd φ z S z F z z F z 0 1
25 24 ralimdva φ z S z F z z z S F z 0 1
26 4 25 mpd φ z S F z 0 1
27 ffnfv F : S 0 1 F Fn S z S F z 0 1
28 3 26 27 sylanbrc φ F : S 0 1
29 28 frnd φ ran F 0 1
30 5 adantr φ v 0 1 G : 1-1 onto 1 1
31 f1ocnv G : 1-1 onto 1 1 G -1 : 1 1 1-1 onto
32 f1of G -1 : 1 1 1-1 onto G -1 : 1 1
33 30 31 32 3syl φ v 0 1 G -1 : 1 1
34 simpr φ v 0 1 v 0 1
35 34 14 sylib φ v 0 1 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 0 1 z S z F z z
42 ovex 0 1 V
43 erex ˙ Er 0 1 0 1 V ˙ V
44 9 42 43 mp2 ˙ V
45 44 ecelqsi v 0 1 v ˙ 0 1 / ˙
46 45 adantl φ v 0 1 v ˙ 0 1 / ˙
47 46 2 eleqtrrdi φ v 0 1 v ˙ S
48 40 41 47 rspcdva φ v 0 1 v ˙ F v ˙ v ˙
49 35 48 mpd φ v 0 1 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 0 1 F v ˙ 0 1 v F v ˙
56 52 55 bitri F v ˙ v ˙ v 0 1 F v ˙ 0 1 v F v ˙
57 49 56 sylib φ v 0 1 v 0 1 F v ˙ 0 1 v F v ˙
58 57 simprd φ v 0 1 v F v ˙
59 elicc01 v 0 1 v 0 v v 1
60 34 59 sylib φ v 0 1 v 0 v v 1
61 60 simp1d φ v 0 1 v
62 57 simpld φ v 0 1 v 0 1 F v ˙ 0 1
63 62 simprd φ v 0 1 F v ˙ 0 1
64 elicc01 F v ˙ 0 1 F v ˙ 0 F v ˙ F v ˙ 1
65 63 64 sylib φ v 0 1 F v ˙ 0 F v ˙ F v ˙ 1
66 65 simp1d φ v 0 1 F v ˙
67 61 66 resubcld φ v 0 1 v F v ˙
68 66 61 resubcld φ v 0 1 F v ˙ v
69 1red φ v 0 1 1
70 60 simp2d φ v 0 1 0 v
71 66 61 subge02d φ v 0 1 0 v F v ˙ v F v ˙
72 70 71 mpbid φ v 0 1 F v ˙ v F v ˙
73 65 simp3d φ v 0 1 F v ˙ 1
74 68 66 69 72 73 letrd φ v 0 1 F v ˙ v 1
75 68 69 lenegd φ v 0 1 F v ˙ v 1 1 F v ˙ v
76 74 75 mpbid φ v 0 1 1 F v ˙ v
77 66 recnd φ v 0 1 F v ˙
78 61 recnd φ v 0 1 v
79 77 78 negsubdi2d φ v 0 1 F v ˙ v = v F v ˙
80 76 79 breqtrd φ v 0 1 1 v F v ˙
81 65 simp2d φ v 0 1 0 F v ˙
82 61 66 subge02d φ v 0 1 0 F v ˙ v F v ˙ v
83 81 82 mpbid φ v 0 1 v F v ˙ v
84 60 simp3d φ v 0 1 v 1
85 67 61 69 83 84 letrd φ v 0 1 v F v ˙ 1
86 neg1rr 1
87 1re 1
88 86 87 elicc2i v F v ˙ 1 1 v F v ˙ 1 v F v ˙ v F v ˙ 1
89 67 80 85 88 syl3anbrc φ v 0 1 v F v ˙ 1 1
90 58 89 elind φ v 0 1 v F v ˙ 1 1
91 33 90 ffvelrnd φ v 0 1 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 1 1 v F v ˙ 1 1 G G -1 v F v ˙ = v F v ˙
95 5 90 94 syl2an2r φ v 0 1 G G -1 v F v ˙ = v F v ˙
96 95 oveq2d φ v 0 1 v G G -1 v F v ˙ = v v F v ˙
97 78 77 nncand φ v 0 1 v v F v ˙ = F v ˙
98 96 97 eqtrd φ v 0 1 v G G -1 v F v ˙ = F v ˙
99 fnfvelrn F Fn S v ˙ S F v ˙ ran F
100 3 47 99 syl2an2r φ v 0 1 F v ˙ ran F
101 98 100 eqeltrd φ v 0 1 v G G -1 v F v ˙ ran F
102 93 61 101 elrabd φ v 0 1 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 0 1 T G -1 v F v ˙ = s | s G G -1 v F v ˙ ran F
111 102 110 eleqtrrd φ v 0 1 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 0 1 v m T m
115 114 ex φ v 0 1 v m T m
116 115 ssrdv φ 0 1 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 1 1
134 86 87 133 mp2an 1 1
135 f1of G : 1-1 onto 1 1 G : 1 1
136 5 135 syl φ G : 1 1
137 136 ffvelrnda φ m G m 1 1
138 137 elin2d φ m G m 1 1
139 134 138 sseldi φ m G m
140 139 adantr φ m x T m G m
141 138 adantr φ m x T m G m 1 1
142 86 87 elicc2i G m 1 1 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 0 1
146 130 simprd φ m x T m x G m ran F
147 145 146 sseldd φ m x T m x G m 0 1
148 elicc01 x G m 0 1 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 1 2 x 1 x x 2
168 131 153 166 167 syl3anbrc φ m x T m x 1 2
169 168 rexlimdva2 φ m x T m x 1 2
170 117 169 syl5bi φ x m T m x 1 2
171 170 ssrdv φ m T m 1 2
172 29 116 171 3jca φ ran F 0 1 0 1 m T m m T m 1 2