Metamath Proof Explorer

Theorem ovoliunlem2

Description: Lemma for ovoliun . (Contributed by Mario Carneiro, 12-Jun-2014)

Ref Expression
Hypotheses ovoliun.t 
|- T = seq 1 ( + , G )
ovoliun.g 
|- G = ( n e. NN |-> ( vol* ` A ) )
ovoliun.a 
|- ( ( ph /\ n e. NN ) -> A C_ RR )
ovoliun.v 
|- ( ( ph /\ n e. NN ) -> ( vol* ` A ) e. RR )
ovoliun.r 
|- ( ph -> sup ( ran T , RR* , < ) e. RR )
ovoliun.b 
|- ( ph -> B e. RR+ )
ovoliun.s 
|- S = seq 1 ( + , ( ( abs o. - ) o. ( F ` n ) ) )
ovoliun.u 
|- U = seq 1 ( + , ( ( abs o. - ) o. H ) )
ovoliun.h 
|- H = ( k e. NN |-> ( ( F ` ( 1st ` ( J ` k ) ) ) ` ( 2nd ` ( J ` k ) ) ) )
ovoliun.j 
|- ( ph -> J : NN -1-1-onto-> ( NN X. NN ) )
ovoliun.f 
|- ( ph -> F : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
ovoliun.x1 
|- ( ( ph /\ n e. NN ) -> A C_ U. ran ( (,) o. ( F ` n ) ) )
ovoliun.x2 
|- ( ( ph /\ n e. NN ) -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) )
Assertion ovoliunlem2 
|- ( ph -> ( vol* ` U_ n e. NN A ) <_ ( sup ( ran T , RR* , < ) + B ) )

Proof

Step Hyp Ref Expression
1 ovoliun.t 
 |-  T = seq 1 ( + , G )
2 ovoliun.g 
 |-  G = ( n e. NN |-> ( vol* ` A ) )
3 ovoliun.a 
 |-  ( ( ph /\ n e. NN ) -> A C_ RR )
4 ovoliun.v 
 |-  ( ( ph /\ n e. NN ) -> ( vol* ` A ) e. RR )
5 ovoliun.r 
 |-  ( ph -> sup ( ran T , RR* , < ) e. RR )
6 ovoliun.b 
 |-  ( ph -> B e. RR+ )
7 ovoliun.s 
 |-  S = seq 1 ( + , ( ( abs o. - ) o. ( F ` n ) ) )
8 ovoliun.u 
 |-  U = seq 1 ( + , ( ( abs o. - ) o. H ) )
9 ovoliun.h 
 |-  H = ( k e. NN |-> ( ( F ` ( 1st ` ( J ` k ) ) ) ` ( 2nd ` ( J ` k ) ) ) )
10 ovoliun.j 
 |-  ( ph -> J : NN -1-1-onto-> ( NN X. NN ) )
11 ovoliun.f 
 |-  ( ph -> F : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
12 ovoliun.x1 
 |-  ( ( ph /\ n e. NN ) -> A C_ U. ran ( (,) o. ( F ` n ) ) )
13 ovoliun.x2 
 |-  ( ( ph /\ n e. NN ) -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) )
14 3 ralrimiva 
 |-  ( ph -> A. n e. NN A C_ RR )
15 iunss 
 |-  ( U_ n e. NN A C_ RR <-> A. n e. NN A C_ RR )
16 14 15 sylibr 
 |-  ( ph -> U_ n e. NN A C_ RR )
17 ovolcl 
 |-  ( U_ n e. NN A C_ RR -> ( vol* ` U_ n e. NN A ) e. RR* )
18 16 17 syl 
 |-  ( ph -> ( vol* ` U_ n e. NN A ) e. RR* )
19 11 adantr 
 |-  ( ( ph /\ k e. NN ) -> F : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
20 f1of 
 |-  ( J : NN -1-1-onto-> ( NN X. NN ) -> J : NN --> ( NN X. NN ) )
21 10 20 syl 
 |-  ( ph -> J : NN --> ( NN X. NN ) )
22 21 ffvelrnda 
 |-  ( ( ph /\ k e. NN ) -> ( J ` k ) e. ( NN X. NN ) )
23 xp1st 
 |-  ( ( J ` k ) e. ( NN X. NN ) -> ( 1st ` ( J ` k ) ) e. NN )
24 22 23 syl 
 |-  ( ( ph /\ k e. NN ) -> ( 1st ` ( J ` k ) ) e. NN )
25 19 24 ffvelrnd 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( 1st ` ( J ` k ) ) ) e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
26 elovolmlem 
 |-  ( ( F ` ( 1st ` ( J ` k ) ) ) e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> ( F ` ( 1st ` ( J ` k ) ) ) : NN --> ( <_ i^i ( RR X. RR ) ) )
27 25 26 sylib 
 |-  ( ( ph /\ k e. NN ) -> ( F ` ( 1st ` ( J ` k ) ) ) : NN --> ( <_ i^i ( RR X. RR ) ) )
28 xp2nd 
 |-  ( ( J ` k ) e. ( NN X. NN ) -> ( 2nd ` ( J ` k ) ) e. NN )
29 22 28 syl 
 |-  ( ( ph /\ k e. NN ) -> ( 2nd ` ( J ` k ) ) e. NN )
30 27 29 ffvelrnd 
 |-  ( ( ph /\ k e. NN ) -> ( ( F ` ( 1st ` ( J ` k ) ) ) ` ( 2nd ` ( J ` k ) ) ) e. ( <_ i^i ( RR X. RR ) ) )
31 30 9 fmptd 
 |-  ( ph -> H : NN --> ( <_ i^i ( RR X. RR ) ) )
32 eqid 
 |-  ( ( abs o. - ) o. H ) = ( ( abs o. - ) o. H )
33 32 8 ovolsf 
 |-  ( H : NN --> ( <_ i^i ( RR X. RR ) ) -> U : NN --> ( 0 [,) +oo ) )
34 frn 
 |-  ( U : NN --> ( 0 [,) +oo ) -> ran U C_ ( 0 [,) +oo ) )
35 31 33 34 3syl 
 |-  ( ph -> ran U C_ ( 0 [,) +oo ) )
36 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
37 35 36 sstrdi 
 |-  ( ph -> ran U C_ RR* )
38 supxrcl 
 |-  ( ran U C_ RR* -> sup ( ran U , RR* , < ) e. RR* )
39 37 38 syl 
 |-  ( ph -> sup ( ran U , RR* , < ) e. RR* )
40 6 rpred 
 |-  ( ph -> B e. RR )
41 5 40 readdcld 
 |-  ( ph -> ( sup ( ran T , RR* , < ) + B ) e. RR )
42 41 rexrd 
 |-  ( ph -> ( sup ( ran T , RR* , < ) + B ) e. RR* )
43 eliun 
 |-  ( z e. U_ n e. NN A <-> E. n e. NN z e. A )
44 12 3adant3 
 |-  ( ( ph /\ n e. NN /\ z e. A ) -> A C_ U. ran ( (,) o. ( F ` n ) ) )
45 3 3adant3 
 |-  ( ( ph /\ n e. NN /\ z e. A ) -> A C_ RR )
46 11 ffvelrnda 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
47 elovolmlem 
 |-  ( ( F ` n ) e. ( ( <_ i^i ( RR X. RR ) ) ^m NN ) <-> ( F ` n ) : NN --> ( <_ i^i ( RR X. RR ) ) )
48 46 47 sylib 
 |-  ( ( ph /\ n e. NN ) -> ( F ` n ) : NN --> ( <_ i^i ( RR X. RR ) ) )
49 48 3adant3 
 |-  ( ( ph /\ n e. NN /\ z e. A ) -> ( F ` n ) : NN --> ( <_ i^i ( RR X. RR ) ) )
50 ovolfioo 
 |-  ( ( A C_ RR /\ ( F ` n ) : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( A C_ U. ran ( (,) o. ( F ` n ) ) <-> A. z e. A E. j e. NN ( ( 1st ` ( ( F ` n ) ` j ) ) < z /\ z < ( 2nd ` ( ( F ` n ) ` j ) ) ) ) )
51 45 49 50 syl2anc 
 |-  ( ( ph /\ n e. NN /\ z e. A ) -> ( A C_ U. ran ( (,) o. ( F ` n ) ) <-> A. z e. A E. j e. NN ( ( 1st ` ( ( F ` n ) ` j ) ) < z /\ z < ( 2nd ` ( ( F ` n ) ` j ) ) ) ) )
52 44 51 mpbid 
 |-  ( ( ph /\ n e. NN /\ z e. A ) -> A. z e. A E. j e. NN ( ( 1st ` ( ( F ` n ) ` j ) ) < z /\ z < ( 2nd ` ( ( F ` n ) ` j ) ) ) )
53 simp3 
 |-  ( ( ph /\ n e. NN /\ z e. A ) -> z e. A )
54 rsp 
 |-  ( A. z e. A E. j e. NN ( ( 1st ` ( ( F ` n ) ` j ) ) < z /\ z < ( 2nd ` ( ( F ` n ) ` j ) ) ) -> ( z e. A -> E. j e. NN ( ( 1st ` ( ( F ` n ) ` j ) ) < z /\ z < ( 2nd ` ( ( F ` n ) ` j ) ) ) ) )
55 52 53 54 sylc 
 |-  ( ( ph /\ n e. NN /\ z e. A ) -> E. j e. NN ( ( 1st ` ( ( F ` n ) ` j ) ) < z /\ z < ( 2nd ` ( ( F ` n ) ` j ) ) ) )
56 simpl1 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ph )
57 f1ocnv 
 |-  ( J : NN -1-1-onto-> ( NN X. NN ) -> `' J : ( NN X. NN ) -1-1-onto-> NN )
58 f1of 
 |-  ( `' J : ( NN X. NN ) -1-1-onto-> NN -> `' J : ( NN X. NN ) --> NN )
59 56 10 57 58 4syl 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> `' J : ( NN X. NN ) --> NN )
60 simpl2 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> n e. NN )
61 simpr 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> j e. NN )
62 59 60 61 fovrnd 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( n `' J j ) e. NN )
63 2fveq3 
 |-  ( k = ( n `' J j ) -> ( 1st ` ( J ` k ) ) = ( 1st ` ( J ` ( n `' J j ) ) ) )
64 63 fveq2d 
 |-  ( k = ( n `' J j ) -> ( F ` ( 1st ` ( J ` k ) ) ) = ( F ` ( 1st ` ( J ` ( n `' J j ) ) ) ) )
65 2fveq3 
 |-  ( k = ( n `' J j ) -> ( 2nd ` ( J ` k ) ) = ( 2nd ` ( J ` ( n `' J j ) ) ) )
66 64 65 fveq12d 
 |-  ( k = ( n `' J j ) -> ( ( F ` ( 1st ` ( J ` k ) ) ) ` ( 2nd ` ( J ` k ) ) ) = ( ( F ` ( 1st ` ( J ` ( n `' J j ) ) ) ) ` ( 2nd ` ( J ` ( n `' J j ) ) ) ) )
67 fvex 
 |-  ( ( F ` ( 1st ` ( J ` ( n `' J j ) ) ) ) ` ( 2nd ` ( J ` ( n `' J j ) ) ) ) e. _V
68 66 9 67 fvmpt 
 |-  ( ( n `' J j ) e. NN -> ( H ` ( n `' J j ) ) = ( ( F ` ( 1st ` ( J ` ( n `' J j ) ) ) ) ` ( 2nd ` ( J ` ( n `' J j ) ) ) ) )
69 62 68 syl 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( H ` ( n `' J j ) ) = ( ( F ` ( 1st ` ( J ` ( n `' J j ) ) ) ) ` ( 2nd ` ( J ` ( n `' J j ) ) ) ) )
70 df-ov 
 |-  ( n `' J j ) = ( `' J ` <. n , j >. )
71 70 fveq2i 
 |-  ( J ` ( n `' J j ) ) = ( J ` ( `' J ` <. n , j >. ) )
72 56 10 syl 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> J : NN -1-1-onto-> ( NN X. NN ) )
73 60 61 opelxpd 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> <. n , j >. e. ( NN X. NN ) )
74 f1ocnvfv2 
 |-  ( ( J : NN -1-1-onto-> ( NN X. NN ) /\ <. n , j >. e. ( NN X. NN ) ) -> ( J ` ( `' J ` <. n , j >. ) ) = <. n , j >. )
75 72 73 74 syl2anc 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( J ` ( `' J ` <. n , j >. ) ) = <. n , j >. )
76 71 75 eqtrid 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( J ` ( n `' J j ) ) = <. n , j >. )
77 76 fveq2d 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( 1st ` ( J ` ( n `' J j ) ) ) = ( 1st ` <. n , j >. ) )
78 vex 
 |-  n e. _V
79 vex 
 |-  j e. _V
80 78 79 op1st 
 |-  ( 1st ` <. n , j >. ) = n
81 77 80 eqtrdi 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( 1st ` ( J ` ( n `' J j ) ) ) = n )
82 81 fveq2d 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( F ` ( 1st ` ( J ` ( n `' J j ) ) ) ) = ( F ` n ) )
83 76 fveq2d 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( 2nd ` ( J ` ( n `' J j ) ) ) = ( 2nd ` <. n , j >. ) )
84 78 79 op2nd 
 |-  ( 2nd ` <. n , j >. ) = j
85 83 84 eqtrdi 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( 2nd ` ( J ` ( n `' J j ) ) ) = j )
86 82 85 fveq12d 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( ( F ` ( 1st ` ( J ` ( n `' J j ) ) ) ) ` ( 2nd ` ( J ` ( n `' J j ) ) ) ) = ( ( F ` n ) ` j ) )
87 69 86 eqtrd 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( H ` ( n `' J j ) ) = ( ( F ` n ) ` j ) )
88 87 fveq2d 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( 1st ` ( H ` ( n `' J j ) ) ) = ( 1st ` ( ( F ` n ) ` j ) ) )
89 88 breq1d 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( ( 1st ` ( H ` ( n `' J j ) ) ) < z <-> ( 1st ` ( ( F ` n ) ` j ) ) < z ) )
90 87 fveq2d 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( 2nd ` ( H ` ( n `' J j ) ) ) = ( 2nd ` ( ( F ` n ) ` j ) ) )
91 90 breq2d 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( z < ( 2nd ` ( H ` ( n `' J j ) ) ) <-> z < ( 2nd ` ( ( F ` n ) ` j ) ) ) )
92 89 91 anbi12d 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( ( ( 1st ` ( H ` ( n `' J j ) ) ) < z /\ z < ( 2nd ` ( H ` ( n `' J j ) ) ) ) <-> ( ( 1st ` ( ( F ` n ) ` j ) ) < z /\ z < ( 2nd ` ( ( F ` n ) ` j ) ) ) ) )
93 92 biimprd 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( ( ( 1st ` ( ( F ` n ) ` j ) ) < z /\ z < ( 2nd ` ( ( F ` n ) ` j ) ) ) -> ( ( 1st ` ( H ` ( n `' J j ) ) ) < z /\ z < ( 2nd ` ( H ` ( n `' J j ) ) ) ) ) )
94 2fveq3 
 |-  ( m = ( n `' J j ) -> ( 1st ` ( H ` m ) ) = ( 1st ` ( H ` ( n `' J j ) ) ) )
95 94 breq1d 
 |-  ( m = ( n `' J j ) -> ( ( 1st ` ( H ` m ) ) < z <-> ( 1st ` ( H ` ( n `' J j ) ) ) < z ) )
96 2fveq3 
 |-  ( m = ( n `' J j ) -> ( 2nd ` ( H ` m ) ) = ( 2nd ` ( H ` ( n `' J j ) ) ) )
97 96 breq2d 
 |-  ( m = ( n `' J j ) -> ( z < ( 2nd ` ( H ` m ) ) <-> z < ( 2nd ` ( H ` ( n `' J j ) ) ) ) )
98 95 97 anbi12d 
 |-  ( m = ( n `' J j ) -> ( ( ( 1st ` ( H ` m ) ) < z /\ z < ( 2nd ` ( H ` m ) ) ) <-> ( ( 1st ` ( H ` ( n `' J j ) ) ) < z /\ z < ( 2nd ` ( H ` ( n `' J j ) ) ) ) ) )
99 98 rspcev 
 |-  ( ( ( n `' J j ) e. NN /\ ( ( 1st ` ( H ` ( n `' J j ) ) ) < z /\ z < ( 2nd ` ( H ` ( n `' J j ) ) ) ) ) -> E. m e. NN ( ( 1st ` ( H ` m ) ) < z /\ z < ( 2nd ` ( H ` m ) ) ) )
100 62 93 99 syl6an 
 |-  ( ( ( ph /\ n e. NN /\ z e. A ) /\ j e. NN ) -> ( ( ( 1st ` ( ( F ` n ) ` j ) ) < z /\ z < ( 2nd ` ( ( F ` n ) ` j ) ) ) -> E. m e. NN ( ( 1st ` ( H ` m ) ) < z /\ z < ( 2nd ` ( H ` m ) ) ) ) )
101 100 rexlimdva 
 |-  ( ( ph /\ n e. NN /\ z e. A ) -> ( E. j e. NN ( ( 1st ` ( ( F ` n ) ` j ) ) < z /\ z < ( 2nd ` ( ( F ` n ) ` j ) ) ) -> E. m e. NN ( ( 1st ` ( H ` m ) ) < z /\ z < ( 2nd ` ( H ` m ) ) ) ) )
102 55 101 mpd 
 |-  ( ( ph /\ n e. NN /\ z e. A ) -> E. m e. NN ( ( 1st ` ( H ` m ) ) < z /\ z < ( 2nd ` ( H ` m ) ) ) )
103 102 rexlimdv3a 
 |-  ( ph -> ( E. n e. NN z e. A -> E. m e. NN ( ( 1st ` ( H ` m ) ) < z /\ z < ( 2nd ` ( H ` m ) ) ) ) )
104 43 103 syl5bi 
 |-  ( ph -> ( z e. U_ n e. NN A -> E. m e. NN ( ( 1st ` ( H ` m ) ) < z /\ z < ( 2nd ` ( H ` m ) ) ) ) )
105 104 ralrimiv 
 |-  ( ph -> A. z e. U_ n e. NN A E. m e. NN ( ( 1st ` ( H ` m ) ) < z /\ z < ( 2nd ` ( H ` m ) ) ) )
106 ovolfioo 
 |-  ( ( U_ n e. NN A C_ RR /\ H : NN --> ( <_ i^i ( RR X. RR ) ) ) -> ( U_ n e. NN A C_ U. ran ( (,) o. H ) <-> A. z e. U_ n e. NN A E. m e. NN ( ( 1st ` ( H ` m ) ) < z /\ z < ( 2nd ` ( H ` m ) ) ) ) )
107 16 31 106 syl2anc 
 |-  ( ph -> ( U_ n e. NN A C_ U. ran ( (,) o. H ) <-> A. z e. U_ n e. NN A E. m e. NN ( ( 1st ` ( H ` m ) ) < z /\ z < ( 2nd ` ( H ` m ) ) ) ) )
108 105 107 mpbird 
 |-  ( ph -> U_ n e. NN A C_ U. ran ( (,) o. H ) )
109 8 ovollb 
 |-  ( ( H : NN --> ( <_ i^i ( RR X. RR ) ) /\ U_ n e. NN A C_ U. ran ( (,) o. H ) ) -> ( vol* ` U_ n e. NN A ) <_ sup ( ran U , RR* , < ) )
110 31 108 109 syl2anc 
 |-  ( ph -> ( vol* ` U_ n e. NN A ) <_ sup ( ran U , RR* , < ) )
111 fzfi 
 |-  ( 1 ... j ) e. Fin
112 elfznn 
 |-  ( w e. ( 1 ... j ) -> w e. NN )
113 ffvelrn 
 |-  ( ( J : NN --> ( NN X. NN ) /\ w e. NN ) -> ( J ` w ) e. ( NN X. NN ) )
114 xp1st 
 |-  ( ( J ` w ) e. ( NN X. NN ) -> ( 1st ` ( J ` w ) ) e. NN )
115 nnre 
 |-  ( ( 1st ` ( J ` w ) ) e. NN -> ( 1st ` ( J ` w ) ) e. RR )
116 113 114 115 3syl 
 |-  ( ( J : NN --> ( NN X. NN ) /\ w e. NN ) -> ( 1st ` ( J ` w ) ) e. RR )
117 21 112 116 syl2an 
 |-  ( ( ph /\ w e. ( 1 ... j ) ) -> ( 1st ` ( J ` w ) ) e. RR )
118 117 ralrimiva 
 |-  ( ph -> A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) e. RR )
119 118 adantr 
 |-  ( ( ph /\ j e. NN ) -> A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) e. RR )
120 fimaxre3 
 |-  ( ( ( 1 ... j ) e. Fin /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) e. RR ) -> E. x e. RR A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ x )
121 111 119 120 sylancr 
 |-  ( ( ph /\ j e. NN ) -> E. x e. RR A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ x )
122 fllep1 
 |-  ( x e. RR -> x <_ ( ( |_ ` x ) + 1 ) )
123 122 ad2antlr 
 |-  ( ( ( ph /\ x e. RR ) /\ w e. ( 1 ... j ) ) -> x <_ ( ( |_ ` x ) + 1 ) )
124 117 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ w e. ( 1 ... j ) ) -> ( 1st ` ( J ` w ) ) e. RR )
125 simplr 
 |-  ( ( ( ph /\ x e. RR ) /\ w e. ( 1 ... j ) ) -> x e. RR )
126 flcl 
 |-  ( x e. RR -> ( |_ ` x ) e. ZZ )
127 126 peano2zd 
 |-  ( x e. RR -> ( ( |_ ` x ) + 1 ) e. ZZ )
128 127 zred 
 |-  ( x e. RR -> ( ( |_ ` x ) + 1 ) e. RR )
129 128 ad2antlr 
 |-  ( ( ( ph /\ x e. RR ) /\ w e. ( 1 ... j ) ) -> ( ( |_ ` x ) + 1 ) e. RR )
130 letr 
 |-  ( ( ( 1st ` ( J ` w ) ) e. RR /\ x e. RR /\ ( ( |_ ` x ) + 1 ) e. RR ) -> ( ( ( 1st ` ( J ` w ) ) <_ x /\ x <_ ( ( |_ ` x ) + 1 ) ) -> ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) )
131 124 125 129 130 syl3anc 
 |-  ( ( ( ph /\ x e. RR ) /\ w e. ( 1 ... j ) ) -> ( ( ( 1st ` ( J ` w ) ) <_ x /\ x <_ ( ( |_ ` x ) + 1 ) ) -> ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) )
132 123 131 mpan2d 
 |-  ( ( ( ph /\ x e. RR ) /\ w e. ( 1 ... j ) ) -> ( ( 1st ` ( J ` w ) ) <_ x -> ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) )
133 132 ralimdva 
 |-  ( ( ph /\ x e. RR ) -> ( A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ x -> A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) )
134 133 adantlr 
 |-  ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ x -> A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) )
135 simpll 
 |-  ( ( ( ph /\ j e. NN ) /\ ( x e. RR /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) ) -> ph )
136 135 3 sylan 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( x e. RR /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) ) /\ n e. NN ) -> A C_ RR )
137 135 4 sylan 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( x e. RR /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) ) /\ n e. NN ) -> ( vol* ` A ) e. RR )
138 135 5 syl 
 |-  ( ( ( ph /\ j e. NN ) /\ ( x e. RR /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) ) -> sup ( ran T , RR* , < ) e. RR )
139 135 6 syl 
 |-  ( ( ( ph /\ j e. NN ) /\ ( x e. RR /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) ) -> B e. RR+ )
140 135 10 syl 
 |-  ( ( ( ph /\ j e. NN ) /\ ( x e. RR /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) ) -> J : NN -1-1-onto-> ( NN X. NN ) )
141 135 11 syl 
 |-  ( ( ( ph /\ j e. NN ) /\ ( x e. RR /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) ) -> F : NN --> ( ( <_ i^i ( RR X. RR ) ) ^m NN ) )
142 135 12 sylan 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( x e. RR /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) ) /\ n e. NN ) -> A C_ U. ran ( (,) o. ( F ` n ) ) )
143 135 13 sylan 
 |-  ( ( ( ( ph /\ j e. NN ) /\ ( x e. RR /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) ) /\ n e. NN ) -> sup ( ran S , RR* , < ) <_ ( ( vol* ` A ) + ( B / ( 2 ^ n ) ) ) )
144 simplr 
 |-  ( ( ( ph /\ j e. NN ) /\ ( x e. RR /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) ) -> j e. NN )
145 127 ad2antrl 
 |-  ( ( ( ph /\ j e. NN ) /\ ( x e. RR /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) ) -> ( ( |_ ` x ) + 1 ) e. ZZ )
146 simprr 
 |-  ( ( ( ph /\ j e. NN ) /\ ( x e. RR /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) ) -> A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) )
147 1 2 136 137 138 139 7 8 9 140 141 142 143 144 145 146 ovoliunlem1 
 |-  ( ( ( ph /\ j e. NN ) /\ ( x e. RR /\ A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) ) ) -> ( U ` j ) <_ ( sup ( ran T , RR* , < ) + B ) )
148 147 expr 
 |-  ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ ( ( |_ ` x ) + 1 ) -> ( U ` j ) <_ ( sup ( ran T , RR* , < ) + B ) ) )
149 134 148 syld 
 |-  ( ( ( ph /\ j e. NN ) /\ x e. RR ) -> ( A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ x -> ( U ` j ) <_ ( sup ( ran T , RR* , < ) + B ) ) )
150 149 rexlimdva 
 |-  ( ( ph /\ j e. NN ) -> ( E. x e. RR A. w e. ( 1 ... j ) ( 1st ` ( J ` w ) ) <_ x -> ( U ` j ) <_ ( sup ( ran T , RR* , < ) + B ) ) )
151 121 150 mpd 
 |-  ( ( ph /\ j e. NN ) -> ( U ` j ) <_ ( sup ( ran T , RR* , < ) + B ) )
152 151 ralrimiva 
 |-  ( ph -> A. j e. NN ( U ` j ) <_ ( sup ( ran T , RR* , < ) + B ) )
153 ffn 
 |-  ( U : NN --> ( 0 [,) +oo ) -> U Fn NN )
154 breq1 
 |-  ( z = ( U ` j ) -> ( z <_ ( sup ( ran T , RR* , < ) + B ) <-> ( U ` j ) <_ ( sup ( ran T , RR* , < ) + B ) ) )
155 154 ralrn 
 |-  ( U Fn NN -> ( A. z e. ran U z <_ ( sup ( ran T , RR* , < ) + B ) <-> A. j e. NN ( U ` j ) <_ ( sup ( ran T , RR* , < ) + B ) ) )
156 31 33 153 155 4syl 
 |-  ( ph -> ( A. z e. ran U z <_ ( sup ( ran T , RR* , < ) + B ) <-> A. j e. NN ( U ` j ) <_ ( sup ( ran T , RR* , < ) + B ) ) )
157 152 156 mpbird 
 |-  ( ph -> A. z e. ran U z <_ ( sup ( ran T , RR* , < ) + B ) )
158 supxrleub 
 |-  ( ( ran U C_ RR* /\ ( sup ( ran T , RR* , < ) + B ) e. RR* ) -> ( sup ( ran U , RR* , < ) <_ ( sup ( ran T , RR* , < ) + B ) <-> A. z e. ran U z <_ ( sup ( ran T , RR* , < ) + B ) ) )
159 37 42 158 syl2anc 
 |-  ( ph -> ( sup ( ran U , RR* , < ) <_ ( sup ( ran T , RR* , < ) + B ) <-> A. z e. ran U z <_ ( sup ( ran T , RR* , < ) + B ) ) )
160 157 159 mpbird 
 |-  ( ph -> sup ( ran U , RR* , < ) <_ ( sup ( ran T , RR* , < ) + B ) )
161 18 39 42 110 160 xrletrd 
 |-  ( ph -> ( vol* ` U_ n e. NN A ) <_ ( sup ( ran T , RR* , < ) + B ) )