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 : NN --> dom vol /\ A. n e. NN ( F ` n ) C_ ( F ` ( n + 1 ) ) ) -> ( vol ` U. ran F ) = sup ( ( vol " ran F ) , RR* , < ) )

Proof

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