Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ovnsubaddlem1 Structured version   Unicode version

Theorem ovnsubaddlem1 38296
Description: The Lebesgue outer measure is subadditive. Proposition 115D (a)(iv) of [Fremlin1] p. 31 . (Contributed by Glauco Siliprandi, 11-Oct-2020.)
Hypotheses
Ref Expression
ovnsubaddlem1.x  |-  ( ph  ->  X  e.  Fin )
ovnsubaddlem1.n0  |-  ( ph  ->  X  =/=  (/) )
ovnsubaddlem1.a  |-  ( ph  ->  A : NN --> ~P ( RR  ^m  X ) )
ovnsubaddlem1.e  |-  ( ph  ->  E  e.  RR+ )
ovnsubaddlem1.z  |-  Z  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  { z  e.  RR*  |  E. i  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN ) ( a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( i `  j
) ) `  k
)  /\  z  =  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) } )
ovnsubaddlem1.c  |-  C  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  { h  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  |  a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) } )
ovnsubaddlem1.l  |-  L  =  ( i  e.  ( ( RR  X.  RR )  ^m  X )  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  i ) `
 k ) ) )
ovnsubaddlem1.d  |-  D  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  ( e  e.  RR+  |->  { i  e.  ( C `  a )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) } ) )
ovnsubaddlem1.i  |-  ( (
ph  /\  n  e.  NN )  ->  ( I `
 n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) )
ovnsubaddlem1.f  |-  ( ph  ->  F : NN -1-1-onto-> ( NN  X.  NN ) )
ovnsubaddlem1.g  |-  G  =  ( m  e.  NN  |->  ( ( I `  ( 1st `  ( F `
 m ) ) ) `  ( 2nd `  ( F `  m
) ) ) )
Assertion
Ref Expression
ovnsubaddlem1  |-  ( ph  ->  ( (voln* `  X ) `  U_ n  e.  NN  ( A `  n ) )  <_ 
( (Σ^ `  ( n  e.  NN  |->  ( (voln* `  X ) `  ( A `  n )
) ) ) +e E ) )
Distinct variable groups:    A, a,
e, i, n    A, h, a, n    z, A, a, i, n    C, a, e, i    D, n   
e, E, i, n    F, a, e, i, j, m, n    h, F, k, a, j, m, n    i, k, G, j, m, n    h, I, j, k, m, n   
i, I    L, a,
e, i, j, m, n    X, a, e, i, j, m, n    h, X, k    z, X, j, k    ph, a, e, i, j, m, n    ph, k
Allowed substitution hints:    ph( z, h)    A( j, k, m)    C( z, h, j, k, m, n)    D( z, e, h, i, j, k, m, a)    E( z, h, j, k, m, a)    F( z)    G( z, e, h, a)    I( z, e, a)    L( z, h, k)    Z( z, e, h, i, j, k, m, n, a)

Proof of Theorem ovnsubaddlem1
Dummy variable  p is distinct from all other variables.
StepHypRef Expression
1 ovnsubaddlem1.x . . . 4  |-  ( ph  ->  X  e.  Fin )
2 ovnsubaddlem1.a . . . . . . . . 9  |-  ( ph  ->  A : NN --> ~P ( RR  ^m  X ) )
32adantr 466 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  A : NN
--> ~P ( RR  ^m  X ) )
4 simpr 462 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  n  e.  NN )
53, 4ffvelrnd 6038 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( A `
 n )  e. 
~P ( RR  ^m  X ) )
6 elpwi 3990 . . . . . . 7  |-  ( ( A `  n )  e.  ~P ( RR 
^m  X )  -> 
( A `  n
)  C_  ( RR  ^m  X ) )
75, 6syl 17 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( A `
 n )  C_  ( RR  ^m  X ) )
87ralrimiva 2836 . . . . 5  |-  ( ph  ->  A. n  e.  NN  ( A `  n ) 
C_  ( RR  ^m  X ) )
9 iunss 4340 . . . . 5  |-  ( U_ n  e.  NN  ( A `  n )  C_  ( RR  ^m  X
)  <->  A. n  e.  NN  ( A `  n ) 
C_  ( RR  ^m  X ) )
108, 9sylibr 215 . . . 4  |-  ( ph  ->  U_ n  e.  NN  ( A `  n ) 
C_  ( RR  ^m  X ) )
111, 10ovnxrcl 38295 . . 3  |-  ( ph  ->  ( (voln* `  X ) `  U_ n  e.  NN  ( A `  n ) )  e. 
RR* )
12 nfv 1755 . . . 4  |-  F/ m ph
13 nnex 10622 . . . . 5  |-  NN  e.  _V
1413a1i 11 . . . 4  |-  ( ph  ->  NN  e.  _V )
15 icossicc 11728 . . . . 5  |-  ( 0 [,) +oo )  C_  ( 0 [,] +oo )
16 nfv 1755 . . . . . 6  |-  F/ k ( ph  /\  m  e.  NN )
17 simpl 458 . . . . . . 7  |-  ( (
ph  /\  m  e.  NN )  ->  ph )
1817, 1syl 17 . . . . . 6  |-  ( (
ph  /\  m  e.  NN )  ->  X  e. 
Fin )
19 ovnsubaddlem1.l . . . . . 6  |-  L  =  ( i  e.  ( ( RR  X.  RR )  ^m  X )  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  i ) `
 k ) ) )
20 ovnsubaddlem1.f . . . . . . . . . . . 12  |-  ( ph  ->  F : NN -1-1-onto-> ( NN  X.  NN ) )
21 f1of 5831 . . . . . . . . . . . 12  |-  ( F : NN -1-1-onto-> ( NN  X.  NN )  ->  F : NN --> ( NN  X.  NN ) )
2220, 21syl 17 . . . . . . . . . . 11  |-  ( ph  ->  F : NN --> ( NN 
X.  NN ) )
2322adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  F : NN
--> ( NN  X.  NN ) )
24 simpr 462 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  m  e.  NN )
2523, 24ffvelrnd 6038 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  NN )  ->  ( F `
 m )  e.  ( NN  X.  NN ) )
26 xp1st 6837 . . . . . . . . 9  |-  ( ( F `  m )  e.  ( NN  X.  NN )  ->  ( 1st `  ( F `  m
) )  e.  NN )
2725, 26syl 17 . . . . . . . 8  |-  ( (
ph  /\  m  e.  NN )  ->  ( 1st `  ( F `  m
) )  e.  NN )
28 xp2nd 6838 . . . . . . . . 9  |-  ( ( F `  m )  e.  ( NN  X.  NN )  ->  ( 2nd `  ( F `  m
) )  e.  NN )
2925, 28syl 17 . . . . . . . 8  |-  ( (
ph  /\  m  e.  NN )  ->  ( 2nd `  ( F `  m
) )  e.  NN )
30 fvex 5891 . . . . . . . . 9  |-  ( 2nd `  ( F `  m
) )  e.  _V
31 eleq1 2495 . . . . . . . . . . 11  |-  ( j  =  ( 2nd `  ( F `  m )
)  ->  ( j  e.  NN  <->  ( 2nd `  ( F `  m )
)  e.  NN ) )
32313anbi3d 1341 . . . . . . . . . 10  |-  ( j  =  ( 2nd `  ( F `  m )
)  ->  ( ( ph  /\  ( 1st `  ( F `  m )
)  e.  NN  /\  j  e.  NN )  <->  (
ph  /\  ( 1st `  ( F `  m
) )  e.  NN  /\  ( 2nd `  ( F `  m )
)  e.  NN ) ) )
33 fveq2 5881 . . . . . . . . . . 11  |-  ( j  =  ( 2nd `  ( F `  m )
)  ->  ( (
I `  ( 1st `  ( F `  m
) ) ) `  j )  =  ( ( I `  ( 1st `  ( F `  m ) ) ) `
 ( 2nd `  ( F `  m )
) ) )
3433feq1d 5732 . . . . . . . . . 10  |-  ( j  =  ( 2nd `  ( F `  m )
)  ->  ( (
( I `  ( 1st `  ( F `  m ) ) ) `
 j ) : X --> ( RR  X.  RR )  <->  ( ( I `
 ( 1st `  ( F `  m )
) ) `  ( 2nd `  ( F `  m ) ) ) : X --> ( RR 
X.  RR ) ) )
3532, 34imbi12d 321 . . . . . . . . 9  |-  ( j  =  ( 2nd `  ( F `  m )
)  ->  ( (
( ph  /\  ( 1st `  ( F `  m ) )  e.  NN  /\  j  e.  NN )  ->  (
( I `  ( 1st `  ( F `  m ) ) ) `
 j ) : X --> ( RR  X.  RR ) )  <->  ( ( ph  /\  ( 1st `  ( F `  m )
)  e.  NN  /\  ( 2nd `  ( F `
 m ) )  e.  NN )  -> 
( ( I `  ( 1st `  ( F `
 m ) ) ) `  ( 2nd `  ( F `  m
) ) ) : X --> ( RR  X.  RR ) ) ) )
36 fvex 5891 . . . . . . . . . 10  |-  ( 1st `  ( F `  m
) )  e.  _V
37 eleq1 2495 . . . . . . . . . . . 12  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( n  e.  NN  <->  ( 1st `  ( F `  m )
)  e.  NN ) )
38373anbi2d 1340 . . . . . . . . . . 11  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( ( ph  /\  n  e.  NN  /\  j  e.  NN )  <-> 
( ph  /\  ( 1st `  ( F `  m ) )  e.  NN  /\  j  e.  NN ) ) )
39 fveq2 5881 . . . . . . . . . . . . 13  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( I `  n )  =  ( I `  ( 1st `  ( F `  m
) ) ) )
4039fveq1d 5883 . . . . . . . . . . . 12  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( (
I `  n ) `  j )  =  ( ( I `  ( 1st `  ( F `  m ) ) ) `
 j ) )
4140feq1d 5732 . . . . . . . . . . 11  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( (
( I `  n
) `  j ) : X --> ( RR  X.  RR )  <->  ( ( I `
 ( 1st `  ( F `  m )
) ) `  j
) : X --> ( RR 
X.  RR ) ) )
4238, 41imbi12d 321 . . . . . . . . . 10  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( (
( ph  /\  n  e.  NN  /\  j  e.  NN )  ->  (
( I `  n
) `  j ) : X --> ( RR  X.  RR ) )  <->  ( ( ph  /\  ( 1st `  ( F `  m )
)  e.  NN  /\  j  e.  NN )  ->  ( ( I `  ( 1st `  ( F `
 m ) ) ) `  j ) : X --> ( RR 
X.  RR ) ) ) )
43 ovnsubaddlem1.c . . . . . . . . . . . . . . . . . . . 20  |-  C  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  { h  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  |  a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) } )
4443a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  C  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  { h  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  |  a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) } ) )
45 sseq1 3485 . . . . . . . . . . . . . . . . . . . . 21  |-  ( a  =  ( A `  n )  ->  (
a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
)  <->  ( A `  n )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) ) )
4645rabbidv 3071 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( A `  n )  ->  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  a  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
h `  j )
) `  k ) }  =  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  ( A `  n )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) } )
4746adantl 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  a  =  ( A `  n ) )  ->  { h  e.  (
( ( RR  X.  RR )  ^m  X )  ^m  NN )  |  a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) }  =  {
h  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  |  ( A `  n )  C_ 
U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  (
h `  j )
) `  k ) } )
48 ovex 6333 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  e.  _V
4948rabex 4575 . . . . . . . . . . . . . . . . . . . 20  |-  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  ( A `  n )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) }  e.  _V
5049a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  ( A `  n )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) }  e.  _V )
5144, 47, 5, 50fvmptd 5970 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  ( C `
 ( A `  n ) )  =  { h  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  |  ( A `  n
)  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) } )
52 ssrab2 3546 . . . . . . . . . . . . . . . . . . 19  |-  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  ( A `  n )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) }  C_  (
( ( RR  X.  RR )  ^m  X )  ^m  NN )
5352a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  ( A `  n )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) }  C_  (
( ( RR  X.  RR )  ^m  X )  ^m  NN ) )
5451, 53eqsstrd 3498 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( C `
 ( A `  n ) )  C_  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN ) )
55 ovnsubaddlem1.d . . . . . . . . . . . . . . . . . . . . . 22  |-  D  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  ( e  e.  RR+  |->  { i  e.  ( C `  a )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) } ) )
5655a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  NN )  ->  D  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  ( e  e.  RR+  |->  { i  e.  ( C `  a )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) } ) ) )
57 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  ( A `  n )  ->  ( C `  a )  =  ( C `  ( A `  n ) ) )
5857eleq2d 2492 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  ( A `  n )  ->  (
i  e.  ( C `
 a )  <->  i  e.  ( C `  ( A `
 n ) ) ) )
59 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  ( A `  n )  ->  (
(voln* `  X ) `  a
)  =  ( (voln* `  X
) `  ( A `  n ) ) )
6059oveq1d 6320 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  ( A `  n )  ->  (
( (voln* `  X ) `  a
) +e e )  =  ( ( (voln* `  X ) `  ( A `  n )
) +e e ) )
6160breq2d 4435 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( a  =  ( A `  n )  ->  (
(Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e )  <->  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e e ) ) )
6258, 61anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  =  ( A `  n )  ->  (
( i  e.  ( C `  a )  /\  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) )  <->  ( i  e.  ( C `  ( A `  n )
)  /\  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e e ) ) ) )
6362rabbidva2 3069 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( a  =  ( A `  n )  ->  { i  e.  ( C `  a )  |  (Σ^ `  (
j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) }  =  {
i  e.  ( C `
 ( A `  n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e e ) } )
6463mpteq2dv 4511 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( a  =  ( A `  n )  ->  (
e  e.  RR+  |->  { i  e.  ( C `  a )  |  (Σ^ `  (
j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) } )  =  ( e  e.  RR+  |->  { i  e.  ( C `  ( A `
 n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e e ) } ) )
6564adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  a  =  ( A `  n ) )  -> 
( e  e.  RR+  |->  { i  e.  ( C `  a )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) } )  =  ( e  e.  RR+  |->  { i  e.  ( C `  ( A `
 n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e e ) } ) )
66 rpex 37523 . . . . . . . . . . . . . . . . . . . . . . 23  |-  RR+  e.  _V
6766mptex 6151 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( e  e.  RR+  |->  { i  e.  ( C `  ( A `  n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e e ) } )  e. 
_V
6867a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  NN )  ->  ( e  e.  RR+  |->  { i  e.  ( C `  ( A `  n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e e ) } )  e. 
_V )
6956, 65, 5, 68fvmptd 5970 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  ( D `
 ( A `  n ) )  =  ( e  e.  RR+  |->  { i  e.  ( C `  ( A `
 n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e e ) } ) )
70 oveq2 6313 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( e  =  ( E  / 
( 2 ^ n
) )  ->  (
( (voln* `  X ) `  ( A `  n )
) +e e )  =  ( ( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) ) )
7170breq2d 4435 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( e  =  ( E  / 
( 2 ^ n
) )  ->  (
(Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e e )  <->  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) ) ) )
7271rabbidv 3071 . . . . . . . . . . . . . . . . . . . . 21  |-  ( e  =  ( E  / 
( 2 ^ n
) )  ->  { i  e.  ( C `  ( A `  n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e e ) }  =  {
i  e.  ( C `
 ( A `  n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) ) } )
7372adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  e  =  ( E  / 
( 2 ^ n
) ) )  ->  { i  e.  ( C `  ( A `
 n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e e ) }  =  {
i  e.  ( C `
 ( A `  n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) ) } )
74 ovnsubaddlem1.e . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  E  e.  RR+ )
7574adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  NN )  ->  E  e.  RR+ )
76 2nn 10774 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  2  e.  NN
7776a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  NN  ->  2  e.  NN )
78 nnnn0 10883 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  e.  NN  ->  n  e.  NN0 )
7977, 78nnexpcld 12443 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  e.  NN  ->  (
2 ^ n )  e.  NN )
8079nnrpd 11346 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  NN  ->  (
2 ^ n )  e.  RR+ )
8180adantl 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2 ^ n )  e.  RR+ )
8275, 81rpdivcld 11365 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  ( E  /  ( 2 ^ n ) )  e.  RR+ )
83 fvex 5891 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( C `
 ( A `  n ) )  e. 
_V
8483rabex 4575 . . . . . . . . . . . . . . . . . . . . 21  |-  { i  e.  ( C `  ( A `  n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) ) }  e.  _V
8584a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  n  e.  NN )  ->  { i  e.  ( C `  ( A `  n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) ) }  e.  _V )
8669, 73, 82, 85fvmptd 5970 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) )  =  { i  e.  ( C `  ( A `
 n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) ) } )
87 ssrab2 3546 . . . . . . . . . . . . . . . . . . . 20  |-  { i  e.  ( C `  ( A `  n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) ) }  C_  ( C `  ( A `  n ) )
8887a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  n  e.  NN )  ->  { i  e.  ( C `  ( A `  n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) ) }  C_  ( C `  ( A `  n ) ) )
8986, 88eqsstrd 3498 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( D `  ( A `
 n ) ) `
 ( E  / 
( 2 ^ n
) ) )  C_  ( C `  ( A `
 n ) ) )
90 ovnsubaddlem1.i . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  n  e.  NN )  ->  ( I `
 n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) )
9189, 90sseldd 3465 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( I `
 n )  e.  ( C `  ( A `  n )
) )
9254, 91sseldd 3465 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  NN )  ->  ( I `
 n )  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN ) )
93 elmapfn 7505 . . . . . . . . . . . . . . . 16  |-  ( ( I `  n )  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  ->  ( I `
 n )  Fn  NN )
9492, 93syl 17 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  ( I `
 n )  Fn  NN )
95 elmapi 7504 . . . . . . . . . . . . . . . . . 18  |-  ( ( I `  n )  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  ->  ( I `
 n ) : NN --> ( ( RR 
X.  RR )  ^m  X ) )
9692, 95syl 17 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  NN )  ->  ( I `
 n ) : NN --> ( ( RR 
X.  RR )  ^m  X ) )
9796ffvelrnda 6037 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  j  e.  NN )  ->  (
( I `  n
) `  j )  e.  ( ( RR  X.  RR )  ^m  X ) )
9897ralrimiva 2836 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  A. j  e.  NN  ( ( I `
 n ) `  j )  e.  ( ( RR  X.  RR )  ^m  X ) )
9994, 98jca 534 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( I `  n )  Fn  NN  /\  A. j  e.  NN  (
( I `  n
) `  j )  e.  ( ( RR  X.  RR )  ^m  X ) ) )
100993adant3 1025 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  NN  /\  j  e.  NN )  ->  ( ( I `
 n )  Fn  NN  /\  A. j  e.  NN  ( ( I `
 n ) `  j )  e.  ( ( RR  X.  RR )  ^m  X ) ) )
101 ffnfv 6064 . . . . . . . . . . . . 13  |-  ( ( I `  n ) : NN --> ( ( RR  X.  RR )  ^m  X )  <->  ( (
I `  n )  Fn  NN  /\  A. j  e.  NN  ( ( I `
 n ) `  j )  e.  ( ( RR  X.  RR )  ^m  X ) ) )
102100, 101sylibr 215 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN  /\  j  e.  NN )  ->  ( I `  n ) : NN --> ( ( RR  X.  RR )  ^m  X ) )
103 simp3 1007 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN  /\  j  e.  NN )  ->  j  e.  NN )
104102, 103ffvelrnd 6038 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN  /\  j  e.  NN )  ->  ( ( I `
 n ) `  j )  e.  ( ( RR  X.  RR )  ^m  X ) )
105 elmapi 7504 . . . . . . . . . . 11  |-  ( ( ( I `  n
) `  j )  e.  ( ( RR  X.  RR )  ^m  X )  ->  ( ( I `
 n ) `  j ) : X --> ( RR  X.  RR ) )
106104, 105syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN  /\  j  e.  NN )  ->  ( ( I `
 n ) `  j ) : X --> ( RR  X.  RR ) )
10736, 42, 106vtocl 3133 . . . . . . . . 9  |-  ( (
ph  /\  ( 1st `  ( F `  m
) )  e.  NN  /\  j  e.  NN )  ->  ( ( I `
 ( 1st `  ( F `  m )
) ) `  j
) : X --> ( RR 
X.  RR ) )
10830, 35, 107vtocl 3133 . . . . . . . 8  |-  ( (
ph  /\  ( 1st `  ( F `  m
) )  e.  NN  /\  ( 2nd `  ( F `  m )
)  e.  NN )  ->  ( ( I `
 ( 1st `  ( F `  m )
) ) `  ( 2nd `  ( F `  m ) ) ) : X --> ( RR 
X.  RR ) )
10917, 27, 29, 108syl3anc 1264 . . . . . . 7  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( I `  ( 1st `  ( F `  m
) ) ) `  ( 2nd `  ( F `
 m ) ) ) : X --> ( RR 
X.  RR ) )
110 id 22 . . . . . . . . . 10  |-  ( m  e.  NN  ->  m  e.  NN )
111 fvex 5891 . . . . . . . . . . 11  |-  ( ( I `  ( 1st `  ( F `  m
) ) ) `  ( 2nd `  ( F `
 m ) ) )  e.  _V
112111a1i 11 . . . . . . . . . 10  |-  ( m  e.  NN  ->  (
( I `  ( 1st `  ( F `  m ) ) ) `
 ( 2nd `  ( F `  m )
) )  e.  _V )
113 ovnsubaddlem1.g . . . . . . . . . . 11  |-  G  =  ( m  e.  NN  |->  ( ( I `  ( 1st `  ( F `
 m ) ) ) `  ( 2nd `  ( F `  m
) ) ) )
114113fvmpt2 5973 . . . . . . . . . 10  |-  ( ( m  e.  NN  /\  ( ( I `  ( 1st `  ( F `
 m ) ) ) `  ( 2nd `  ( F `  m
) ) )  e. 
_V )  ->  ( G `  m )  =  ( ( I `
 ( 1st `  ( F `  m )
) ) `  ( 2nd `  ( F `  m ) ) ) )
115110, 112, 114syl2anc 665 . . . . . . . . 9  |-  ( m  e.  NN  ->  ( G `  m )  =  ( ( I `
 ( 1st `  ( F `  m )
) ) `  ( 2nd `  ( F `  m ) ) ) )
116115adantl 467 . . . . . . . 8  |-  ( (
ph  /\  m  e.  NN )  ->  ( G `
 m )  =  ( ( I `  ( 1st `  ( F `
 m ) ) ) `  ( 2nd `  ( F `  m
) ) ) )
117116feq1d 5732 . . . . . . 7  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( G `  m ) : X --> ( RR 
X.  RR )  <->  ( (
I `  ( 1st `  ( F `  m
) ) ) `  ( 2nd `  ( F `
 m ) ) ) : X --> ( RR 
X.  RR ) ) )
118109, 117mpbird 235 . . . . . 6  |-  ( (
ph  /\  m  e.  NN )  ->  ( G `
 m ) : X --> ( RR  X.  RR ) )
11916, 18, 19, 118hoiprodcl2 38281 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( L `
 ( G `  m ) )  e.  ( 0 [,) +oo ) )
12015, 119sseldi 3462 . . . 4  |-  ( (
ph  /\  m  e.  NN )  ->  ( L `
 ( G `  m ) )  e.  ( 0 [,] +oo ) )
12112, 14, 120sge0xrclmpt 38178 . . 3  |-  ( ph  ->  (Σ^ `  ( m  e.  NN  |->  ( L `  ( G `
 m ) ) ) )  e.  RR* )
122 nfv 1755 . . . 4  |-  F/ n ph
123 0xr 9694 . . . . . 6  |-  0  e.  RR*
124123a1i 11 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  0  e. 
RR* )
125 pnfxr 11419 . . . . . 6  |- +oo  e.  RR*
126125a1i 11 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  -> +oo  e.  RR* )
1271adantr 466 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  X  e. 
Fin )
128 ovnsubaddlem1.z . . . . . . . . 9  |-  Z  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  { z  e.  RR*  |  E. i  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN ) ( a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( i `  j
) ) `  k
)  /\  z  =  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) } )
129127, 7, 128ovnval2b 38278 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( (voln* `  X
) `  ( A `  n ) )  =  if ( X  =  (/) ,  0 , inf (
( Z `  ( A `  n )
) ,  RR* ,  <  ) ) )
130 ovnsubaddlem1.n0 . . . . . . . . . . 11  |-  ( ph  ->  X  =/=  (/) )
131130neneqd 2621 . . . . . . . . . 10  |-  ( ph  ->  -.  X  =  (/) )
132131iffalsed 3922 . . . . . . . . 9  |-  ( ph  ->  if ( X  =  (/) ,  0 , inf (
( Z `  ( A `  n )
) ,  RR* ,  <  ) )  = inf ( ( Z `  ( A `
 n ) ) ,  RR* ,  <  )
)
133132adantr 466 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  if ( X  =  (/) ,  0 , inf ( ( Z `
 ( A `  n ) ) , 
RR* ,  <  ) )  = inf ( ( Z `
 ( A `  n ) ) , 
RR* ,  <  ) )
134129, 133eqtrd 2463 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( (voln* `  X
) `  ( A `  n ) )  = inf ( ( Z `  ( A `  n ) ) ,  RR* ,  <  ) )
135128a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  Z  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  { z  e.  RR*  |  E. i  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN ) ( a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( i `  j
) ) `  k
)  /\  z  =  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) } ) )
136 sseq1 3485 . . . . . . . . . . . . . 14  |-  ( a  =  ( A `  n )  ->  (
a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( i `  j
) ) `  k
)  <->  ( A `  n )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( i `  j
) ) `  k
) ) )
137136anbi1d 709 . . . . . . . . . . . . 13  |-  ( a  =  ( A `  n )  ->  (
( a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( i `  j
) ) `  k
)  /\  z  =  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) )  <->  ( ( A `  n )  C_ 
U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  (
i `  j )
) `  k )  /\  z  =  (Σ^ `  (
j  e.  NN  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) ) )
138137rexbidv 2936 . . . . . . . . . . . 12  |-  ( a  =  ( A `  n )  ->  ( E. i  e.  (
( ( RR  X.  RR )  ^m  X )  ^m  NN ) ( a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( i `  j
) ) `  k
)  /\  z  =  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) )  <->  E. i  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN ) ( ( A `
 n )  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
i `  j )
) `  k )  /\  z  =  (Σ^ `  (
j  e.  NN  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) ) )
139138rabbidv 3071 . . . . . . . . . . 11  |-  ( a  =  ( A `  n )  ->  { z  e.  RR*  |  E. i  e.  ( (
( RR  X.  RR )  ^m  X )  ^m  NN ) ( a  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
i `  j )
) `  k )  /\  z  =  (Σ^ `  (
j  e.  NN  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) }  =  { z  e. 
RR*  |  E. i  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN ) ( ( A `
 n )  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
i `  j )
) `  k )  /\  z  =  (Σ^ `  (
j  e.  NN  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) } )
140139adantl 467 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  a  =  ( A `  n ) )  ->  { z  e.  RR*  |  E. i  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN ) ( a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( i `  j
) ) `  k
)  /\  z  =  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) }  =  { z  e. 
RR*  |  E. i  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN ) ( ( A `
 n )  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
i `  j )
) `  k )  /\  z  =  (Σ^ `  (
j  e.  NN  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) } )
141 xrex 11306 . . . . . . . . . . . 12  |-  RR*  e.  _V
142141rabex 4575 . . . . . . . . . . 11  |-  { z  e.  RR*  |  E. i  e.  ( (
( RR  X.  RR )  ^m  X )  ^m  NN ) ( ( A `
 n )  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
i `  j )
) `  k )  /\  z  =  (Σ^ `  (
j  e.  NN  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) }  e.  _V
143142a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  { z  e.  RR*  |  E. i  e.  ( (
( RR  X.  RR )  ^m  X )  ^m  NN ) ( ( A `
 n )  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
i `  j )
) `  k )  /\  z  =  (Σ^ `  (
j  e.  NN  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) }  e.  _V )
144135, 140, 5, 143fvmptd 5970 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( Z `
 ( A `  n ) )  =  { z  e.  RR*  |  E. i  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN ) ( ( A `  n
)  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( i `  j
) ) `  k
)  /\  z  =  (Σ^ `  ( j  e.  NN  |->  prod_ k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) } )
145 ssrab2 3546 . . . . . . . . . 10  |-  { z  e.  RR*  |  E. i  e.  ( (
( RR  X.  RR )  ^m  X )  ^m  NN ) ( ( A `
 n )  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
i `  j )
) `  k )  /\  z  =  (Σ^ `  (
j  e.  NN  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) } 
C_  RR*
146145a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  { z  e.  RR*  |  E. i  e.  ( (
( RR  X.  RR )  ^m  X )  ^m  NN ) ( ( A `
 n )  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
i `  j )
) `  k )  /\  z  =  (Σ^ `  (
j  e.  NN  |->  prod_
k  e.  X  ( vol `  ( ( [,)  o.  ( i `
 j ) ) `
 k ) ) ) ) ) } 
C_  RR* )
147144, 146eqsstrd 3498 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( Z `
 ( A `  n ) )  C_  RR* )
148 infxrcl 11626 . . . . . . . 8  |-  ( ( Z `  ( A `
 n ) ) 
C_  RR*  -> inf ( ( Z `  ( A `  n ) ) , 
RR* ,  <  )  e. 
RR* )
149147, 148syl 17 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  -> inf ( ( Z `  ( A `
 n ) ) ,  RR* ,  <  )  e.  RR* )
150134, 149eqeltrd 2507 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( (voln* `  X
) `  ( A `  n ) )  e. 
RR* )
15174rpred 11348 . . . . . . . . 9  |-  ( ph  ->  E  e.  RR )
152151adantr 466 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  E  e.  RR )
153 2re 10686 . . . . . . . . . . 11  |-  2  e.  RR
154153a1i 11 . . . . . . . . . 10  |-  ( n  e.  NN  ->  2  e.  RR )
155154, 78reexpcld 12439 . . . . . . . . 9  |-  ( n  e.  NN  ->  (
2 ^ n )  e.  RR )
156155adantl 467 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2 ^ n )  e.  RR )
157154recnd 9676 . . . . . . . . . 10  |-  ( n  e.  NN  ->  2  e.  CC )
158 2ne0 10709 . . . . . . . . . . 11  |-  2  =/=  0
159158a1i 11 . . . . . . . . . 10  |-  ( n  e.  NN  ->  2  =/=  0 )
160 nnz 10966 . . . . . . . . . 10  |-  ( n  e.  NN  ->  n  e.  ZZ )
161157, 159, 160expne0d 12428 . . . . . . . . 9  |-  ( n  e.  NN  ->  (
2 ^ n )  =/=  0 )
162161adantl 467 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( 2 ^ n )  =/=  0 )
163152, 156, 162redivcld 10442 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( E  /  ( 2 ^ n ) )  e.  RR )
164163rexrd 9697 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( E  /  ( 2 ^ n ) )  e. 
RR* )
165150, 164xaddcld 11594 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) )  e.  RR* )
166127, 7ovncl 38293 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( (voln* `  X
) `  ( A `  n ) )  e.  ( 0 [,] +oo ) )
167 xrge0ge0 37524 . . . . . . 7  |-  ( ( (voln* `  X ) `  ( A `  n )
)  e.  ( 0 [,] +oo )  -> 
0  <_  ( (voln* `  X
) `  ( A `  n ) ) )
168166, 167syl 17 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( (voln* `  X ) `  ( A `  n )
) )
169 0red 9651 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  0  e.  RR )
17082rpgt0d 11351 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  0  < 
( E  /  (
2 ^ n ) ) )
171169, 163, 170ltled 9790 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( E  /  (
2 ^ n ) ) )
172163ltpnfd 11430 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( E  /  ( 2 ^ n ) )  < +oo )
173164, 126, 172xrltled 37438 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( E  /  ( 2 ^ n ) )  <_ +oo )
174124, 126, 164, 171, 173eliccxrd 37577 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( E  /  ( 2 ^ n ) )  e.  ( 0 [,] +oo ) )
175150, 174xadd0ge 37496 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( (voln* `  X
) `  ( A `  n ) )  <_ 
( ( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) ) )
176124, 150, 165, 168, 175xrletrd 11466 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  0  <_ 
( ( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) ) )
177 pnfge 11439 . . . . . 6  |-  ( ( ( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) )  e.  RR*  ->  ( ( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) )  <_ +oo )
178165, 177syl 17 . . . . 5  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) )  <_ +oo )
179124, 126, 165, 176, 178eliccxrd 37577 . . . 4  |-  ( (
ph  /\  n  e.  NN )  ->  ( ( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) )  e.  ( 0 [,] +oo ) )
180122, 14, 179sge0xrclmpt 38178 . . 3  |-  ( ph  ->  (Σ^ `  ( n  e.  NN  |->  ( ( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) ) ) )  e. 
RR* )
18143a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  C  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  { h  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  |  a  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) } ) )
182 sseq1 3485 . . . . . . . . . . . . . 14  |-  ( a  =  ( A `  ( 1st `  ( F `
 m ) ) )  ->  ( a  C_ 
U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  (
h `  j )
) `  k )  <->  ( A `  ( 1st `  ( F `  m
) ) )  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
h `  j )
) `  k )
) )
183182rabbidv 3071 . . . . . . . . . . . . 13  |-  ( a  =  ( A `  ( 1st `  ( F `
 m ) ) )  ->  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  a  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
h `  j )
) `  k ) }  =  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  ( A `  ( 1st `  ( F `  m )
) )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) } )
184183adantl 467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  m  e.  NN )  /\  a  =  ( A `  ( 1st `  ( F `
 m ) ) ) )  ->  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  a  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
h `  j )
) `  k ) }  =  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  ( A `  ( 1st `  ( F `  m )
) )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) } )
1852adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  NN )  ->  A : NN
--> ~P ( RR  ^m  X ) )
186185, 27ffvelrnd 6038 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  ( A `
 ( 1st `  ( F `  m )
) )  e.  ~P ( RR  ^m  X ) )
18748rabex 4575 . . . . . . . . . . . . 13  |-  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  ( A `  ( 1st `  ( F `  m )
) )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) }  e.  _V
188187a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  ( A `  ( 1st `  ( F `  m )
) )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) }  e.  _V )
189181, 184, 186, 188fvmptd 5970 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  ( C `
 ( A `  ( 1st `  ( F `
 m ) ) ) )  =  {
h  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  |  ( A `  ( 1st `  ( F `  m
) ) )  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
h `  j )
) `  k ) } )
190 ssrab2 3546 . . . . . . . . . . . 12  |-  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  ( A `  ( 1st `  ( F `  m )
) )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) }  C_  (
( ( RR  X.  RR )  ^m  X )  ^m  NN )
191190a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  ( A `  ( 1st `  ( F `  m )
) )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) }  C_  (
( ( RR  X.  RR )  ^m  X )  ^m  NN ) )
192189, 191eqsstrd 3498 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  ( C `
 ( A `  ( 1st `  ( F `
 m ) ) ) )  C_  (
( ( RR  X.  RR )  ^m  X )  ^m  NN ) )
19355a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  NN )  ->  D  =  ( a  e.  ~P ( RR  ^m  X ) 
|->  ( e  e.  RR+  |->  { i  e.  ( C `  a )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) } ) ) )
194 fveq2 5881 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  ( A `  ( 1st `  ( F `
 m ) ) )  ->  ( C `  a )  =  ( C `  ( A `
 ( 1st `  ( F `  m )
) ) ) )
195194eleq2d 2492 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( A `  ( 1st `  ( F `
 m ) ) )  ->  ( i  e.  ( C `  a
)  <->  i  e.  ( C `  ( A `
 ( 1st `  ( F `  m )
) ) ) ) )
196 fveq2 5881 . . . . . . . . . . . . . . . . . . . 20  |-  ( a  =  ( A `  ( 1st `  ( F `
 m ) ) )  ->  ( (voln* `  X
) `  a )  =  ( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) )
197196oveq1d 6320 . . . . . . . . . . . . . . . . . . 19  |-  ( a  =  ( A `  ( 1st `  ( F `
 m ) ) )  ->  ( (
(voln* `  X ) `  a
) +e e )  =  ( ( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e e ) )
198197breq2d 4435 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  ( A `  ( 1st `  ( F `
 m ) ) )  ->  ( (Σ^ `  (
j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e )  <->  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e e ) ) )
199195, 198anbi12d 715 . . . . . . . . . . . . . . . . 17  |-  ( a  =  ( A `  ( 1st `  ( F `
 m ) ) )  ->  ( (
i  e.  ( C `
 a )  /\  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) )  <->  ( i  e.  ( C `  ( A `  ( 1st `  ( F `  m
) ) ) )  /\  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e e ) ) ) )
200199rabbidva2 3069 . . . . . . . . . . . . . . . 16  |-  ( a  =  ( A `  ( 1st `  ( F `
 m ) ) )  ->  { i  e.  ( C `  a
)  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) }  =  {
i  e.  ( C `
 ( A `  ( 1st `  ( F `
 m ) ) ) )  |  (Σ^ `  (
j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e e ) } )
201200mpteq2dv 4511 . . . . . . . . . . . . . . 15  |-  ( a  =  ( A `  ( 1st `  ( F `
 m ) ) )  ->  ( e  e.  RR+  |->  { i  e.  ( C `  a
)  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) } )  =  ( e  e.  RR+  |->  { i  e.  ( C `  ( A `
 ( 1st `  ( F `  m )
) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e e ) } ) )
202201adantl 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  m  e.  NN )  /\  a  =  ( A `  ( 1st `  ( F `
 m ) ) ) )  ->  (
e  e.  RR+  |->  { i  e.  ( C `  a )  |  (Σ^ `  (
j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  a
) +e e ) } )  =  ( e  e.  RR+  |->  { i  e.  ( C `  ( A `
 ( 1st `  ( F `  m )
) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e e ) } ) )
20366mptex 6151 . . . . . . . . . . . . . . 15  |-  ( e  e.  RR+  |->  { i  e.  ( C `  ( A `  ( 1st `  ( F `  m
) ) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e e ) } )  e.  _V
204203a1i 11 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  NN )  ->  ( e  e.  RR+  |->  { i  e.  ( C `  ( A `  ( 1st `  ( F `  m
) ) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e e ) } )  e.  _V )
205193, 202, 186, 204fvmptd 5970 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  NN )  ->  ( D `
 ( A `  ( 1st `  ( F `
 m ) ) ) )  =  ( e  e.  RR+  |->  { i  e.  ( C `  ( A `  ( 1st `  ( F `  m
) ) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e e ) } ) )
206 oveq2 6313 . . . . . . . . . . . . . . . 16  |-  ( e  =  ( E  / 
( 2 ^ ( 1st `  ( F `  m ) ) ) )  ->  ( (
(voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e e )  =  ( ( (voln* `  X
) `  ( A `  ( 1st `  ( F `  m )
) ) ) +e ( E  / 
( 2 ^ ( 1st `  ( F `  m ) ) ) ) ) )
207206breq2d 4435 . . . . . . . . . . . . . . 15  |-  ( e  =  ( E  / 
( 2 ^ ( 1st `  ( F `  m ) ) ) )  ->  ( (Σ^ `  (
j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e e )  <-> 
(Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e ( E  /  ( 2 ^ ( 1st `  ( F `  m )
) ) ) ) ) )
208207rabbidv 3071 . . . . . . . . . . . . . 14  |-  ( e  =  ( E  / 
( 2 ^ ( 1st `  ( F `  m ) ) ) )  ->  { i  e.  ( C `  ( A `  ( 1st `  ( F `  m
) ) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e e ) }  =  { i  e.  ( C `  ( A `  ( 1st `  ( F `  m
) ) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e ( E  /  ( 2 ^ ( 1st `  ( F `  m )
) ) ) ) } )
209208adantl 467 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  m  e.  NN )  /\  e  =  ( E  / 
( 2 ^ ( 1st `  ( F `  m ) ) ) ) )  ->  { i  e.  ( C `  ( A `  ( 1st `  ( F `  m
) ) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e e ) }  =  { i  e.  ( C `  ( A `  ( 1st `  ( F `  m
) ) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e ( E  /  ( 2 ^ ( 1st `  ( F `  m )
) ) ) ) } )
21017, 74syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  NN )  ->  E  e.  RR+ )
211 2rp 11314 . . . . . . . . . . . . . . . 16  |-  2  e.  RR+
212211a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  NN )  ->  2  e.  RR+ )
21327nnzd 11046 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  m  e.  NN )  ->  ( 1st `  ( F `  m
) )  e.  ZZ )
214212, 213rpexpcld 12445 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  m  e.  NN )  ->  ( 2 ^ ( 1st `  ( F `  m )
) )  e.  RR+ )
215210, 214rpdivcld 11365 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  NN )  ->  ( E  /  ( 2 ^ ( 1st `  ( F `  m )
) ) )  e.  RR+ )
216 fvex 5891 . . . . . . . . . . . . . . 15  |-  ( C `
 ( A `  ( 1st `  ( F `
 m ) ) ) )  e.  _V
217216rabex 4575 . . . . . . . . . . . . . 14  |-  { i  e.  ( C `  ( A `  ( 1st `  ( F `  m
) ) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e ( E  /  ( 2 ^ ( 1st `  ( F `  m )
) ) ) ) }  e.  _V
218217a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  m  e.  NN )  ->  { i  e.  ( C `  ( A `  ( 1st `  ( F `  m
) ) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e ( E  /  ( 2 ^ ( 1st `  ( F `  m )
) ) ) ) }  e.  _V )
219205, 209, 215, 218fvmptd 5970 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( D `  ( A `
 ( 1st `  ( F `  m )
) ) ) `  ( E  /  (
2 ^ ( 1st `  ( F `  m
) ) ) ) )  =  { i  e.  ( C `  ( A `  ( 1st `  ( F `  m
) ) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e ( E  /  ( 2 ^ ( 1st `  ( F `  m )
) ) ) ) } )
220 ssrab2 3546 . . . . . . . . . . . . 13  |-  { i  e.  ( C `  ( A `  ( 1st `  ( F `  m
) ) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e ( E  /  ( 2 ^ ( 1st `  ( F `  m )
) ) ) ) }  C_  ( C `  ( A `  ( 1st `  ( F `  m ) ) ) )
221220a1i 11 . . . . . . . . . . . 12  |-  ( (
ph  /\  m  e.  NN )  ->  { i  e.  ( C `  ( A `  ( 1st `  ( F `  m
) ) ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  ( 1st `  ( F `  m
) ) ) ) +e ( E  /  ( 2 ^ ( 1st `  ( F `  m )
) ) ) ) }  C_  ( C `  ( A `  ( 1st `  ( F `  m ) ) ) ) )
222219, 221eqsstrd 3498 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( D `  ( A `
 ( 1st `  ( F `  m )
) ) ) `  ( E  /  (
2 ^ ( 1st `  ( F `  m
) ) ) ) )  C_  ( C `  ( A `  ( 1st `  ( F `  m ) ) ) ) )
22337anbi2d 708 . . . . . . . . . . . . . 14  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( ( ph  /\  n  e.  NN ) 
<->  ( ph  /\  ( 1st `  ( F `  m ) )  e.  NN ) ) )
224 fveq2 5881 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( A `  n )  =  ( A `  ( 1st `  ( F `  m
) ) ) )
225224fveq2d 5885 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( D `  ( A `  n
) )  =  ( D `  ( A `
 ( 1st `  ( F `  m )
) ) ) )
226 oveq2 6313 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( 2 ^ n )  =  ( 2 ^ ( 1st `  ( F `  m ) ) ) )
227226oveq2d 6321 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( E  /  ( 2 ^ n ) )  =  ( E  /  (
2 ^ ( 1st `  ( F `  m
) ) ) ) )
228225, 227fveq12d 5887 . . . . . . . . . . . . . . 15  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( ( D `  ( A `  n ) ) `  ( E  /  (
2 ^ n ) ) )  =  ( ( D `  ( A `  ( 1st `  ( F `  m
) ) ) ) `
 ( E  / 
( 2 ^ ( 1st `  ( F `  m ) ) ) ) ) )
22939, 228eleq12d 2501 . . . . . . . . . . . . . 14  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( (
I `  n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) )  <-> 
( I `  ( 1st `  ( F `  m ) ) )  e.  ( ( D `
 ( A `  ( 1st `  ( F `
 m ) ) ) ) `  ( E  /  ( 2 ^ ( 1st `  ( F `  m )
) ) ) ) ) )
230223, 229imbi12d 321 . . . . . . . . . . . . 13  |-  ( n  =  ( 1st `  ( F `  m )
)  ->  ( (
( ph  /\  n  e.  NN )  ->  (
I `  n )  e.  ( ( D `  ( A `  n ) ) `  ( E  /  ( 2 ^ n ) ) ) )  <->  ( ( ph  /\  ( 1st `  ( F `  m )
)  e.  NN )  ->  ( I `  ( 1st `  ( F `
 m ) ) )  e.  ( ( D `  ( A `
 ( 1st `  ( F `  m )
) ) ) `  ( E  /  (
2 ^ ( 1st `  ( F `  m
) ) ) ) ) ) ) )
23136, 230, 90vtocl 3133 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( 1st `  ( F `  m
) )  e.  NN )  ->  ( I `  ( 1st `  ( F `
 m ) ) )  e.  ( ( D `  ( A `
 ( 1st `  ( F `  m )
) ) ) `  ( E  /  (
2 ^ ( 1st `  ( F `  m
) ) ) ) ) )
23217, 27, 231syl2anc 665 . . . . . . . . . . 11  |-  ( (
ph  /\  m  e.  NN )  ->  ( I `
 ( 1st `  ( F `  m )
) )  e.  ( ( D `  ( A `  ( 1st `  ( F `  m
) ) ) ) `
 ( E  / 
( 2 ^ ( 1st `  ( F `  m ) ) ) ) ) )
233222, 232sseldd 3465 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  ( I `
 ( 1st `  ( F `  m )
) )  e.  ( C `  ( A `
 ( 1st `  ( F `  m )
) ) ) )
234192, 233sseldd 3465 . . . . . . . . 9  |-  ( (
ph  /\  m  e.  NN )  ->  ( I `
 ( 1st `  ( F `  m )
) )  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN ) )
235 elmapfn 7505 . . . . . . . . 9  |-  ( ( I `  ( 1st `  ( F `  m
) ) )  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  ->  ( I `  ( 1st `  ( F `
 m ) ) )  Fn  NN )
236234, 235syl 17 . . . . . . . 8  |-  ( (
ph  /\  m  e.  NN )  ->  ( I `
 ( 1st `  ( F `  m )
) )  Fn  NN )
237 elmapi 7504 . . . . . . . . . . 11  |-  ( ( I `  ( 1st `  ( F `  m
) ) )  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  ->  ( I `  ( 1st `  ( F `
 m ) ) ) : NN --> ( ( RR  X.  RR )  ^m  X ) )
238234, 237syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  m  e.  NN )  ->  ( I `
 ( 1st `  ( F `  m )
) ) : NN --> ( ( RR  X.  RR )  ^m  X ) )
239238ffvelrnda 6037 . . . . . . . . 9  |-  ( ( ( ph  /\  m  e.  NN )  /\  j  e.  NN )  ->  (
( I `  ( 1st `  ( F `  m ) ) ) `
 j )  e.  ( ( RR  X.  RR )  ^m  X ) )
240239ralrimiva 2836 . . . . . . . 8  |-  ( (
ph  /\  m  e.  NN )  ->  A. j  e.  NN  ( ( I `
 ( 1st `  ( F `  m )
) ) `  j
)  e.  ( ( RR  X.  RR )  ^m  X ) )
241236, 240jca 534 . . . . . . 7  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( I `  ( 1st `  ( F `  m
) ) )  Fn  NN  /\  A. j  e.  NN  ( ( I `
 ( 1st `  ( F `  m )
) ) `  j
)  e.  ( ( RR  X.  RR )  ^m  X ) ) )
242 ffnfv 6064 . . . . . . 7  |-  ( ( I `  ( 1st `  ( F `  m
) ) ) : NN --> ( ( RR 
X.  RR )  ^m  X )  <->  ( (
I `  ( 1st `  ( F `  m
) ) )  Fn  NN  /\  A. j  e.  NN  ( ( I `
 ( 1st `  ( F `  m )
) ) `  j
)  e.  ( ( RR  X.  RR )  ^m  X ) ) )
243241, 242sylibr 215 . . . . . 6  |-  ( (
ph  /\  m  e.  NN )  ->  ( I `
 ( 1st `  ( F `  m )
) ) : NN --> ( ( RR  X.  RR )  ^m  X ) )
244243, 29ffvelrnd 6038 . . . . 5  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( I `  ( 1st `  ( F `  m
) ) ) `  ( 2nd `  ( F `
 m ) ) )  e.  ( ( RR  X.  RR )  ^m  X ) )
245244, 113fmptd 6061 . . . 4  |-  ( ph  ->  G : NN --> ( ( RR  X.  RR )  ^m  X ) )
246 simpl 458 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ph )
24790, 86eleqtrd 2509 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN )  ->  ( I `
 n )  e. 
{ i  e.  ( C `  ( A `
 n ) )  |  (Σ^ `  ( j  e.  NN  |->  ( L `  ( i `
 j ) ) ) )  <_  (
( (voln* `  X ) `  ( A `  n )
) +e ( E  /  ( 2 ^ n ) ) ) } )
24887, 247sseldi 3462 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  ( I `
 n )  e.  ( C `  ( A `  n )
) )
249 simp3 1007 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN  /\  ( I `  n )  e.  ( C `  ( A `
 n ) ) )  ->  ( I `  n )  e.  ( C `  ( A `
 n ) ) )
250513adant3 1025 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  NN  /\  ( I `  n )  e.  ( C `  ( A `
 n ) ) )  ->  ( C `  ( A `  n
) )  =  {
h  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  |  ( A `  n )  C_ 
U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  (
h `  j )
) `  k ) } )
251249, 250eleqtrd 2509 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  NN  /\  ( I `  n )  e.  ( C `  ( A `
 n ) ) )  ->  ( I `  n )  e.  {
h  e.  ( ( ( RR  X.  RR )  ^m  X )  ^m  NN )  |  ( A `  n )  C_ 
U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  (
h `  j )
) `  k ) } )
252 fveq1 5880 . . . . . . . . . . . . . . . . 17  |-  ( h  =  ( I `  n )  ->  (
h `  j )  =  ( ( I `
 n ) `  j ) )
253252coeq2d 5016 . . . . . . . . . . . . . . . 16  |-  ( h  =  ( I `  n )  ->  ( [,)  o.  ( h `  j ) )  =  ( [,)  o.  (
( I `  n
) `  j )
) )
254253fveq1d 5883 . . . . . . . . . . . . . . 15  |-  ( h  =  ( I `  n )  ->  (
( [,)  o.  (
h `  j )
) `  k )  =  ( ( [,) 
o.  ( ( I `
 n ) `  j ) ) `  k ) )
255254ixpeq2dv 7549 . . . . . . . . . . . . . 14  |-  ( h  =  ( I `  n )  ->  X_ k  e.  X  ( ( [,)  o.  ( h `  j ) ) `  k )  =  X_ k  e.  X  (
( [,)  o.  (
( I `  n
) `  j )
) `  k )
)
256255iuneq2d 4326 . . . . . . . . . . . . 13  |-  ( h  =  ( I `  n )  ->  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
)  =  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( ( I `  n ) `  j
) ) `  k
) )
257256sseq2d 3492 . . . . . . . . . . . 12  |-  ( h  =  ( I `  n )  ->  (
( A `  n
)  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
)  <->  ( A `  n )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( ( I `  n ) `  j
) ) `  k
) ) )
258257elrab 3228 . . . . . . . . . . 11  |-  ( ( I `  n )  e.  { h  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  |  ( A `  n )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( h `  j
) ) `  k
) }  <->  ( (
I `  n )  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  /\  ( A `  n )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( ( I `  n ) `  j
) ) `  k
) ) )
259251, 258sylib 199 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  NN  /\  ( I `  n )  e.  ( C `  ( A `
 n ) ) )  ->  ( (
I `  n )  e.  ( ( ( RR 
X.  RR )  ^m  X )  ^m  NN )  /\  ( A `  n )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( ( I `  n ) `  j
) ) `  k
) ) )
260259simprd 464 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN  /\  ( I `  n )  e.  ( C `  ( A `
 n ) ) )  ->  ( A `  n )  C_  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( ( I `  n ) `  j
) ) `  k
) )
261246, 4, 248, 260syl3anc 1264 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( A `
 n )  C_  U_ j  e.  NN  X_ k  e.  X  (
( [,)  o.  (
( I `  n
) `  j )
) `  k )
)
262 f1ofo 5838 . . . . . . . . . . . . . 14  |-  ( F : NN -1-1-onto-> ( NN  X.  NN )  ->  F : NN -onto->
( NN  X.  NN ) )
26320, 262syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  F : NN -onto-> ( NN  X.  NN ) )
264263ad2antrr 730 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  j  e.  NN )  ->  F : NN -onto-> ( NN  X.  NN ) )
265 opelxpi 4885 . . . . . . . . . . . . 13  |-  ( ( n  e.  NN  /\  j  e.  NN )  -> 
<. n ,  j >.  e.  ( NN  X.  NN ) )
2664, 265sylan 473 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  j  e.  NN )  ->  <. n ,  j >.  e.  ( NN  X.  NN ) )
267 foelrni 5929 . . . . . . . . . . . 12  |-  ( ( F : NN -onto-> ( NN  X.  NN )  /\  <.
n ,  j >.  e.  ( NN  X.  NN ) )  ->  E. m  e.  NN  ( F `  m )  =  <. n ,  j >. )
268264, 266, 267syl2anc 665 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  j  e.  NN )  ->  E. m  e.  NN  ( F `  m )  =  <. n ,  j >. )
269 nfv 1755 . . . . . . . . . . . 12  |-  F/ m
( ( ph  /\  n  e.  NN )  /\  j  e.  NN )
270 nfre1 2883 . . . . . . . . . . . 12  |-  F/ m E. m  e.  { i  e.  NN  |  ( 1st `  ( F `
 i ) )  =  n } X_ k  e.  X  (
( [,)  o.  (
( I `  n
) `  j )
) `  k )  C_  X_ k  e.  X  ( ( [,)  o.  ( G `  m ) ) `  k )
271 simpl 458 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  NN  /\  ( F `  m )  =  <. n ,  j
>. )  ->  m  e.  NN )
272 fveq2 5881 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  m )  =  <. n ,  j
>.  ->  ( 1st `  ( F `  m )
)  =  ( 1st `  <. n ,  j
>. ) )
273 vex 3083 . . . . . . . . . . . . . . . . . . . . 21  |-  n  e. 
_V
274 vex 3083 . . . . . . . . . . . . . . . . . . . . 21  |-  j  e. 
_V
275 op1stg 6819 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  _V  /\  j  e.  _V )  ->  ( 1st `  <. n ,  j >. )  =  n )
276273, 274, 275mp2an 676 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1st `  <. n ,  j
>. )  =  n
277276a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( F `  m )  =  <. n ,  j
>.  ->  ( 1st `  <. n ,  j >. )  =  n )
278272, 277eqtrd 2463 . . . . . . . . . . . . . . . . . 18  |-  ( ( F `  m )  =  <. n ,  j
>.  ->  ( 1st `  ( F `  m )
)  =  n )
279278adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  NN  /\  ( F `  m )  =  <. n ,  j
>. )  ->  ( 1st `  ( F `  m
) )  =  n )
280271, 279jca 534 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  NN  /\  ( F `  m )  =  <. n ,  j
>. )  ->  ( m  e.  NN  /\  ( 1st `  ( F `  m ) )  =  n ) )
281 fveq2 5881 . . . . . . . . . . . . . . . . . . 19  |-  ( i  =  m  ->  ( F `  i )  =  ( F `  m ) )
282281fveq2d 5885 . . . . . . . . . . . . . . . . . 18  |-  ( i  =  m  ->  ( 1st `  ( F `  i ) )  =  ( 1st `  ( F `  m )
) )
283282eqeq1d 2424 . . . . . . . . . . . . . . . . 17  |-  ( i  =  m  ->  (
( 1st `  ( F `  i )
)  =  n  <->  ( 1st `  ( F `  m
) )  =  n ) )
284283elrab 3228 . . . . . . . . . . . . . . . 16  |-  ( m  e.  { i  e.  NN  |  ( 1st `  ( F `  i
) )  =  n }  <->  ( m  e.  NN  /\  ( 1st `  ( F `  m
) )  =  n ) )
285280, 284sylibr 215 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  NN  /\  ( F `  m )  =  <. n ,  j
>. )  ->  m  e. 
{ i  e.  NN  |  ( 1st `  ( F `  i )
)  =  n }
)
2862853adant1 1023 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  j  e.  NN )  /\  m  e.  NN  /\  ( F `  m
)  =  <. n ,  j >. )  ->  m  e.  { i  e.  NN  |  ( 1st `  ( F `
 i ) )  =  n } )
287271, 115syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( m  e.  NN  /\  ( F `  m )  =  <. n ,  j
>. )  ->  ( G `
 m )  =  ( ( I `  ( 1st `  ( F `
 m ) ) ) `  ( 2nd `  ( F `  m
) ) ) )
288278fveq2d 5885 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  m )  =  <. n ,  j
>.  ->  ( I `  ( 1st `  ( F `
 m ) ) )  =  ( I `
 n ) )
289273, 274op2ndd 6818 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( F `  m )  =  <. n ,  j
>.  ->  ( 2nd `  ( F `  m )
)  =  j )
290288, 289fveq12d 5887 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( F `  m )  =  <. n ,  j
>.  ->  ( ( I `
 ( 1st `  ( F `  m )
) ) `  ( 2nd `  ( F `  m ) ) )  =  ( ( I `
 n ) `  j ) )
291290adantl 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( m  e.  NN  /\  ( F `  m )  =  <. n ,  j
>. )  ->  ( ( I `  ( 1st `  ( F `  m
) ) ) `  ( 2nd `  ( F `
 m ) ) )  =  ( ( I `  n ) `
 j ) )
292287, 291eqtr2d 2464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( m  e.  NN  /\  ( F `  m )  =  <. n ,  j
>. )  ->  ( ( I `  n ) `
 j )  =  ( G `  m
) )
293292coeq2d 5016 . . . . . . . . . . . . . . . . . 18  |-  ( ( m  e.  NN  /\  ( F `  m )  =  <. n ,  j
>. )  ->  ( [,) 
o.  ( ( I `
 n ) `  j ) )  =  ( [,)  o.  ( G `  m )
) )
294293fveq1d 5883 . . . . . . . . . . . . . . . . 17  |-  ( ( m  e.  NN  /\  ( F `  m )  =  <. n ,  j
>. )  ->  ( ( [,)  o.  ( ( I `  n ) `
 j ) ) `
 k )  =  ( ( [,)  o.  ( G `  m ) ) `  k ) )
295294ixpeq2dv 7549 . . . . . . . . . . . . . . . 16  |-  ( ( m  e.  NN  /\  ( F `  m )  =  <. n ,  j
>. )  ->  X_ k  e.  X  ( ( [,)  o.  ( ( I `
 n ) `  j ) ) `  k )  =  X_ k  e.  X  (
( [,)  o.  ( G `  m )
) `  k )
)
296 eqimss 3516 . . . . . . . . . . . . . . . 16  |-  ( X_ k  e.  X  (
( [,)  o.  (
( I `  n
) `  j )
) `  k )  =  X_ k  e.  X  ( ( [,)  o.  ( G `  m ) ) `  k )  ->  X_ k  e.  X  ( ( [,)  o.  ( ( I `  n ) `  j
) ) `  k
)  C_  X_ k  e.  X  ( ( [,) 
o.  ( G `  m ) ) `  k ) )
297295, 296syl 17 . . . . . . . . . . . . . . 15  |-  ( ( m  e.  NN  /\  ( F `  m )  =  <. n ,  j
>. )  ->  X_ k  e.  X  ( ( [,)  o.  ( ( I `
 n ) `  j ) ) `  k )  C_  X_ k  e.  X  ( ( [,)  o.  ( G `  m ) ) `  k ) )
2982973adant1 1023 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  j  e.  NN )  /\  m  e.  NN  /\  ( F `  m
)  =  <. n ,  j >. )  -> 
X_ k  e.  X  ( ( [,)  o.  ( ( I `  n ) `  j
) ) `  k
)  C_  X_ k  e.  X  ( ( [,) 
o.  ( G `  m ) ) `  k ) )
299 rspe 2880 . . . . . . . . . . . . . 14  |-  ( ( m  e.  { i  e.  NN  |  ( 1st `  ( F `
 i ) )  =  n }  /\  X_ k  e.  X  ( ( [,)  o.  (
( I `  n
) `  j )
) `  k )  C_  X_ k  e.  X  ( ( [,)  o.  ( G `  m ) ) `  k ) )  ->  E. m  e.  { i  e.  NN  |  ( 1st `  ( F `  i )
)  =  n } X_ k  e.  X  ( ( [,)  o.  (
( I `  n
) `  j )
) `  k )  C_  X_ k  e.  X  ( ( [,)  o.  ( G `  m ) ) `  k ) )
300286, 298, 299syl2anc 665 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  j  e.  NN )  /\  m  e.  NN  /\  ( F `  m
)  =  <. n ,  j >. )  ->  E. m  e.  {
i  e.  NN  | 
( 1st `  ( F `  i )
)  =  n } X_ k  e.  X  ( ( [,)  o.  (
( I `  n
) `  j )
) `  k )  C_  X_ k  e.  X  ( ( [,)  o.  ( G `  m ) ) `  k ) )
3013003exp 1204 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  j  e.  NN )  ->  (
m  e.  NN  ->  ( ( F `  m
)  =  <. n ,  j >.  ->  E. m  e.  { i  e.  NN  |  ( 1st `  ( F `  i )
)  =  n } X_ k  e.  X  ( ( [,)  o.  (
( I `  n
) `  j )
) `  k )  C_  X_ k  e.  X  ( ( [,)  o.  ( G `  m ) ) `  k ) ) ) )
302269, 270, 301rexlimd 2906 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  j  e.  NN )  ->  ( E. m  e.  NN  ( F `  m )  =  <. n ,  j
>.  ->  E. m  e.  {
i  e.  NN  | 
( 1st `  ( F `  i )
)  =  n } X_ k  e.  X  ( ( [,)  o.  (
( I `  n
) `  j )
) `  k )  C_  X_ k  e.  X  ( ( [,)  o.  ( G `  m ) ) `  k ) ) )
303268, 302mpd 15 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  j  e.  NN )  ->  E. m  e.  { i  e.  NN  |  ( 1st `  ( F `  i )
)  =  n } X_ k  e.  X  ( ( [,)  o.  (
( I `  n
) `  j )
) `  k )  C_  X_ k  e.  X  ( ( [,)  o.  ( G `  m ) ) `  k ) )
304303ralrimiva 2836 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  NN )  ->  A. j  e.  NN  E. m  e. 
{ i  e.  NN  |  ( 1st `  ( F `  i )
)  =  n } X_ k  e.  X  ( ( [,)  o.  (
( I `  n
) `  j )
) `  k )  C_  X_ k  e.  X  ( ( [,)  o.  ( G `  m ) ) `  k ) )
305 iunss2 4344 . . . . . . . . 9  |-  ( A. j  e.  NN  E. m  e.  { i  e.  NN  |  ( 1st `  ( F `  i )
)  =  n } X_ k  e.  X  ( ( [,)  o.  (
( I `  n
) `  j )
) `  k )  C_  X_ k  e.  X  ( ( [,)  o.  ( G `  m ) ) `  k )  ->  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  (
( I `  n
) `  j )
) `  k )  C_ 
U_ m  e.  {
i  e.  NN  | 
( 1st `  ( F `  i )
)  =  n } X_ k  e.  X  ( ( [,)  o.  ( G `  m )
) `  k )
)
306304, 305syl 17 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  U_ j  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( ( I `  n ) `  j
) ) `  k
)  C_  U_ m  e. 
{ i  e.  NN  |  ( 1st `  ( F `  i )
)  =  n } X_ k  e.  X  ( ( [,)  o.  ( G `  m )
) `  k )
)
307261, 306sstrd 3474 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ( A `
 n )  C_  U_ m  e.  { i  e.  NN  |  ( 1st `  ( F `
 i ) )  =  n } X_ k  e.  X  (
( [,)  o.  ( G `  m )
) `  k )
)
308 ssrab2 3546 . . . . . . . . 9  |-  { i  e.  NN  |  ( 1st `  ( F `
 i ) )  =  n }  C_  NN
309 iunss1 4311 . . . . . . . . 9  |-  ( { i  e.  NN  | 
( 1st `  ( F `  i )
)  =  n }  C_  NN  ->  U_ m  e. 
{ i  e.  NN  |  ( 1st `  ( F `  i )
)  =  n } X_ k  e.  X  ( ( [,)  o.  ( G `  m )
) `  k )  C_ 
U_ m  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( G `  m )
) `  k )
)
310308, 309ax-mp 5 . . . . . . . 8  |-  U_ m  e.  { i  e.  NN  |  ( 1st `  ( F `  i )
)  =  n } X_ k  e.  X  ( ( [,)  o.  ( G `  m )
) `  k )  C_ 
U_ m  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( G `  m )
) `  k )
311310a1i 11 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  U_ m  e.  { i  e.  NN  |  ( 1st `  ( F `  i )
)  =  n } X_ k  e.  X  ( ( [,)  o.  ( G `  m )
) `  k )  C_ 
U_ m  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( G `  m )
) `  k )
)
312307, 311sstrd 3474 . . . . . 6  |-  ( (
ph  /\  n  e.  NN )  ->  ( A `
 n )  C_  U_ m  e.  NN  X_ k  e.  X  (
( [,)  o.  ( G `  m )
) `  k )
)
313312ralrimiva 2836 . . . . 5  |-  ( ph  ->  A. n  e.  NN  ( A `  n ) 
C_  U_ m  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( G `  m )
) `  k )
)
314 iunss 4340 . . . . 5  |-  ( U_ n  e.  NN  ( A `  n )  C_ 
U_ m  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( G `  m )
) `  k )  <->  A. n  e.  NN  ( A `  n )  C_ 
U_ m  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( G `  m )
) `  k )
)
315313, 314sylibr 215 . . . 4  |-  ( ph  ->  U_ n  e.  NN  ( A `  n ) 
C_  U_ m  e.  NN  X_ k  e.  X  ( ( [,)  o.  ( G `  m )
) `  k )
)
3161, 130, 19, 245, 315ovnlecvr 38284 . . 3  |-  ( ph  ->  ( (voln* `  X ) `  U_ n  e.  NN  ( A `  n ) )  <_ 
(Σ^ `  ( m  e.  NN  |->  ( L `  ( G `
 m ) ) ) ) )
317116fveq2d 5885 . . . . . . 7  |-  ( (
ph  /\  m  e.  NN )  ->  ( L `
 ( G `  m ) )  =  ( L `  (
( I `  ( 1st `  ( F `  m ) ) ) `
 ( 2nd `  (