Metamath Proof Explorer

Theorem voliunlem1

Description: Lemma for voliun . (Contributed by Mario Carneiro, 20-Mar-2014)

Ref Expression
Hypotheses voliunlem.3 
|- ( ph -> F : NN --> dom vol )
voliunlem.5 
|- ( ph -> Disj_ i e. NN ( F ` i ) )
voliunlem1.6 
|- H = ( n e. NN |-> ( vol* ` ( E i^i ( F ` n ) ) ) )
voliunlem1.7 
|- ( ph -> E C_ RR )
voliunlem1.8 
|- ( ph -> ( vol* ` E ) e. RR )
Assertion voliunlem1 
|- ( ( ph /\ k e. NN ) -> ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( E \ U. ran F ) ) ) <_ ( vol* ` E ) )

Proof

Step Hyp Ref Expression
1 voliunlem.3 
 |-  ( ph -> F : NN --> dom vol )
2 voliunlem.5 
 |-  ( ph -> Disj_ i e. NN ( F ` i ) )
3 voliunlem1.6 
 |-  H = ( n e. NN |-> ( vol* ` ( E i^i ( F ` n ) ) ) )
4 voliunlem1.7 
 |-  ( ph -> E C_ RR )
5 voliunlem1.8 
 |-  ( ph -> ( vol* ` E ) e. RR )
6 difss 
 |-  ( E \ U. ran F ) C_ E
7 5 adantr 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` E ) e. RR )
8 ovolsscl 
 |-  ( ( ( E \ U. ran F ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E \ U. ran F ) ) e. RR )
9 6 4 7 8 mp3an2ani 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` ( E \ U. ran F ) ) e. RR )
10 difss 
 |-  ( E \ U_ n e. ( 1 ... k ) ( F ` n ) ) C_ E
11 ovolsscl 
 |-  ( ( ( E \ U_ n e. ( 1 ... k ) ( F ` n ) ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E \ U_ n e. ( 1 ... k ) ( F ` n ) ) ) e. RR )
12 10 4 7 11 mp3an2ani 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` ( E \ U_ n e. ( 1 ... k ) ( F ` n ) ) ) e. RR )
13 inss1 
 |-  ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) C_ E
14 ovolsscl 
 |-  ( ( ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) e. RR )
15 13 4 7 14 mp3an2ani 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) e. RR )
16 elfznn 
 |-  ( n e. ( 1 ... k ) -> n e. NN )
17 1 ffnd 
 |-  ( ph -> F Fn NN )
18 fnfvelrn 
 |-  ( ( F Fn NN /\ n e. NN ) -> ( F ` n ) e. ran F )
19 17 18 sylan 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. ran F )
20 elssuni 
 |-  ( ( F ` n ) e. ran F -> ( F ` n ) C_ U. ran F )
21 19 20 syl 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) C_ U. ran F )
22 16 21 sylan2 
 |-  ( ( ph /\ n e. ( 1 ... k ) ) -> ( F ` n ) C_ U. ran F )
23 22 ralrimiva 
 |-  ( ph -> A. n e. ( 1 ... k ) ( F ` n ) C_ U. ran F )
24 23 adantr 
 |-  ( ( ph /\ k e. NN ) -> A. n e. ( 1 ... k ) ( F ` n ) C_ U. ran F )
25 iunss 
 |-  ( U_ n e. ( 1 ... k ) ( F ` n ) C_ U. ran F <-> A. n e. ( 1 ... k ) ( F ` n ) C_ U. ran F )
26 24 25 sylibr 
 |-  ( ( ph /\ k e. NN ) -> U_ n e. ( 1 ... k ) ( F ` n ) C_ U. ran F )
27 26 sscond 
 |-  ( ( ph /\ k e. NN ) -> ( E \ U. ran F ) C_ ( E \ U_ n e. ( 1 ... k ) ( F ` n ) ) )
28 4 adantr 
 |-  ( ( ph /\ k e. NN ) -> E C_ RR )
29 10 28 sstrid 
 |-  ( ( ph /\ k e. NN ) -> ( E \ U_ n e. ( 1 ... k ) ( F ` n ) ) C_ RR )
30 ovolss 
 |-  ( ( ( E \ U. ran F ) C_ ( E \ U_ n e. ( 1 ... k ) ( F ` n ) ) /\ ( E \ U_ n e. ( 1 ... k ) ( F ` n ) ) C_ RR ) -> ( vol* ` ( E \ U. ran F ) ) <_ ( vol* ` ( E \ U_ n e. ( 1 ... k ) ( F ` n ) ) ) )
31 27 29 30 syl2anc 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` ( E \ U. ran F ) ) <_ ( vol* ` ( E \ U_ n e. ( 1 ... k ) ( F ` n ) ) ) )
32 9 12 15 31 leadd2dd 
 |-  ( ( ph /\ k e. NN ) -> ( ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) + ( vol* ` ( E \ U. ran F ) ) ) <_ ( ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) + ( vol* ` ( E \ U_ n e. ( 1 ... k ) ( F ` n ) ) ) ) )
33 oveq2 
 |-  ( z = 1 -> ( 1 ... z ) = ( 1 ... 1 ) )
34 33 iuneq1d 
 |-  ( z = 1 -> U_ n e. ( 1 ... z ) ( F ` n ) = U_ n e. ( 1 ... 1 ) ( F ` n ) )
35 34 eleq1d 
 |-  ( z = 1 -> ( U_ n e. ( 1 ... z ) ( F ` n ) e. dom vol <-> U_ n e. ( 1 ... 1 ) ( F ` n ) e. dom vol ) )
36 34 ineq2d 
 |-  ( z = 1 -> ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) = ( E i^i U_ n e. ( 1 ... 1 ) ( F ` n ) ) )
37 36 fveq2d 
 |-  ( z = 1 -> ( vol* ` ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) ) = ( vol* ` ( E i^i U_ n e. ( 1 ... 1 ) ( F ` n ) ) ) )
38 fveq2 
 |-  ( z = 1 -> ( seq 1 ( + , H ) ` z ) = ( seq 1 ( + , H ) ` 1 ) )
39 37 38 eqeq12d 
 |-  ( z = 1 -> ( ( vol* ` ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` z ) <-> ( vol* ` ( E i^i U_ n e. ( 1 ... 1 ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` 1 ) ) )
40 35 39 anbi12d 
 |-  ( z = 1 -> ( ( U_ n e. ( 1 ... z ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` z ) ) <-> ( U_ n e. ( 1 ... 1 ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... 1 ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` 1 ) ) ) )
41 40 imbi2d 
 |-  ( z = 1 -> ( ( ph -> ( U_ n e. ( 1 ... z ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` z ) ) ) <-> ( ph -> ( U_ n e. ( 1 ... 1 ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... 1 ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` 1 ) ) ) ) )
42 oveq2 
 |-  ( z = k -> ( 1 ... z ) = ( 1 ... k ) )
43 42 iuneq1d 
 |-  ( z = k -> U_ n e. ( 1 ... z ) ( F ` n ) = U_ n e. ( 1 ... k ) ( F ` n ) )
44 43 eleq1d 
 |-  ( z = k -> ( U_ n e. ( 1 ... z ) ( F ` n ) e. dom vol <-> U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol ) )
45 43 ineq2d 
 |-  ( z = k -> ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) = ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) )
46 45 fveq2d 
 |-  ( z = k -> ( vol* ` ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) ) = ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) )
47 fveq2 
 |-  ( z = k -> ( seq 1 ( + , H ) ` z ) = ( seq 1 ( + , H ) ` k ) )
48 46 47 eqeq12d 
 |-  ( z = k -> ( ( vol* ` ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` z ) <-> ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` k ) ) )
49 44 48 anbi12d 
 |-  ( z = k -> ( ( U_ n e. ( 1 ... z ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` z ) ) <-> ( U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` k ) ) ) )
50 49 imbi2d 
 |-  ( z = k -> ( ( ph -> ( U_ n e. ( 1 ... z ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` z ) ) ) <-> ( ph -> ( U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` k ) ) ) ) )
51 oveq2 
 |-  ( z = ( k + 1 ) -> ( 1 ... z ) = ( 1 ... ( k + 1 ) ) )
52 51 iuneq1d 
 |-  ( z = ( k + 1 ) -> U_ n e. ( 1 ... z ) ( F ` n ) = U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) )
53 52 eleq1d 
 |-  ( z = ( k + 1 ) -> ( U_ n e. ( 1 ... z ) ( F ` n ) e. dom vol <-> U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) e. dom vol ) )
54 52 ineq2d 
 |-  ( z = ( k + 1 ) -> ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) = ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) )
55 54 fveq2d 
 |-  ( z = ( k + 1 ) -> ( vol* ` ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) ) = ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) )
56 fveq2 
 |-  ( z = ( k + 1 ) -> ( seq 1 ( + , H ) ` z ) = ( seq 1 ( + , H ) ` ( k + 1 ) ) )
57 55 56 eqeq12d 
 |-  ( z = ( k + 1 ) -> ( ( vol* ` ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` z ) <-> ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` ( k + 1 ) ) ) )
58 53 57 anbi12d 
 |-  ( z = ( k + 1 ) -> ( ( U_ n e. ( 1 ... z ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` z ) ) <-> ( U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` ( k + 1 ) ) ) ) )
59 58 imbi2d 
 |-  ( z = ( k + 1 ) -> ( ( ph -> ( U_ n e. ( 1 ... z ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... z ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` z ) ) ) <-> ( ph -> ( U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` ( k + 1 ) ) ) ) ) )
60 1z 
 |-  1 e. ZZ
61 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
62 iuneq1 
 |-  ( ( 1 ... 1 ) = { 1 } -> U_ n e. ( 1 ... 1 ) ( F ` n ) = U_ n e. { 1 } ( F ` n ) )
63 60 61 62 mp2b 
 |-  U_ n e. ( 1 ... 1 ) ( F ` n ) = U_ n e. { 1 } ( F ` n )
64 1ex 
 |-  1 e. _V
65 fveq2 
 |-  ( n = 1 -> ( F ` n ) = ( F ` 1 ) )
66 64 65 iunxsn 
 |-  U_ n e. { 1 } ( F ` n ) = ( F ` 1 )
67 63 66 eqtri 
 |-  U_ n e. ( 1 ... 1 ) ( F ` n ) = ( F ` 1 )
68 1nn 
 |-  1 e. NN
69 ffvelrn 
 |-  ( ( F : NN --> dom vol /\ 1 e. NN ) -> ( F ` 1 ) e. dom vol )
70 1 68 69 sylancl 
 |-  ( ph -> ( F ` 1 ) e. dom vol )
71 67 70 eqeltrid 
 |-  ( ph -> U_ n e. ( 1 ... 1 ) ( F ` n ) e. dom vol )
72 65 ineq2d 
 |-  ( n = 1 -> ( E i^i ( F ` n ) ) = ( E i^i ( F ` 1 ) ) )
73 72 fveq2d 
 |-  ( n = 1 -> ( vol* ` ( E i^i ( F ` n ) ) ) = ( vol* ` ( E i^i ( F ` 1 ) ) ) )
74 fvex 
 |-  ( vol* ` ( E i^i ( F ` 1 ) ) ) e. _V
75 73 3 74 fvmpt 
 |-  ( 1 e. NN -> ( H ` 1 ) = ( vol* ` ( E i^i ( F ` 1 ) ) ) )
76 68 75 ax-mp 
 |-  ( H ` 1 ) = ( vol* ` ( E i^i ( F ` 1 ) ) )
77 seq1 
 |-  ( 1 e. ZZ -> ( seq 1 ( + , H ) ` 1 ) = ( H ` 1 ) )
78 60 77 ax-mp 
 |-  ( seq 1 ( + , H ) ` 1 ) = ( H ` 1 )
79 67 ineq2i 
 |-  ( E i^i U_ n e. ( 1 ... 1 ) ( F ` n ) ) = ( E i^i ( F ` 1 ) )
80 79 fveq2i 
 |-  ( vol* ` ( E i^i U_ n e. ( 1 ... 1 ) ( F ` n ) ) ) = ( vol* ` ( E i^i ( F ` 1 ) ) )
81 76 78 80 3eqtr4ri 
 |-  ( vol* ` ( E i^i U_ n e. ( 1 ... 1 ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` 1 )
82 71 81 jctir 
 |-  ( ph -> ( U_ n e. ( 1 ... 1 ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... 1 ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` 1 ) ) )
83 peano2nn 
 |-  ( k e. NN -> ( k + 1 ) e. NN )
84 ffvelrn 
 |-  ( ( F : NN --> dom vol /\ ( k + 1 ) e. NN ) -> ( F ` ( k + 1 ) ) e. dom vol )
85 1 83 84 syl2an 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) e. dom vol )
86 unmbl 
 |-  ( ( U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol /\ ( F ` ( k + 1 ) ) e. dom vol ) -> ( U_ n e. ( 1 ... k ) ( F ` n ) u. ( F ` ( k + 1 ) ) ) e. dom vol )
87 86 ex 
 |-  ( U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol -> ( ( F ` ( k + 1 ) ) e. dom vol -> ( U_ n e. ( 1 ... k ) ( F ` n ) u. ( F ` ( k + 1 ) ) ) e. dom vol ) )
88 85 87 syl5com 
 |-  ( ( ph /\ k e. NN ) -> ( U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol -> ( U_ n e. ( 1 ... k ) ( F ` n ) u. ( F ` ( k + 1 ) ) ) e. dom vol ) )
89 simpr 
 |-  ( ( ph /\ k e. NN ) -> k e. NN )
90 nnuz 
 |-  NN = ( ZZ>= ` 1 )
91 89 90 eleqtrdi 
 |-  ( ( ph /\ k e. NN ) -> k e. ( ZZ>= ` 1 ) )
92 fzsuc 
 |-  ( k e. ( ZZ>= ` 1 ) -> ( 1 ... ( k + 1 ) ) = ( ( 1 ... k ) u. { ( k + 1 ) } ) )
93 iuneq1 
 |-  ( ( 1 ... ( k + 1 ) ) = ( ( 1 ... k ) u. { ( k + 1 ) } ) -> U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) = U_ n e. ( ( 1 ... k ) u. { ( k + 1 ) } ) ( F ` n ) )
94 91 92 93 3syl 
 |-  ( ( ph /\ k e. NN ) -> U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) = U_ n e. ( ( 1 ... k ) u. { ( k + 1 ) } ) ( F ` n ) )
95 iunxun 
 |-  U_ n e. ( ( 1 ... k ) u. { ( k + 1 ) } ) ( F ` n ) = ( U_ n e. ( 1 ... k ) ( F ` n ) u. U_ n e. { ( k + 1 ) } ( F ` n ) )
96 ovex 
 |-  ( k + 1 ) e. _V
97 fveq2 
 |-  ( n = ( k + 1 ) -> ( F ` n ) = ( F ` ( k + 1 ) ) )
98 96 97 iunxsn 
 |-  U_ n e. { ( k + 1 ) } ( F ` n ) = ( F ` ( k + 1 ) )
99 98 uneq2i 
 |-  ( U_ n e. ( 1 ... k ) ( F ` n ) u. U_ n e. { ( k + 1 ) } ( F ` n ) ) = ( U_ n e. ( 1 ... k ) ( F ` n ) u. ( F ` ( k + 1 ) ) )
100 95 99 eqtri 
 |-  U_ n e. ( ( 1 ... k ) u. { ( k + 1 ) } ) ( F ` n ) = ( U_ n e. ( 1 ... k ) ( F ` n ) u. ( F ` ( k + 1 ) ) )
101 94 100 eqtrdi 
 |-  ( ( ph /\ k e. NN ) -> U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) = ( U_ n e. ( 1 ... k ) ( F ` n ) u. ( F ` ( k + 1 ) ) ) )
102 101 eleq1d 
 |-  ( ( ph /\ k e. NN ) -> ( U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) e. dom vol <-> ( U_ n e. ( 1 ... k ) ( F ` n ) u. ( F ` ( k + 1 ) ) ) e. dom vol ) )
103 88 102 sylibrd 
 |-  ( ( ph /\ k e. NN ) -> ( U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol -> U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) e. dom vol ) )
104 oveq1 
 |-  ( ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` k ) -> ( ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) + ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) ) = ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) ) )
105 inss1 
 |-  ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) C_ E
106 105 28 sstrid 
 |-  ( ( ph /\ k e. NN ) -> ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) C_ RR )
107 ovolsscl 
 |-  ( ( ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) e. RR )
108 105 4 7 107 mp3an2ani 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) e. RR )
109 mblsplit 
 |-  ( ( ( F ` ( k + 1 ) ) e. dom vol /\ ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) C_ RR /\ ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) e. RR ) -> ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) = ( ( vol* ` ( ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) i^i ( F ` ( k + 1 ) ) ) ) + ( vol* ` ( ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) \ ( F ` ( k + 1 ) ) ) ) ) )
110 85 106 108 109 syl3anc 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) = ( ( vol* ` ( ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) i^i ( F ` ( k + 1 ) ) ) ) + ( vol* ` ( ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) \ ( F ` ( k + 1 ) ) ) ) ) )
111 in32 
 |-  ( ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) i^i ( F ` ( k + 1 ) ) ) = ( ( E i^i ( F ` ( k + 1 ) ) ) i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) )
112 inss2 
 |-  ( E i^i ( F ` ( k + 1 ) ) ) C_ ( F ` ( k + 1 ) )
113 83 adantl 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) e. NN )
114 113 90 eleqtrdi 
 |-  ( ( ph /\ k e. NN ) -> ( k + 1 ) e. ( ZZ>= ` 1 ) )
115 eluzfz2 
 |-  ( ( k + 1 ) e. ( ZZ>= ` 1 ) -> ( k + 1 ) e. ( 1 ... ( k + 1 ) ) )
116 97 ssiun2s 
 |-  ( ( k + 1 ) e. ( 1 ... ( k + 1 ) ) -> ( F ` ( k + 1 ) ) C_ U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) )
117 114 115 116 3syl 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( k + 1 ) ) C_ U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) )
118 112 117 sstrid 
 |-  ( ( ph /\ k e. NN ) -> ( E i^i ( F ` ( k + 1 ) ) ) C_ U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) )
119 df-ss 
 |-  ( ( E i^i ( F ` ( k + 1 ) ) ) C_ U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) <-> ( ( E i^i ( F ` ( k + 1 ) ) ) i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) = ( E i^i ( F ` ( k + 1 ) ) ) )
120 118 119 sylib 
 |-  ( ( ph /\ k e. NN ) -> ( ( E i^i ( F ` ( k + 1 ) ) ) i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) = ( E i^i ( F ` ( k + 1 ) ) ) )
121 111 120 syl5eq 
 |-  ( ( ph /\ k e. NN ) -> ( ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) i^i ( F ` ( k + 1 ) ) ) = ( E i^i ( F ` ( k + 1 ) ) ) )
122 121 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` ( ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) i^i ( F ` ( k + 1 ) ) ) ) = ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) )
123 indif2 
 |-  ( E i^i ( U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) \ ( F ` ( k + 1 ) ) ) ) = ( ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) \ ( F ` ( k + 1 ) ) )
124 uncom 
 |-  ( U_ n e. ( 1 ... k ) ( F ` n ) u. ( F ` ( k + 1 ) ) ) = ( ( F ` ( k + 1 ) ) u. U_ n e. ( 1 ... k ) ( F ` n ) )
125 101 124 eqtr2di 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` ( k + 1 ) ) u. U_ n e. ( 1 ... k ) ( F ` n ) ) = U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) )
126 2 ad2antrr 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> Disj_ i e. NN ( F ` i ) )
127 113 adantr 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( k + 1 ) e. NN )
128 16 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> n e. NN )
129 128 nnred 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> n e. RR )
130 elfzle2 
 |-  ( n e. ( 1 ... k ) -> n <_ k )
131 130 adantl 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> n <_ k )
132 89 adantr 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> k e. NN )
133 nnleltp1 
 |-  ( ( n e. NN /\ k e. NN ) -> ( n <_ k <-> n < ( k + 1 ) ) )
134 128 132 133 syl2anc 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( n <_ k <-> n < ( k + 1 ) ) )
135 131 134 mpbid 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> n < ( k + 1 ) )
136 129 135 gtned 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( k + 1 ) =/= n )
137 fveq2 
 |-  ( i = ( k + 1 ) -> ( F ` i ) = ( F ` ( k + 1 ) ) )
138 fveq2 
 |-  ( i = n -> ( F ` i ) = ( F ` n ) )
139 137 138 disji2 
 |-  ( ( Disj_ i e. NN ( F ` i ) /\ ( ( k + 1 ) e. NN /\ n e. NN ) /\ ( k + 1 ) =/= n ) -> ( ( F ` ( k + 1 ) ) i^i ( F ` n ) ) = (/) )
140 126 127 128 136 139 syl121anc 
 |-  ( ( ( ph /\ k e. NN ) /\ n e. ( 1 ... k ) ) -> ( ( F ` ( k + 1 ) ) i^i ( F ` n ) ) = (/) )
141 140 iuneq2dv 
 |-  ( ( ph /\ k e. NN ) -> U_ n e. ( 1 ... k ) ( ( F ` ( k + 1 ) ) i^i ( F ` n ) ) = U_ n e. ( 1 ... k ) (/) )
142 iunin2 
 |-  U_ n e. ( 1 ... k ) ( ( F ` ( k + 1 ) ) i^i ( F ` n ) ) = ( ( F ` ( k + 1 ) ) i^i U_ n e. ( 1 ... k ) ( F ` n ) )
143 iun0 
 |-  U_ n e. ( 1 ... k ) (/) = (/)
144 141 142 143 3eqtr3g 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` ( k + 1 ) ) i^i U_ n e. ( 1 ... k ) ( F ` n ) ) = (/) )
145 uneqdifeq 
 |-  ( ( ( F ` ( k + 1 ) ) C_ U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) /\ ( ( F ` ( k + 1 ) ) i^i U_ n e. ( 1 ... k ) ( F ` n ) ) = (/) ) -> ( ( ( F ` ( k + 1 ) ) u. U_ n e. ( 1 ... k ) ( F ` n ) ) = U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) <-> ( U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) \ ( F ` ( k + 1 ) ) ) = U_ n e. ( 1 ... k ) ( F ` n ) ) )
146 117 144 145 syl2anc 
 |-  ( ( ph /\ k e. NN ) -> ( ( ( F ` ( k + 1 ) ) u. U_ n e. ( 1 ... k ) ( F ` n ) ) = U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) <-> ( U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) \ ( F ` ( k + 1 ) ) ) = U_ n e. ( 1 ... k ) ( F ` n ) ) )
147 125 146 mpbid 
 |-  ( ( ph /\ k e. NN ) -> ( U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) \ ( F ` ( k + 1 ) ) ) = U_ n e. ( 1 ... k ) ( F ` n ) )
148 147 ineq2d 
 |-  ( ( ph /\ k e. NN ) -> ( E i^i ( U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) \ ( F ` ( k + 1 ) ) ) ) = ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) )
149 123 148 syl5eqr 
 |-  ( ( ph /\ k e. NN ) -> ( ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) \ ( F ` ( k + 1 ) ) ) = ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) )
150 149 fveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` ( ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) \ ( F ` ( k + 1 ) ) ) ) = ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) )
151 122 150 oveq12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( vol* ` ( ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) i^i ( F ` ( k + 1 ) ) ) ) + ( vol* ` ( ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) \ ( F ` ( k + 1 ) ) ) ) ) = ( ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) + ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) ) )
152 inss1 
 |-  ( E i^i ( F ` ( k + 1 ) ) ) C_ E
153 ovolsscl 
 |-  ( ( ( E i^i ( F ` ( k + 1 ) ) ) C_ E /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) e. RR )
154 152 4 7 153 mp3an2ani 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) e. RR )
155 154 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) e. CC )
156 15 recnd 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) e. CC )
157 155 156 addcomd 
 |-  ( ( ph /\ k e. NN ) -> ( ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) + ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) ) = ( ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) + ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) ) )
158 110 151 157 3eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) = ( ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) + ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) ) )
159 seqp1 
 |-  ( k e. ( ZZ>= ` 1 ) -> ( seq 1 ( + , H ) ` ( k + 1 ) ) = ( ( seq 1 ( + , H ) ` k ) + ( H ` ( k + 1 ) ) ) )
160 91 159 syl 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , H ) ` ( k + 1 ) ) = ( ( seq 1 ( + , H ) ` k ) + ( H ` ( k + 1 ) ) ) )
161 97 ineq2d 
 |-  ( n = ( k + 1 ) -> ( E i^i ( F ` n ) ) = ( E i^i ( F ` ( k + 1 ) ) ) )
162 161 fveq2d 
 |-  ( n = ( k + 1 ) -> ( vol* ` ( E i^i ( F ` n ) ) ) = ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) )
163 fvex 
 |-  ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) e. _V
164 162 3 163 fvmpt 
 |-  ( ( k + 1 ) e. NN -> ( H ` ( k + 1 ) ) = ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) )
165 113 164 syl 
 |-  ( ( ph /\ k e. NN ) -> ( H ` ( k + 1 ) ) = ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) )
166 165 oveq2d 
 |-  ( ( ph /\ k e. NN ) -> ( ( seq 1 ( + , H ) ` k ) + ( H ` ( k + 1 ) ) ) = ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) ) )
167 160 166 eqtrd 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , H ) ` ( k + 1 ) ) = ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) ) )
168 158 167 eqeq12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` ( k + 1 ) ) <-> ( ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) + ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) ) = ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( E i^i ( F ` ( k + 1 ) ) ) ) ) ) )
169 104 168 syl5ibr 
 |-  ( ( ph /\ k e. NN ) -> ( ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` k ) -> ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` ( k + 1 ) ) ) )
170 103 169 anim12d 
 |-  ( ( ph /\ k e. NN ) -> ( ( U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` k ) ) -> ( U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` ( k + 1 ) ) ) ) )
171 170 expcom 
 |-  ( k e. NN -> ( ph -> ( ( U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` k ) ) -> ( U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` ( k + 1 ) ) ) ) ) )
172 171 a2d 
 |-  ( k e. NN -> ( ( ph -> ( U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` k ) ) ) -> ( ph -> ( U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... ( k + 1 ) ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` ( k + 1 ) ) ) ) ) )
173 41 50 59 50 82 172 nnind 
 |-  ( k e. NN -> ( ph -> ( U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` k ) ) ) )
174 173 impcom 
 |-  ( ( ph /\ k e. NN ) -> ( U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol /\ ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` k ) ) )
175 174 simprd 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) = ( seq 1 ( + , H ) ` k ) )
176 175 eqcomd 
 |-  ( ( ph /\ k e. NN ) -> ( seq 1 ( + , H ) ` k ) = ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) )
177 176 oveq1d 
 |-  ( ( ph /\ k e. NN ) -> ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( E \ U. ran F ) ) ) = ( ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) + ( vol* ` ( E \ U. ran F ) ) ) )
178 174 simpld 
 |-  ( ( ph /\ k e. NN ) -> U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol )
179 mblsplit 
 |-  ( ( U_ n e. ( 1 ... k ) ( F ` n ) e. dom vol /\ E C_ RR /\ ( vol* ` E ) e. RR ) -> ( vol* ` E ) = ( ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) + ( vol* ` ( E \ U_ n e. ( 1 ... k ) ( F ` n ) ) ) ) )
180 178 28 7 179 syl3anc 
 |-  ( ( ph /\ k e. NN ) -> ( vol* ` E ) = ( ( vol* ` ( E i^i U_ n e. ( 1 ... k ) ( F ` n ) ) ) + ( vol* ` ( E \ U_ n e. ( 1 ... k ) ( F ` n ) ) ) ) )
181 32 177 180 3brtr4d 
 |-  ( ( ph /\ k e. NN ) -> ( ( seq 1 ( + , H ) ` k ) + ( vol* ` ( E \ U. ran F ) ) ) <_ ( vol* ` E ) )