Metamath Proof Explorer


Theorem volsup

Description: The volume of the limit of an increasing sequence of measurable sets is the limit of the volumes. (Contributed by Mario Carneiro, 14-Aug-2014) (Revised by Mario Carneiro, 11-Dec-2016)

Ref Expression
Assertion volsup F : dom vol n F n F n + 1 vol ran F = sup vol ran F * <

Proof

Step Hyp Ref Expression
1 ffvelrn F : dom vol k F k dom vol
2 1 ad2ant2r F : dom vol n F n F n + 1 k vol F k F k dom vol
3 fzofi 1 ..^ k Fin
4 simpll F : dom vol n F n F n + 1 k vol F k F : dom vol
5 elfzouz m 1 ..^ k m 1
6 nnuz = 1
7 5 6 eleqtrrdi m 1 ..^ k m
8 ffvelrn F : dom vol m F m dom vol
9 4 7 8 syl2an F : dom vol n F n F n + 1 k vol F k m 1 ..^ k F m dom vol
10 9 ralrimiva F : dom vol n F n F n + 1 k vol F k m 1 ..^ k F m dom vol
11 finiunmbl 1 ..^ k Fin m 1 ..^ k F m dom vol m 1 ..^ k F m dom vol
12 3 10 11 sylancr F : dom vol n F n F n + 1 k vol F k m 1 ..^ k F m dom vol
13 difmbl F k dom vol m 1 ..^ k F m dom vol F k m 1 ..^ k F m dom vol
14 2 12 13 syl2anc F : dom vol n F n F n + 1 k vol F k F k m 1 ..^ k F m dom vol
15 mblvol F k m 1 ..^ k F m dom vol vol F k m 1 ..^ k F m = vol * F k m 1 ..^ k F m
16 14 15 syl F : dom vol n F n F n + 1 k vol F k vol F k m 1 ..^ k F m = vol * F k m 1 ..^ k F m
17 difssd F : dom vol n F n F n + 1 k vol F k F k m 1 ..^ k F m F k
18 mblss F k dom vol F k
19 2 18 syl F : dom vol n F n F n + 1 k vol F k F k
20 mblvol F k dom vol vol F k = vol * F k
21 2 20 syl F : dom vol n F n F n + 1 k vol F k vol F k = vol * F k
22 simprr F : dom vol n F n F n + 1 k vol F k vol F k
23 21 22 eqeltrrd F : dom vol n F n F n + 1 k vol F k vol * F k
24 ovolsscl F k m 1 ..^ k F m F k F k vol * F k vol * F k m 1 ..^ k F m
25 17 19 23 24 syl3anc F : dom vol n F n F n + 1 k vol F k vol * F k m 1 ..^ k F m
26 16 25 eqeltrd F : dom vol n F n F n + 1 k vol F k vol F k m 1 ..^ k F m
27 14 26 jca F : dom vol n F n F n + 1 k vol F k F k m 1 ..^ k F m dom vol vol F k m 1 ..^ k F m
28 27 expr F : dom vol n F n F n + 1 k vol F k F k m 1 ..^ k F m dom vol vol F k m 1 ..^ k F m
29 28 ralimdva F : dom vol n F n F n + 1 k vol F k k F k m 1 ..^ k F m dom vol vol F k m 1 ..^ k F m
30 29 imp F : dom vol n F n F n + 1 k vol F k k F k m 1 ..^ k F m dom vol vol F k m 1 ..^ k F m
31 fveq2 k = m F k = F m
32 31 iundisj2 Disj k F k m 1 ..^ k F m
33 eqid seq 1 + k vol F k m 1 ..^ k F m = seq 1 + k vol F k m 1 ..^ k F m
34 eqid k vol F k m 1 ..^ k F m = k vol F k m 1 ..^ k F m
35 33 34 voliun k F k m 1 ..^ k F m dom vol vol F k m 1 ..^ k F m Disj k F k m 1 ..^ k F m vol k F k m 1 ..^ k F m = sup ran seq 1 + k vol F k m 1 ..^ k F m * <
36 30 32 35 sylancl F : dom vol n F n F n + 1 k vol F k vol k F k m 1 ..^ k F m = sup ran seq 1 + k vol F k m 1 ..^ k F m * <
37 31 iundisj k F k = k F k m 1 ..^ k F m
38 ffn F : dom vol F Fn
39 38 ad2antrr F : dom vol n F n F n + 1 k vol F k F Fn
40 fniunfv F Fn k F k = ran F
41 39 40 syl F : dom vol n F n F n + 1 k vol F k k F k = ran F
42 37 41 eqtr3id F : dom vol n F n F n + 1 k vol F k k F k m 1 ..^ k F m = ran F
43 42 fveq2d F : dom vol n F n F n + 1 k vol F k vol k F k m 1 ..^ k F m = vol ran F
44 1z 1
45 seqfn 1 seq 1 + k vol F k m 1 ..^ k F m Fn 1
46 44 45 ax-mp seq 1 + k vol F k m 1 ..^ k F m Fn 1
47 6 fneq2i seq 1 + k vol F k m 1 ..^ k F m Fn seq 1 + k vol F k m 1 ..^ k F m Fn 1
48 46 47 mpbir seq 1 + k vol F k m 1 ..^ k F m Fn
49 48 a1i F : dom vol n F n F n + 1 k vol F k seq 1 + k vol F k m 1 ..^ k F m Fn
50 volf vol : dom vol 0 +∞
51 simpll F : dom vol n F n F n + 1 k vol F k F : dom vol
52 fco vol : dom vol 0 +∞ F : dom vol vol F : 0 +∞
53 50 51 52 sylancr F : dom vol n F n F n + 1 k vol F k vol F : 0 +∞
54 53 ffnd F : dom vol n F n F n + 1 k vol F k vol F Fn
55 fveq2 x = 1 seq 1 + k vol F k m 1 ..^ k F m x = seq 1 + k vol F k m 1 ..^ k F m 1
56 2fveq3 x = 1 vol F x = vol F 1
57 55 56 eqeq12d x = 1 seq 1 + k vol F k m 1 ..^ k F m x = vol F x seq 1 + k vol F k m 1 ..^ k F m 1 = vol F 1
58 57 imbi2d x = 1 F : dom vol n F n F n + 1 k vol F k seq 1 + k vol F k m 1 ..^ k F m x = vol F x F : dom vol n F n F n + 1 k vol F k seq 1 + k vol F k m 1 ..^ k F m 1 = vol F 1
59 fveq2 x = j seq 1 + k vol F k m 1 ..^ k F m x = seq 1 + k vol F k m 1 ..^ k F m j
60 2fveq3 x = j vol F x = vol F j
61 59 60 eqeq12d x = j seq 1 + k vol F k m 1 ..^ k F m x = vol F x seq 1 + k vol F k m 1 ..^ k F m j = vol F j
62 61 imbi2d x = j F : dom vol n F n F n + 1 k vol F k seq 1 + k vol F k m 1 ..^ k F m x = vol F x F : dom vol n F n F n + 1 k vol F k seq 1 + k vol F k m 1 ..^ k F m j = vol F j
63 fveq2 x = j + 1 seq 1 + k vol F k m 1 ..^ k F m x = seq 1 + k vol F k m 1 ..^ k F m j + 1
64 2fveq3 x = j + 1 vol F x = vol F j + 1
65 63 64 eqeq12d x = j + 1 seq 1 + k vol F k m 1 ..^ k F m x = vol F x seq 1 + k vol F k m 1 ..^ k F m j + 1 = vol F j + 1
66 65 imbi2d x = j + 1 F : dom vol n F n F n + 1 k vol F k seq 1 + k vol F k m 1 ..^ k F m x = vol F x F : dom vol n F n F n + 1 k vol F k seq 1 + k vol F k m 1 ..^ k F m j + 1 = vol F j + 1
67 seq1 1 seq 1 + k vol F k m 1 ..^ k F m 1 = k vol F k m 1 ..^ k F m 1
68 44 67 ax-mp seq 1 + k vol F k m 1 ..^ k F m 1 = k vol F k m 1 ..^ k F m 1
69 1nn 1
70 oveq2 k = 1 1 ..^ k = 1 ..^ 1
71 fzo0 1 ..^ 1 =
72 70 71 eqtrdi k = 1 1 ..^ k =
73 72 iuneq1d k = 1 m 1 ..^ k F m = m F m
74 0iun m F m =
75 73 74 eqtrdi k = 1 m 1 ..^ k F m =
76 75 difeq2d k = 1 F k m 1 ..^ k F m = F k
77 dif0 F k = F k
78 76 77 eqtrdi k = 1 F k m 1 ..^ k F m = F k
79 fveq2 k = 1 F k = F 1
80 78 79 eqtrd k = 1 F k m 1 ..^ k F m = F 1
81 80 fveq2d k = 1 vol F k m 1 ..^ k F m = vol F 1
82 fvex vol F 1 V
83 81 34 82 fvmpt 1 k vol F k m 1 ..^ k F m 1 = vol F 1
84 69 83 ax-mp k vol F k m 1 ..^ k F m 1 = vol F 1
85 68 84 eqtri seq 1 + k vol F k m 1 ..^ k F m 1 = vol F 1
86 85 a1i F : dom vol n F n F n + 1 k vol F k seq 1 + k vol F k m 1 ..^ k F m 1 = vol F 1
87 oveq1 seq 1 + k vol F k m 1 ..^ k F m j = vol F j seq 1 + k vol F k m 1 ..^ k F m j + k vol F k m 1 ..^ k F m j + 1 = vol F j + k vol F k m 1 ..^ k F m j + 1
88 seqp1 j 1 seq 1 + k vol F k m 1 ..^ k F m j + 1 = seq 1 + k vol F k m 1 ..^ k F m j + k vol F k m 1 ..^ k F m j + 1
89 88 6 eleq2s j seq 1 + k vol F k m 1 ..^ k F m j + 1 = seq 1 + k vol F k m 1 ..^ k F m j + k vol F k m 1 ..^ k F m j + 1
90 89 adantl F : dom vol n F n F n + 1 k vol F k j seq 1 + k vol F k m 1 ..^ k F m j + 1 = seq 1 + k vol F k m 1 ..^ k F m j + k vol F k m 1 ..^ k F m j + 1
91 undif2 F j F j + 1 F j = F j F j + 1
92 fveq2 n = j F n = F j
93 fvoveq1 n = j F n + 1 = F j + 1
94 92 93 sseq12d n = j F n F n + 1 F j F j + 1
95 simpllr F : dom vol n F n F n + 1 k vol F k j n F n F n + 1
96 simpr F : dom vol n F n F n + 1 k vol F k j j
97 94 95 96 rspcdva F : dom vol n F n F n + 1 k vol F k j F j F j + 1
98 ssequn1 F j F j + 1 F j F j + 1 = F j + 1
99 97 98 sylib F : dom vol n F n F n + 1 k vol F k j F j F j + 1 = F j + 1
100 91 99 eqtr2id F : dom vol n F n F n + 1 k vol F k j F j + 1 = F j F j + 1 F j
101 100 fveq2d F : dom vol n F n F n + 1 k vol F k j vol F j + 1 = vol F j F j + 1 F j
102 simplll F : dom vol n F n F n + 1 k vol F k j F : dom vol
103 102 96 ffvelrnd F : dom vol n F n F n + 1 k vol F k j F j dom vol
104 peano2nn j j + 1
105 104 adantl F : dom vol n F n F n + 1 k vol F k j j + 1
106 102 105 ffvelrnd F : dom vol n F n F n + 1 k vol F k j F j + 1 dom vol
107 difmbl F j + 1 dom vol F j dom vol F j + 1 F j dom vol
108 106 103 107 syl2anc F : dom vol n F n F n + 1 k vol F k j F j + 1 F j dom vol
109 disjdif F j F j + 1 F j =
110 109 a1i F : dom vol n F n F n + 1 k vol F k j F j F j + 1 F j =
111 2fveq3 k = j vol F k = vol F j
112 111 eleq1d k = j vol F k vol F j
113 simplr F : dom vol n F n F n + 1 k vol F k j k vol F k
114 112 113 96 rspcdva F : dom vol n F n F n + 1 k vol F k j vol F j
115 mblvol F j + 1 F j dom vol vol F j + 1 F j = vol * F j + 1 F j
116 108 115 syl F : dom vol n F n F n + 1 k vol F k j vol F j + 1 F j = vol * F j + 1 F j
117 difssd F : dom vol n F n F n + 1 k vol F k j F j + 1 F j F j + 1
118 mblss F j + 1 dom vol F j + 1
119 106 118 syl F : dom vol n F n F n + 1 k vol F k j F j + 1
120 mblvol F j + 1 dom vol vol F j + 1 = vol * F j + 1
121 106 120 syl F : dom vol n F n F n + 1 k vol F k j vol F j + 1 = vol * F j + 1
122 2fveq3 k = j + 1 vol F k = vol F j + 1
123 122 eleq1d k = j + 1 vol F k vol F j + 1
124 123 113 105 rspcdva F : dom vol n F n F n + 1 k vol F k j vol F j + 1
125 121 124 eqeltrrd F : dom vol n F n F n + 1 k vol F k j vol * F j + 1
126 ovolsscl F j + 1 F j F j + 1 F j + 1 vol * F j + 1 vol * F j + 1 F j
127 117 119 125 126 syl3anc F : dom vol n F n F n + 1 k vol F k j vol * F j + 1 F j
128 116 127 eqeltrd F : dom vol n F n F n + 1 k vol F k j vol F j + 1 F j
129 volun F j dom vol F j + 1 F j dom vol F j F j + 1 F j = vol F j vol F j + 1 F j vol F j F j + 1 F j = vol F j + vol F j + 1 F j
130 103 108 110 114 128 129 syl32anc F : dom vol n F n F n + 1 k vol F k j vol F j F j + 1 F j = vol F j + vol F j + 1 F j
131 95 adantr F : dom vol n F n F n + 1 k vol F k j m 1 j n F n F n + 1
132 elfznn m 1 j m
133 132 adantl F : dom vol n F n F n + 1 k vol F k j m 1 j m
134 elfzuz3 m 1 j j m
135 134 adantl F : dom vol n F n F n + 1 k vol F k j m 1 j j m
136 volsuplem n F n F n + 1 m j m F m F j
137 131 133 135 136 syl12anc F : dom vol n F n F n + 1 k vol F k j m 1 j F m F j
138 137 ralrimiva F : dom vol n F n F n + 1 k vol F k j m 1 j F m F j
139 iunss m = 1 j F m F j m 1 j F m F j
140 138 139 sylibr F : dom vol n F n F n + 1 k vol F k j m = 1 j F m F j
141 96 6 eleqtrdi F : dom vol n F n F n + 1 k vol F k j j 1
142 eluzfz2 j 1 j 1 j
143 141 142 syl F : dom vol n F n F n + 1 k vol F k j j 1 j
144 fveq2 m = j F m = F j
145 144 ssiun2s j 1 j F j m = 1 j F m
146 143 145 syl F : dom vol n F n F n + 1 k vol F k j F j m = 1 j F m
147 140 146 eqssd F : dom vol n F n F n + 1 k vol F k j m = 1 j F m = F j
148 96 nnzd F : dom vol n F n F n + 1 k vol F k j j
149 fzval3 j 1 j = 1 ..^ j + 1
150 148 149 syl F : dom vol n F n F n + 1 k vol F k j 1 j = 1 ..^ j + 1
151 150 iuneq1d F : dom vol n F n F n + 1 k vol F k j m = 1 j F m = m 1 ..^ j + 1 F m
152 147 151 eqtr3d F : dom vol n F n F n + 1 k vol F k j F j = m 1 ..^ j + 1 F m
153 152 difeq2d F : dom vol n F n F n + 1 k vol F k j F j + 1 F j = F j + 1 m 1 ..^ j + 1 F m
154 153 fveq2d F : dom vol n F n F n + 1 k vol F k j vol F j + 1 F j = vol F j + 1 m 1 ..^ j + 1 F m
155 fveq2 k = j + 1 F k = F j + 1
156 oveq2 k = j + 1 1 ..^ k = 1 ..^ j + 1
157 156 iuneq1d k = j + 1 m 1 ..^ k F m = m 1 ..^ j + 1 F m
158 155 157 difeq12d k = j + 1 F k m 1 ..^ k F m = F j + 1 m 1 ..^ j + 1 F m
159 158 fveq2d k = j + 1 vol F k m 1 ..^ k F m = vol F j + 1 m 1 ..^ j + 1 F m
160 fvex vol F j + 1 m 1 ..^ j + 1 F m V
161 159 34 160 fvmpt j + 1 k vol F k m 1 ..^ k F m j + 1 = vol F j + 1 m 1 ..^ j + 1 F m
162 105 161 syl F : dom vol n F n F n + 1 k vol F k j k vol F k m 1 ..^ k F m j + 1 = vol F j + 1 m 1 ..^ j + 1 F m
163 154 162 eqtr4d F : dom vol n F n F n + 1 k vol F k j vol F j + 1 F j = k vol F k m 1 ..^ k F m j + 1
164 163 oveq2d F : dom vol n F n F n + 1 k vol F k j vol F j + vol F j + 1 F j = vol F j + k vol F k m 1 ..^ k F m j + 1
165 101 130 164 3eqtrd F : dom vol n F n F n + 1 k vol F k j vol F j + 1 = vol F j + k vol F k m 1 ..^ k F m j + 1
166 90 165 eqeq12d F : dom vol n F n F n + 1 k vol F k j seq 1 + k vol F k m 1 ..^ k F m j + 1 = vol F j + 1 seq 1 + k vol F k m 1 ..^ k F m j + k vol F k m 1 ..^ k F m j + 1 = vol F j + k vol F k m 1 ..^ k F m j + 1
167 87 166 syl5ibr F : dom vol n F n F n + 1 k vol F k j seq 1 + k vol F k m 1 ..^ k F m j = vol F j seq 1 + k vol F k m 1 ..^ k F m j + 1 = vol F j + 1
168 167 expcom j F : dom vol n F n F n + 1 k vol F k seq 1 + k vol F k m 1 ..^ k F m j = vol F j seq 1 + k vol F k m 1 ..^ k F m j + 1 = vol F j + 1
169 168 a2d j F : dom vol n F n F n + 1 k vol F k seq 1 + k vol F k m 1 ..^ k F m j = vol F j F : dom vol n F n F n + 1 k vol F k seq 1 + k vol F k m 1 ..^ k F m j + 1 = vol F j + 1
170 58 62 66 62 86 169 nnind j F : dom vol n F n F n + 1 k vol F k seq 1 + k vol F k m 1 ..^ k F m j = vol F j
171 170 impcom F : dom vol n F n F n + 1 k vol F k j seq 1 + k vol F k m 1 ..^ k F m j = vol F j
172 fvco3 F : dom vol j vol F j = vol F j
173 51 172 sylan F : dom vol n F n F n + 1 k vol F k j vol F j = vol F j
174 171 173 eqtr4d F : dom vol n F n F n + 1 k vol F k j seq 1 + k vol F k m 1 ..^ k F m j = vol F j
175 49 54 174 eqfnfvd F : dom vol n F n F n + 1 k vol F k seq 1 + k vol F k m 1 ..^ k F m = vol F
176 175 rneqd F : dom vol n F n F n + 1 k vol F k ran seq 1 + k vol F k m 1 ..^ k F m = ran vol F
177 rnco2 ran vol F = vol ran F
178 176 177 eqtrdi F : dom vol n F n F n + 1 k vol F k ran seq 1 + k vol F k m 1 ..^ k F m = vol ran F
179 178 supeq1d F : dom vol n F n F n + 1 k vol F k sup ran seq 1 + k vol F k m 1 ..^ k F m * < = sup vol ran F * <
180 36 43 179 3eqtr3d F : dom vol n F n F n + 1 k vol F k vol ran F = sup vol ran F * <
181 180 ex F : dom vol n F n F n + 1 k vol F k vol ran F = sup vol ran F * <
182 rexnal k ¬ vol F k ¬ k vol F k
183 fniunfv F Fn n F n = ran F
184 38 183 syl F : dom vol n F n = ran F
185 ffvelrn F : dom vol n F n dom vol
186 185 ralrimiva F : dom vol n F n dom vol
187 iunmbl n F n dom vol n F n dom vol
188 186 187 syl F : dom vol n F n dom vol
189 184 188 eqeltrrd F : dom vol ran F dom vol
190 189 ad2antrr F : dom vol n F n F n + 1 k ¬ vol F k ran F dom vol
191 mblss ran F dom vol ran F
192 190 191 syl F : dom vol n F n F n + 1 k ¬ vol F k ran F
193 ovolcl ran F vol * ran F *
194 192 193 syl F : dom vol n F n F n + 1 k ¬ vol F k vol * ran F *
195 pnfge vol * ran F * vol * ran F +∞
196 194 195 syl F : dom vol n F n F n + 1 k ¬ vol F k vol * ran F +∞
197 simprr F : dom vol n F n F n + 1 k ¬ vol F k ¬ vol F k
198 1 ad2ant2r F : dom vol n F n F n + 1 k ¬ vol F k F k dom vol
199 198 18 syl F : dom vol n F n F n + 1 k ¬ vol F k F k
200 ovolcl F k vol * F k *
201 199 200 syl F : dom vol n F n F n + 1 k ¬ vol F k vol * F k *
202 xrrebnd vol * F k * vol * F k −∞ < vol * F k vol * F k < +∞
203 201 202 syl F : dom vol n F n F n + 1 k ¬ vol F k vol * F k −∞ < vol * F k vol * F k < +∞
204 198 20 syl F : dom vol n F n F n + 1 k ¬ vol F k vol F k = vol * F k
205 204 eleq1d F : dom vol n F n F n + 1 k ¬ vol F k vol F k vol * F k
206 ovolge0 F k 0 vol * F k
207 mnflt0 −∞ < 0
208 mnfxr −∞ *
209 0xr 0 *
210 xrltletr −∞ * 0 * vol * F k * −∞ < 0 0 vol * F k −∞ < vol * F k
211 208 209 210 mp3an12 vol * F k * −∞ < 0 0 vol * F k −∞ < vol * F k
212 207 211 mpani vol * F k * 0 vol * F k −∞ < vol * F k
213 200 206 212 sylc F k −∞ < vol * F k
214 199 213 syl F : dom vol n F n F n + 1 k ¬ vol F k −∞ < vol * F k
215 214 biantrurd F : dom vol n F n F n + 1 k ¬ vol F k vol * F k < +∞ −∞ < vol * F k vol * F k < +∞
216 203 205 215 3bitr4d F : dom vol n F n F n + 1 k ¬ vol F k vol F k vol * F k < +∞
217 197 216 mtbid F : dom vol n F n F n + 1 k ¬ vol F k ¬ vol * F k < +∞
218 nltpnft vol * F k * vol * F k = +∞ ¬ vol * F k < +∞
219 201 218 syl F : dom vol n F n F n + 1 k ¬ vol F k vol * F k = +∞ ¬ vol * F k < +∞
220 217 219 mpbird F : dom vol n F n F n + 1 k ¬ vol F k vol * F k = +∞
221 38 ad2antrr F : dom vol n F n F n + 1 k ¬ vol F k F Fn
222 simprl F : dom vol n F n F n + 1 k ¬ vol F k k
223 fnfvelrn F Fn k F k ran F
224 221 222 223 syl2anc F : dom vol n F n F n + 1 k ¬ vol F k F k ran F
225 elssuni F k ran F F k ran F
226 224 225 syl F : dom vol n F n F n + 1 k ¬ vol F k F k ran F
227 ovolss F k ran F ran F vol * F k vol * ran F
228 226 192 227 syl2anc F : dom vol n F n F n + 1 k ¬ vol F k vol * F k vol * ran F
229 220 228 eqbrtrrd F : dom vol n F n F n + 1 k ¬ vol F k +∞ vol * ran F
230 pnfxr +∞ *
231 xrletri3 vol * ran F * +∞ * vol * ran F = +∞ vol * ran F +∞ +∞ vol * ran F
232 194 230 231 sylancl F : dom vol n F n F n + 1 k ¬ vol F k vol * ran F = +∞ vol * ran F +∞ +∞ vol * ran F
233 196 229 232 mpbir2and F : dom vol n F n F n + 1 k ¬ vol F k vol * ran F = +∞
234 mblvol ran F dom vol vol ran F = vol * ran F
235 190 234 syl F : dom vol n F n F n + 1 k ¬ vol F k vol ran F = vol * ran F
236 imassrn vol ran F ran vol
237 frn vol : dom vol 0 +∞ ran vol 0 +∞
238 50 237 ax-mp ran vol 0 +∞
239 iccssxr 0 +∞ *
240 238 239 sstri ran vol *
241 236 240 sstri vol ran F *
242 204 220 eqtrd F : dom vol n F n F n + 1 k ¬ vol F k vol F k = +∞
243 simpll F : dom vol n F n F n + 1 k ¬ vol F k F : dom vol
244 ffun vol : dom vol 0 +∞ Fun vol
245 50 244 ax-mp Fun vol
246 frn F : dom vol ran F dom vol
247 funfvima2 Fun vol ran F dom vol F k ran F vol F k vol ran F
248 245 246 247 sylancr F : dom vol F k ran F vol F k vol ran F
249 243 224 248 sylc F : dom vol n F n F n + 1 k ¬ vol F k vol F k vol ran F
250 242 249 eqeltrrd F : dom vol n F n F n + 1 k ¬ vol F k +∞ vol ran F
251 supxrpnf vol ran F * +∞ vol ran F sup vol ran F * < = +∞
252 241 250 251 sylancr F : dom vol n F n F n + 1 k ¬ vol F k sup vol ran F * < = +∞
253 233 235 252 3eqtr4d F : dom vol n F n F n + 1 k ¬ vol F k vol ran F = sup vol ran F * <
254 253 rexlimdvaa F : dom vol n F n F n + 1 k ¬ vol F k vol ran F = sup vol ran F * <
255 182 254 syl5bir F : dom vol n F n F n + 1 ¬ k vol F k vol ran F = sup vol ran F * <
256 181 255 pm2.61d F : dom vol n F n F n + 1 vol ran F = sup vol ran F * <