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 eqtr3id
 |-  ( ( 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 ) )