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

Theorem stoweidlem59 27911
Description: This lemma proves that there exists a function  x as in the proof in [BrosowskiDeutsh] p. 91, after Lemma 2: xj is in the subalgebra, 0 <= xj <= 1, xj < ε / n on Aj (meaning A in the paper), xj > 1 - \epslon / n on Bj. Here  D is used to represent A in the paper (because A is used for the subalgebra of functions),  E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem59.1  |-  F/_ t F
stoweidlem59.2  |-  F/ t
ph
stoweidlem59.3  |-  K  =  ( topGen `  ran  (,) )
stoweidlem59.4  |-  T  = 
U. J
stoweidlem59.5  |-  C  =  ( J  Cn  K
)
stoweidlem59.6  |-  D  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
stoweidlem59.7  |-  B  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
stoweidlem59.8  |-  Y  =  { y  e.  A  |  A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 ) }
stoweidlem59.9  |-  H  =  ( j  e.  ( 0 ... N ) 
|->  { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) } )
stoweidlem59.10  |-  ( ph  ->  J  e.  Comp )
stoweidlem59.11  |-  ( ph  ->  A  C_  C )
stoweidlem59.12  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  +  ( g `  t ) ) )  e.  A )
stoweidlem59.13  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  x.  ( g `  t ) ) )  e.  A )
stoweidlem59.14  |-  ( (
ph  /\  y  e.  RR )  ->  ( t  e.  T  |->  y )  e.  A )
stoweidlem59.15  |-  ( (
ph  /\  ( r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
stoweidlem59.16  |-  ( ph  ->  F  e.  C )
stoweidlem59.17  |-  ( ph  ->  E  e.  RR+ )
stoweidlem59.18  |-  ( ph  ->  E  <  ( 1  /  3 ) )
stoweidlem59.19  |-  ( ph  ->  N  e.  NN )
Assertion
Ref Expression
stoweidlem59  |-  ( ph  ->  E. x ( x : ( 0 ... N ) --> A  /\  A. j  e.  ( 0 ... N ) ( A. t  e.  T  ( 0  <_  (
( x `  j
) `  t )  /\  ( ( x `  j ) `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( ( x `
 j ) `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( ( x `
 j ) `  t ) ) ) )
Distinct variable groups:    t, j,
y    y, B    y, D    j, N, t, y    j, Y    f, g, j, q, r, t, N    x, f, g, j, t, N   
y, f, q, r, A    A, g, q, r, t    B, f, g, q, r    D, f, g, q, r    f, E, g, r, t    f, J, g, r, t    T, f, g, q, r, t    ph, f, g, j, q, r    x, y, A   
x, B    x, D    x, E, y    x, T, y    ph, y    t, K   
x, H    x, Y    ph, x
Allowed substitution hints:    ph( t)    A( j)    B( t, j)    C( x, y, t, f, g, j, r, q)    D( t, j)    T( j)    E( j, q)    F( x, y, t, f, g, j, r, q)    H( y, t, f, g, j, r, q)    J( x, y, j, q)    K( x, y, f, g, j, r, q)    Y( y, t, f, g, r, q)

Proof of Theorem stoweidlem59
Dummy variables  a  w  h  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem59.8 . . . . . . . . . . . 12  |-  Y  =  { y  e.  A  |  A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 ) }
2 nfrab1 2733 . . . . . . . . . . . 12  |-  F/_ y { y  e.  A  |  A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 ) }
31, 2nfcxfr 2429 . . . . . . . . . . 11  |-  F/_ y Y
4 nfcv 2432 . . . . . . . . . . 11  |-  F/_ z Y
5 nfv 1609 . . . . . . . . . . 11  |-  F/ z ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) )
6 nfv 1609 . . . . . . . . . . 11  |-  F/ y ( A. t  e.  ( D `  j
) ( z `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( z `  t ) )
7 fveq1 5540 . . . . . . . . . . . . . 14  |-  ( y  =  z  ->  (
y `  t )  =  ( z `  t ) )
87breq1d 4049 . . . . . . . . . . . . 13  |-  ( y  =  z  ->  (
( y `  t
)  <  ( E  /  N )  <->  ( z `  t )  <  ( E  /  N ) ) )
98ralbidv 2576 . . . . . . . . . . . 12  |-  ( y  =  z  ->  ( A. t  e.  ( D `  j )
( y `  t
)  <  ( E  /  N )  <->  A. t  e.  ( D `  j
) ( z `  t )  <  ( E  /  N ) ) )
107breq2d 4051 . . . . . . . . . . . . 13  |-  ( y  =  z  ->  (
( 1  -  ( E  /  N ) )  <  ( y `  t )  <->  ( 1  -  ( E  /  N ) )  < 
( z `  t
) ) )
1110ralbidv 2576 . . . . . . . . . . . 12  |-  ( y  =  z  ->  ( A. t  e.  ( B `  j )
( 1  -  ( E  /  N ) )  <  ( y `  t )  <->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
z `  t )
) )
129, 11anbi12d 691 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) )  <->  ( A. t  e.  ( D `  j ) ( z `
 t )  < 
( E  /  N
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
z `  t )
) ) )
133, 4, 5, 6, 12cbvrab 2799 . . . . . . . . . 10  |-  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) }  =  { z  e.  Y  |  ( A. t  e.  ( D `  j
) ( z `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( z `  t ) ) }
14 ssrab2 3271 . . . . . . . . . . . . . . 15  |-  { y  e.  A  |  A. t  e.  T  (
0  <_  ( y `  t )  /\  (
y `  t )  <_  1 ) }  C_  A
151, 14eqsstri 3221 . . . . . . . . . . . . . 14  |-  Y  C_  A
1615a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  Y  C_  A )
17 stoweidlem59.11 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A  C_  C )
18 stoweidlem59.5 . . . . . . . . . . . . . . . 16  |-  C  =  ( J  Cn  K
)
1917, 18syl6sseq 3237 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A  C_  ( J  Cn  K ) )
20 stoweidlem59.10 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  J  e.  Comp )
21 cmptop 17138 . . . . . . . . . . . . . . . . . 18  |-  ( J  e.  Comp  ->  J  e. 
Top )
2220, 21syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  J  e.  Top )
23 stoweidlem59.3 . . . . . . . . . . . . . . . . . . 19  |-  K  =  ( topGen `  ran  (,) )
24 retop 18286 . . . . . . . . . . . . . . . . . . 19  |-  ( topGen ` 
ran  (,) )  e.  Top
2523, 24eqeltri 2366 . . . . . . . . . . . . . . . . . 18  |-  K  e. 
Top
2625a1i 10 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  K  e.  Top )
2722, 26jca 518 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( J  e.  Top  /\  K  e.  Top )
)
28 cnfex 27802 . . . . . . . . . . . . . . . 16  |-  ( ( J  e.  Top  /\  K  e.  Top )  ->  ( J  Cn  K
)  e.  _V )
2927, 28syl 15 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( J  Cn  K
)  e.  _V )
3019, 29jca 518 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A  C_  ( J  Cn  K )  /\  ( J  Cn  K
)  e.  _V )
)
31 ssexg 4176 . . . . . . . . . . . . . 14  |-  ( ( A  C_  ( J  Cn  K )  /\  ( J  Cn  K )  e. 
_V )  ->  A  e.  _V )
3230, 31syl 15 . . . . . . . . . . . . 13  |-  ( ph  ->  A  e.  _V )
3316, 32jca 518 . . . . . . . . . . . 12  |-  ( ph  ->  ( Y  C_  A  /\  A  e.  _V ) )
34 ssexg 4176 . . . . . . . . . . . 12  |-  ( ( Y  C_  A  /\  A  e.  _V )  ->  Y  e.  _V )
3533, 34syl 15 . . . . . . . . . . 11  |-  ( ph  ->  Y  e.  _V )
36 rabexg 4180 . . . . . . . . . . 11  |-  ( Y  e.  _V  ->  { z  e.  Y  |  ( A. t  e.  ( D `  j ) ( z `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( z `  t
) ) }  e.  _V )
3735, 36syl 15 . . . . . . . . . 10  |-  ( ph  ->  { z  e.  Y  |  ( A. t  e.  ( D `  j
) ( z `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( z `  t ) ) }  e.  _V )
3813, 37syl5eqel 2380 . . . . . . . . 9  |-  ( ph  ->  { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }  e.  _V )
3938adantr 451 . . . . . . . 8  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) }  e.  _V )
4039ralrimiva 2639 . . . . . . 7  |-  ( ph  ->  A. j  e.  ( 0 ... N ) { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }  e.  _V )
41 stoweidlem59.9 . . . . . . . 8  |-  H  =  ( j  e.  ( 0 ... N ) 
|->  { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) } )
4241fnmpt 5386 . . . . . . 7  |-  ( A. j  e.  ( 0 ... N ) { y  e.  Y  | 
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }  e.  _V  ->  H  Fn  ( 0 ... N
) )
4340, 42syl 15 . . . . . 6  |-  ( ph  ->  H  Fn  ( 0 ... N ) )
4443idi 2 . . . . 5  |-  ( ph  ->  H  Fn  ( 0 ... N ) )
45 fzfi 11050 . . . . . 6  |-  ( 0 ... N )  e. 
Fin
46 fnfi 7150 . . . . . 6  |-  ( ( H  Fn  ( 0 ... N )  /\  ( 0 ... N
)  e.  Fin )  ->  H  e.  Fin )
4745, 46mpan2 652 . . . . 5  |-  ( H  Fn  ( 0 ... N )  ->  H  e.  Fin )
4844, 47syl 15 . . . 4  |-  ( ph  ->  H  e.  Fin )
49 rnfi 7157 . . . 4  |-  ( H  e.  Fin  ->  ran  H  e.  Fin )
5048, 49syl 15 . . 3  |-  ( ph  ->  ran  H  e.  Fin )
51 fnchoice 27803 . . 3  |-  ( ran 
H  e.  Fin  ->  E. h ( h  Fn 
ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  ( h `  w )  e.  w
) ) )
5250, 51syl 15 . 2  |-  ( ph  ->  E. h ( h  Fn  ran  H  /\  A. w  e.  ran  H
( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )
53 simprl 732 . . . . . . . . 9  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  h  Fn  ran  H )
54 ovex 5899 . . . . . . . . . . . . 13  |-  ( 0 ... N )  e. 
_V
55 mptexg 5761 . . . . . . . . . . . . 13  |-  ( ( 0 ... N )  e.  _V  ->  (
j  e.  ( 0 ... N )  |->  { y  e.  Y  | 
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) } )  e.  _V )
5654, 55ax-mp 8 . . . . . . . . . . . 12  |-  ( j  e.  ( 0 ... N )  |->  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) } )  e.  _V
5741, 56eqeltri 2366 . . . . . . . . . . 11  |-  H  e. 
_V
5857rnex 4958 . . . . . . . . . 10  |-  ran  H  e.  _V
5958a1i 10 . . . . . . . . 9  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ran  H  e.  _V )
6053, 59jca 518 . . . . . . . 8  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( h  Fn 
ran  H  /\  ran  H  e.  _V ) )
61 fnex 5757 . . . . . . . 8  |-  ( ( h  Fn  ran  H  /\  ran  H  e.  _V )  ->  h  e.  _V )
6260, 61syl 15 . . . . . . 7  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  h  e.  _V )
6357a1i 10 . . . . . . 7  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  H  e.  _V )
6462, 63jca 518 . . . . . 6  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( h  e. 
_V  /\  H  e.  _V ) )
65 coexg 5231 . . . . . 6  |-  ( ( h  e.  _V  /\  H  e.  _V )  ->  ( h  o.  H
)  e.  _V )
6664, 65syl 15 . . . . 5  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( h  o.  H )  e.  _V )
67 dffn3 5412 . . . . . . . . . . 11  |-  ( h  Fn  ran  H  <->  h : ran  H --> ran  h )
6853, 67sylib 188 . . . . . . . . . 10  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  h : ran  H --> ran  h )
69 nfv 1609 . . . . . . . . . . . . . . . 16  |-  F/ w ph
70 nfv 1609 . . . . . . . . . . . . . . . . 17  |-  F/ w  h  Fn  ran  H
71 nfra1 2606 . . . . . . . . . . . . . . . . 17  |-  F/ w A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )
7270, 71nfan 1783 . . . . . . . . . . . . . . . 16  |-  F/ w
( h  Fn  ran  H  /\  A. w  e. 
ran  H ( w  =/=  (/)  ->  ( h `  w )  e.  w
) )
7369, 72nfan 1783 . . . . . . . . . . . . . . 15  |-  F/ w
( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )
74 simplrr 737 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  w  e.  ran  H )  ->  A. w  e.  ran  H ( w  =/=  (/)  ->  ( h `  w )  e.  w
) )
75 simpr 447 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  w  e.  ran  H )  ->  w  e.  ran  H )
7674, 75jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  w  e.  ran  H )  ->  ( A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )  /\  w  e.  ran  H ) )
77 simpll 730 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  w  e.  ran  H )  ->  ph )
7877, 75jca 518 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  w  e.  ran  H )  ->  ( ph  /\  w  e.  ran  H
) )
79 fvelrnb 5586 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( H  Fn  ( 0 ... N )  ->  (
w  e.  ran  H  <->  E. a  e.  ( 0 ... N ) ( H `  a )  =  w ) )
80 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ a ( H `  j
)  =  w
81 nfmpt1 4125 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ j
( j  e.  ( 0 ... N ) 
|->  { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) } )
8241, 81nfcxfr 2429 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ j H
83 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ j
a
8482, 83nffv 5548 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ j
( H `  a
)
85 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ j
w
8684, 85nfeq 2439 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ j ( H `  a
)  =  w
87 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  a  ->  ( H `  j )  =  ( H `  a ) )
8887eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  a  ->  (
( H `  j
)  =  w  <->  ( H `  a )  =  w ) )
8980, 86, 88cbvrex 2774 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. j  e.  ( 0 ... N ) ( H `  j )  =  w  <->  E. a  e.  ( 0 ... N
) ( H `  a )  =  w )
9079, 89syl6bbr 254 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( H  Fn  ( 0 ... N )  ->  (
w  e.  ran  H  <->  E. j  e.  ( 0 ... N ) ( H `  j )  =  w ) )
9143, 90syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( w  e.  ran  H  <->  E. j  e.  (
0 ... N ) ( H `  j )  =  w ) )
9291biimpa 470 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  w  e.  ran  H )  ->  E. j  e.  ( 0 ... N
) ( H `  j )  =  w )
93 stoweidlem59.6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  D  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
94 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  F/_ t
( 0 ... N
)
95 nfrab1 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  F/_ t { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) }
9694, 95nfmpt 4124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  F/_ t
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
9793, 96nfcxfr 2429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/_ t D
98 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/_ t
j
9997, 98nffv 5548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  F/_ t
( D `  j
)
100 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/_ t T
101 stoweidlem59.7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  B  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
102 nfrab1 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  F/_ t { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) }
10394, 102nfmpt 4124 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  F/_ t
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
104101, 103nfcxfr 2429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  F/_ t B
105104, 98nffv 5548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/_ t
( B `  j
)
106100, 105nfdif 3310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  F/_ t
( T  \  ( B `  j )
)
107 stoweidlem59.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/ t
ph
108 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  F/ t  j  e.  ( 0 ... N )
109107, 108nfan 1783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  F/ t ( ph  /\  j  e.  ( 0 ... N
) )
110 stoweidlem59.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  T  = 
U. J
11120adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  J  e.  Comp )
11217adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  A  C_  C )
113 simp1l 979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  f  e.  A  /\  g  e.  A )  ->  ph )
114 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  f  e.  A  /\  g  e.  A )  ->  f  e.  A )
115 simp3 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  f  e.  A  /\  g  e.  A )  ->  g  e.  A )
116113, 114, 1153jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  f  e.  A  /\  g  e.  A )  ->  ( ph  /\  f  e.  A  /\  g  e.  A
) )
117 stoweidlem59.12 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  +  ( g `  t ) ) )  e.  A )
118116, 117syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  f  e.  A  /\  g  e.  A )  ->  (
t  e.  T  |->  ( ( f `  t
)  +  ( g `
 t ) ) )  e.  A )
119 stoweidlem59.13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  x.  ( g `  t ) ) )  e.  A )
120116, 119syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  f  e.  A  /\  g  e.  A )  ->  (
t  e.  T  |->  ( ( f `  t
)  x.  ( g `
 t ) ) )  e.  A )
121 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  RR )  ->  ph )
122 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  RR )  ->  y  e.  RR )
123121, 122jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  RR )  ->  ( ph  /\  y  e.  RR ) )
124 stoweidlem59.14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  y  e.  RR )  ->  ( t  e.  T  |->  y )  e.  A )
125123, 124syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  RR )  ->  (
t  e.  T  |->  y )  e.  A )
126 simpll 730 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  ph )
127 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  ( r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )
128126, 127jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  ( ph  /\  ( r  e.  T  /\  t  e.  T  /\  r  =/=  t
) ) )
129 stoweidlem59.15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
130128, 129syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
131 stoweidlem59.1 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  F/_ t F
132 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  =  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) }
133 elfzelz 10814 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( j  e.  ( 0 ... N )  ->  j  e.  ZZ )
134 zre 10044 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( j  e.  ZZ  ->  j  e.  RR )
135133, 134syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( j  e.  ( 0 ... N )  ->  j  e.  RR )
136 1re 8853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  1  e.  RR
137 3re 9833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  3  e.  RR
138 3ne0 9847 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  3  =/=  0
139136, 137, 1383pm3.2i 1130 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( 1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )
140 redivcl 9495 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( 1  e.  RR  /\  3  e.  RR  /\  3  =/=  0 )  ->  (
1  /  3 )  e.  RR )
141139, 140ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( 1  /  3 )  e.  RR
142141a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( j  e.  ( 0 ... N )  ->  (
1  /  3 )  e.  RR )
143135, 142jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  ( 0 ... N )  ->  (
j  e.  RR  /\  ( 1  /  3
)  e.  RR ) )
144 readdcl 8836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( j  e.  RR  /\  ( 1  /  3
)  e.  RR )  ->  ( j  +  ( 1  /  3
) )  e.  RR )
145143, 144syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  ( 1  /  3 ) )  e.  RR )
146145adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
j  +  ( 1  /  3 ) )  e.  RR )
147 stoweidlem59.17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  E  e.  RR+ )
148 rpre 10376 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( E  e.  RR+  ->  E  e.  RR )
149147, 148syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  E  e.  RR )
150149adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  E  e.  RR )
151146, 150jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  +  ( 1  /  3 ) )  e.  RR  /\  E  e.  RR )
)
152 remulcl 8838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( j  +  ( 1  /  3 ) )  e.  RR  /\  E  e.  RR )  ->  ( ( j  +  ( 1  /  3
) )  x.  E
)  e.  RR )
153151, 152syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  +  ( 1  /  3 ) )  x.  E )  e.  RR )
154 stoweidlem59.16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  F  e.  C )
155154, 18syl6eleq 2386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  F  e.  ( J  Cn  K ) )
156155adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  F  e.  ( J  Cn  K
) )
157131, 23, 110, 132, 153, 156rfcnpre3 27807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  e.  ( Clsd `  J )
)
158 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  j  e.  ( 0 ... N
) )
159 uniexg 4533 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( J  e.  Comp  ->  U. J  e.  _V )
16020, 159syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  U. J  e.  _V )
161110eleq1i 2359 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( T  e.  _V  <->  U. J  e. 
_V )
162161biimpri 197 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( U. J  e.  _V  ->  T  e.  _V )
163160, 162syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  T  e.  _V )
164163adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  T  e.  _V )
165 rabexg 4180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( T  e.  _V  ->  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  e.  _V )
166164, 165syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  e.  _V )
167158, 166jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
j  e.  ( 0 ... N )  /\  { t  e.  T  | 
( ( j  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t ) }  e.  _V ) )
168101fvmpt2 5624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( j  e.  ( 0 ... N )  /\  { t  e.  T  | 
( ( j  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t ) }  e.  _V )  ->  ( B `
 j )  =  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
169167, 168syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( B `  j )  =  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
170169eleq1d 2362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( B `  j
)  e.  ( Clsd `  J )  <->  { t  e.  T  |  (
( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  e.  ( Clsd `  J )
) )
171157, 170mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( B `  j )  e.  ( Clsd `  J
) )
172 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) }
173 resubcl 9127 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( j  e.  RR  /\  ( 1  /  3
)  e.  RR )  ->  ( j  -  ( 1  /  3
) )  e.  RR )
174143, 173syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( j  e.  ( 0 ... N )  ->  (
j  -  ( 1  /  3 ) )  e.  RR )
175174adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
j  -  ( 1  /  3 ) )  e.  RR )
176175, 150jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  -  (
1  /  3 ) )  e.  RR  /\  E  e.  RR )
)
177 remulcl 8838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( j  -  (
1  /  3 ) )  e.  RR  /\  E  e.  RR )  ->  ( ( j  -  ( 1  /  3
) )  x.  E
)  e.  RR )
178176, 177syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  e.  RR )
179155idi 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  F  e.  ( J  Cn  K ) )
180179adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  F  e.  ( J  Cn  K
) )
181131, 23, 110, 172, 178, 180rfcnpre4 27808 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  e.  ( Clsd `  J )
)
182 rabexg 4180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
183164, 182syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
184158, 183jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
j  e.  ( 0 ... N )  /\  { t  e.  T  | 
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E ) }  e.  _V ) )
18593fvmpt2 5624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( j  e.  ( 0 ... N )  /\  { t  e.  T  | 
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E ) }  e.  _V )  -> 
( D `  j
)  =  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) } )
186184, 185syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( D `  j )  =  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
187186eleq1d 2362 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( D `  j
)  e.  ( Clsd `  J )  <->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  /  3
) )  x.  E
) }  e.  (
Clsd `  J )
) )
188181, 187mpbird 223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( D `  j )  e.  ( Clsd `  J
) )
189178adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  e.  RR )
190153adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  +  ( 1  /  3 ) )  x.  E )  e.  RR )
19123, 110, 18, 154fcnre 27799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ph  ->  F : T --> RR )
192191ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  F : T --> RR )
193 ssrab2 3271 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  C_  T
194193a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  C_  T )
195169, 194eqsstrd 3225 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( B `  j )  C_  T )
196 ssel 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( B `  j ) 
C_  T  ->  (
t  e.  ( B `
 j )  -> 
t  e.  T ) )
197195, 196syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
t  e.  ( B `
 j )  -> 
t  e.  T ) )
198197imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  t  e.  T )
199192, 198jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  ( F : T --> RR  /\  t  e.  T )
)
200 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( F : T --> RR  /\  t  e.  T )  ->  ( F `  t
)  e.  RR )
201199, 200syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  ( F `  t )  e.  RR )
202189, 190, 2013jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( ( j  -  ( 1  /  3
) )  x.  E
)  e.  RR  /\  ( ( j  +  ( 1  /  3
) )  x.  E
)  e.  RR  /\  ( F `  t )  e.  RR ) )
203141a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( j  e.  RR  ->  (
1  /  3 )  e.  RR )
204203ancli 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( j  e.  RR  ->  (
j  e.  RR  /\  ( 1  /  3
)  e.  RR ) )
205204, 173syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( j  e.  RR  ->  (
j  -  ( 1  /  3 ) )  e.  RR )
206 id 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( j  e.  RR  ->  j  e.  RR )
207204, 144syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( j  e.  RR  ->  (
j  +  ( 1  /  3 ) )  e.  RR )
208205, 206, 2073jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( j  e.  RR  ->  (
( j  -  (
1  /  3 ) )  e.  RR  /\  j  e.  RR  /\  (
j  +  ( 1  /  3 ) )  e.  RR ) )
209 0lt1 9312 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  0  <  1
210136, 209pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( 1  e.  RR  /\  0  <  1 )
211 3pos 9846 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53  |-  0  <  3
212137, 211pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52  |-  ( 3  e.  RR  /\  0  <  3 )
213210, 212pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( 1  e.  RR  /\  0  <  1 )  /\  ( 3  e.  RR  /\  0  <  3 ) )
214 divgt0 9640 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51  |-  ( ( ( 1  e.  RR  /\  0  <  1 )  /\  ( 3  e.  RR  /\  0  <  3 ) )  -> 
0  <  ( 1  /  3 ) )
215213, 214ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50  |-  0  <  ( 1  /  3
)
216141, 215pm3.2i 441 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( 1  /  3 )  e.  RR  /\  0  <  ( 1  /  3
) )
217 elrp 10372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 49  |-  ( ( 1  /  3 )  e.  RR+  <->  ( ( 1  /  3 )  e.  RR  /\  0  < 
( 1  /  3
) ) )
218216, 217mpbir 200 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 48  |-  ( 1  /  3 )  e.  RR+
219218a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47  |-  ( j  e.  RR  ->  (
1  /  3 )  e.  RR+ )
220219ancli 534 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( j  e.  RR  ->  (
j  e.  RR  /\  ( 1  /  3
)  e.  RR+ )
)
221 ltsubrp 10401 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( j  e.  RR  /\  ( 1  /  3
)  e.  RR+ )  ->  ( j  -  (
1  /  3 ) )  <  j )
222220, 221syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( j  e.  RR  ->  (
j  -  ( 1  /  3 ) )  <  j )
223 ltaddrp 10402 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( ( j  e.  RR  /\  ( 1  /  3
)  e.  RR+ )  ->  j  <  ( j  +  ( 1  / 
3 ) ) )
224220, 223syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( j  e.  RR  ->  j  <  ( j  +  ( 1  /  3 ) ) )
225222, 224jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( j  e.  RR  ->  (
( j  -  (
1  /  3 ) )  <  j  /\  j  <  ( j  +  ( 1  /  3
) ) ) )
226 lttr 8915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ( ( j  -  (
1  /  3 ) )  e.  RR  /\  j  e.  RR  /\  (
j  +  ( 1  /  3 ) )  e.  RR )  -> 
( ( ( j  -  ( 1  / 
3 ) )  < 
j  /\  j  <  ( j  +  ( 1  /  3 ) ) )  ->  ( j  -  ( 1  / 
3 ) )  < 
( j  +  ( 1  /  3 ) ) ) )
227208, 225, 226sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( j  e.  RR  ->  (
j  -  ( 1  /  3 ) )  <  ( j  +  ( 1  /  3
) ) )
228135, 227syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( j  e.  ( 0 ... N )  ->  (
j  -  ( 1  /  3 ) )  <  ( j  +  ( 1  /  3
) ) )
229228adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
j  -  ( 1  /  3 ) )  <  ( j  +  ( 1  /  3
) ) )
230 rpgt0 10381 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 46  |-  ( E  e.  RR+  ->  0  < 
E )
231147, 230syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 45  |-  ( ph  ->  0  <  E )
232149, 231jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ph  ->  ( E  e.  RR  /\  0  <  E ) )
233232adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( E  e.  RR  /\  0  <  E ) )
234175, 146, 2333jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  -  (
1  /  3 ) )  e.  RR  /\  ( j  +  ( 1  /  3 ) )  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) ) )
235 ltmul1 9622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( j  -  (
1  /  3 ) )  e.  RR  /\  ( j  +  ( 1  /  3 ) )  e.  RR  /\  ( E  e.  RR  /\  0  <  E ) )  ->  ( (
j  -  ( 1  /  3 ) )  <  ( j  +  ( 1  /  3
) )  <->  ( (
j  -  ( 1  /  3 ) )  x.  E )  < 
( ( j  +  ( 1  /  3
) )  x.  E
) ) )
236234, 235syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  -  (
1  /  3 ) )  <  ( j  +  ( 1  / 
3 ) )  <->  ( (
j  -  ( 1  /  3 ) )  x.  E )  < 
( ( j  +  ( 1  /  3
) )  x.  E
) ) )
237229, 236mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E ) )
238237adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E ) )
239169idi 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( B `  j )  =  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
240 eleq2 2357 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ( B `  j )  =  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_ 
( F `  t
) }  ->  (
t  e.  ( B `
 j )  <->  t  e.  { t  e.  T  | 
( ( j  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t ) } ) )
241239, 240syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
t  e.  ( B `
 j )  <->  t  e.  { t  e.  T  | 
( ( j  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t ) } ) )
242241biimpa 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  t  e.  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
243 rabid 2729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( t  e.  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_ 
( F `  t
) }  <->  ( t  e.  T  /\  (
( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) ) )
244242, 243sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
t  e.  T  /\  ( ( j  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t ) ) )
245244simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) )
246238, 245jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( ( j  -  ( 1  /  3
) )  x.  E
)  <  ( (
j  +  ( 1  /  3 ) )  x.  E )  /\  ( ( j  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t ) ) )
247 ltletr 8929 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( ( ( j  -  ( 1  /  3
) )  x.  E
)  e.  RR  /\  ( ( j  +  ( 1  /  3
) )  x.  E
)  e.  RR  /\  ( F `  t )  e.  RR )  -> 
( ( ( ( j  -  ( 1  /  3 ) )  x.  E )  < 
( ( j  +  ( 1  /  3
) )  x.  E
)  /\  ( (
j  +  ( 1  /  3 ) )  x.  E )  <_ 
( F `  t
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  <  ( F `  t ) ) )
248202, 246, 247sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  <  ( F `  t ) )
249189, 201ltnled 8982 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( ( j  -  ( 1  /  3
) )  x.  E
)  <  ( F `  t )  <->  -.  ( F `  t )  <_  ( ( j  -  ( 1  /  3
) )  x.  E
) ) )
250248, 249mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  -.  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) )
251250intnand 882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  -.  ( t  e.  T  /\  ( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E ) ) )
252 rabid 2729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( t  e.  { t  e.  T  |  ( F `
 t )  <_ 
( ( j  -  ( 1  /  3
) )  x.  E
) }  <->  ( t  e.  T  /\  ( F `  t )  <_  ( ( j  -  ( 1  /  3
) )  x.  E
) ) )
253251, 252sylnibr 296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  -.  t  e.  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  /  3
) )  x.  E
) } )
254186adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  ( D `  j )  =  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
255254eleq2d 2363 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
t  e.  ( D `
 j )  <->  t  e.  { t  e.  T  | 
( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E ) } ) )
256253, 255mtbird 292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  -.  t  e.  ( D `  j ) )
257256ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
t  e.  ( B `
 j )  ->  -.  t  e.  ( D `  j )
) )
258109, 257ralrimi 2637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  A. t  e.  ( B `  j
)  -.  t  e.  ( D `  j
) )
259 disj 3508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( B `  j
)  i^i  ( D `  j ) )  =  (/) 
<-> 
A. a  e.  ( B `  j )  -.  a  e.  ( D `  j ) )
260 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  F/_ a
( B `  j
)
261 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/_ t
a
262261, 99nfel 2440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  F/ t  a  e.  ( D `
 j )
263262nfn 1777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  F/ t  -.  a  e.  ( D `  j )
264 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  F/ a  -.  t  e.  ( D `  j )
265 eleq1 2356 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( a  =  t  ->  (
a  e.  ( D `
 j )  <->  t  e.  ( D `  j ) ) )
266265notbid 285 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( a  =  t  ->  ( -.  a  e.  ( D `  j )  <->  -.  t  e.  ( D `
 j ) ) )
267260, 105, 263, 264, 266cbvralf 2771 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( A. a  e.  ( B `  j )  -.  a  e.  ( D `  j
)  <->  A. t  e.  ( B `  j )  -.  t  e.  ( D `  j ) )
268259, 267bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( B `  j
)  i^i  ( D `  j ) )  =  (/) 
<-> 
A. t  e.  ( B `  j )  -.  t  e.  ( D `  j ) )
269258, 268sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( B `  j
)  i^i  ( D `  j ) )  =  (/) )
270 eqid 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( T 
\  ( B `  j ) )  =  ( T  \  ( B `  j )
)
271 stoweidlem59.19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  N  e.  NN )
272271nnrpd 10405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  N  e.  RR+ )
273147, 272rpdivcld 10423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( E  /  N
)  e.  RR+ )
274273adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( E  /  N )  e.  RR+ )
275271nnred 9777 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  N  e.  RR )
276271nnne0d 9806 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  N  =/=  0 )
277149, 275, 276redivcld 9604 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( E  /  N
)  e.  RR )
278141a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( 1  /  3
)  e.  RR )
279277, 149, 2783jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( ( E  /  N )  e.  RR  /\  E  e.  RR  /\  ( 1  /  3
)  e.  RR ) )
280271nnge1d 9804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  1  <_  N )
281210a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( 1  e.  RR  /\  0  <  1 ) )
282271nngt0d 9805 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ph  ->  0  <  N )
283275, 282jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ph  ->  ( N  e.  RR  /\  0  <  N ) )
284281, 283, 2323jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ph  ->  ( ( 1  e.  RR  /\  0  <  1 )  /\  ( N  e.  RR  /\  0  <  N )  /\  ( E  e.  RR  /\  0  <  E ) ) )
285 lediv2 9662 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( ( 1  e.  RR  /\  0  <  1 )  /\  ( N  e.  RR  /\  0  < 
N )  /\  ( E  e.  RR  /\  0  <  E ) )  -> 
( 1  <_  N  <->  ( E  /  N )  <_  ( E  / 
1 ) ) )
286284, 285syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( 1  <_  N  <->  ( E  /  N )  <_  ( E  / 
1 ) ) )
287280, 286mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( E  /  N
)  <_  ( E  /  1 ) )
288149recnd 8877 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  E  e.  CC )
289288div1d 9544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( E  /  1
)  =  E )
290287, 289breqtrd 4063 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( E  /  N
)  <_  E )
291 stoweidlem59.18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  E  <  ( 1  /  3 ) )
292290, 291jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( ( E  /  N )  <_  E  /\  E  <  ( 1  /  3 ) ) )
293 lelttr 8928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( E  /  N
)  e.  RR  /\  E  e.  RR  /\  (
1  /  3 )  e.  RR )  -> 
( ( ( E  /  N )  <_  E  /\  E  <  (
1  /  3 ) )  ->  ( E  /  N )  <  (
1  /  3 ) ) )
294279, 292, 293sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( E  /  N
)  <  ( 1  /  3 ) )
295294adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( E  /  N )  < 
( 1  /  3
) )
29699, 106, 109, 23, 110, 18, 111, 112, 118, 120, 125, 130, 171, 188, 269, 270, 274, 295stoweidlem58 27910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  E. x  e.  A  ( A. t  e.  T  (
0  <_  ( x `  t )  /\  (
x `  t )  <_  1 )  /\  A. t  e.  ( D `  j ) ( x `
 t )  < 
( E  /  N
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
x `  t )
) )
297 df-rex 2562 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( E. x  e.  A  ( A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) )  <->  E. x
( x  e.  A  /\  ( A. t  e.  T  ( 0  <_ 
( x `  t
)  /\  ( x `  t )  <_  1
)  /\  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) ) ) )
298296, 297sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  E. x
( x  e.  A  /\  ( A. t  e.  T  ( 0  <_ 
( x `  t
)  /\  ( x `  t )  <_  1
)  /\  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) ) ) )
299 simprl 732 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
x  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) ) ) )  ->  x  e.  A )
300 simprr1 1003 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
x  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) ) ) )  ->  A. t  e.  T  ( 0  <_  ( x `  t )  /\  (
x `  t )  <_  1 ) )
301299, 300jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
x  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) ) ) )  ->  ( x  e.  A  /\  A. t  e.  T  ( 0  <_  ( x `  t )  /\  (
x `  t )  <_  1 ) ) )
302 fveq1 5540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( y  =  x  ->  (
y `  t )  =  ( x `  t ) )
303302breq2d 4051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  =  x  ->  (
0  <_  ( y `  t )  <->  0  <_  ( x `  t ) ) )
304302breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( y  =  x  ->  (
( y `  t
)  <_  1  <->  ( x `  t )  <_  1
) )
305303, 304anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( y  =  x  ->  (
( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 )  <-> 
( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 ) ) )
306305ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  x  ->  ( A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 )  <->  A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 ) ) )
307306, 1elrab2 2938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( x  e.  Y  <->  ( x  e.  A  /\  A. t  e.  T  ( 0  <_  ( x `  t )  /\  (
x `  t )  <_  1 ) ) )
308301, 307sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
x  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) ) ) )  ->  x  e.  Y )
309 simprr2 1004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
x  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) ) ) )  ->  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N ) )
310 simprr3 1005 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
x  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) ) ) )  ->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
x `  t )
)
311309, 310jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
x  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) ) ) )  ->  ( A. t  e.  ( D `  j ) ( x `
 t )  < 
( E  /  N
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
x `  t )
) )
312308, 311jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
x  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) ) ) )  ->  ( x  e.  Y  /\  ( A. t  e.  ( D `  j )
( x `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( x `  t
) ) ) )
313 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  F/_ y
x
314 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  F/ y ( A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) )
315302breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  x  ->  (
( y `  t
)  <  ( E  /  N )  <->  ( x `  t )  <  ( E  /  N ) ) )
316315ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  x  ->  ( A. t  e.  ( D `  j )
( y `  t
)  <  ( E  /  N )  <->  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N ) ) )
317302breq2d 4051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( y  =  x  ->  (
( 1  -  ( E  /  N ) )  <  ( y `  t )  <->  ( 1  -  ( E  /  N ) )  < 
( x `  t
) ) )
318317ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  =  x  ->  ( A. t  e.  ( B `  j )
( 1  -  ( E  /  N ) )  <  ( y `  t )  <->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
x `  t )
) )
319316, 318anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  =  x  ->  (
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) )  <->  ( A. t  e.  ( D `  j ) ( x `
 t )  < 
( E  /  N
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
x `  t )
) ) )
320313, 3, 314, 319elrabf 2935 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( x  e.  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `
 t )  < 
( E  /  N
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
y `  t )
) }  <->  ( x  e.  Y  /\  ( A. t  e.  ( D `  j )
( x `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( x `  t
) ) ) )
321312, 320sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
x  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 )  /\  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) ) ) )  ->  x  e.  { y  e.  Y  | 
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) } )
322321ex 423 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( x  e.  A  /\  ( A. t  e.  T  ( 0  <_ 
( x `  t
)  /\  ( x `  t )  <_  1
)  /\  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) ) )  ->  x  e.  {
y  e.  Y  | 
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) } ) )
323322eximdv 1612 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( E. x ( x  e.  A  /\  ( A. t  e.  T  (
0  <_  ( x `  t )  /\  (
x `  t )  <_  1 )  /\  A. t  e.  ( D `  j ) ( x `
 t )  < 
( E  /  N
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
x `  t )
) )  ->  E. x  x  e.  { y  e.  Y  |  ( A. t  e.  ( D `  j )
( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) } ) )
324298, 323mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  E. x  x  e.  { y  e.  Y  |  ( A. t  e.  ( D `  j )
( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) } )
325 ne0i 3474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `
 t )  < 
( E  /  N
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
y `  t )
) }  ->  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) }  =/=  (/) )
326325eximi 1566 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( E. x  x  e.  {
y  e.  Y  | 
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }  ->  E. x { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) }  =/=  (/) )
327 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/ x { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }  =/=  (/)
328 id 19 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( { y  e.  Y  | 
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }  =/=  (/)  ->  { y  e.  Y  |  ( A. t  e.  ( D `  j )
( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) }  =/=  (/) )
329327, 328exlimi 1813 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( E. x { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `
 t )  < 
( E  /  N
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
y `  t )
) }  =/=  (/)  ->  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) }  =/=  (/) )
330326, 329syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( E. x  x  e.  {
y  e.  Y  | 
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }  ->  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `
 t )  < 
( E  /  N
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
y `  t )
) }  =/=  (/) )
331324, 330syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) }  =/=  (/) )
332158, 39jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
j  e.  ( 0 ... N )  /\  { y  e.  Y  | 
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }  e.  _V ) )
33341fvmpt2 5624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( j  e.  ( 0 ... N )  /\  { y  e.  Y  | 
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }  e.  _V )  -> 
( H `  j
)  =  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) } )
334332, 333syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( H `  j )  =  { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) } )
335334eqcomd 2301 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) }  =  ( H `  j ) )
336335neeq1d 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }  =/=  (/)  <->  ( H `  j )  =/=  (/) ) )
337336biimpd 198 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }  =/=  (/)  ->  ( H `  j )  =/=  (/) ) )
338331, 337mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( H `  j )  =/=  (/) )
3393383adant3 975 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  ( H `  j )  =  w )  ->  ( H `  j )  =/=  (/) )
340 simp3 957 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  ( H `  j )  =  w )  ->  ( H `  j )  =  w )
341 neeq1 2467 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( H `  j )  =  w  ->  (
( H `  j
)  =/=  (/)  <->  w  =/=  (/) ) )
342340, 341syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  ( H `  j )  =  w )  ->  ( ( H `  j )  =/=  (/)  <->  w  =/=  (/) ) )
343339, 342mpbid 201 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  ( H `  j )  =  w )  ->  w  =/=  (/) )
3443433exp 1150 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( j  e.  ( 0 ... N )  ->  ( ( H `
 j )  =  w  ->  w  =/=  (/) ) ) )
345344rexlimdv 2679 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( E. j  e.  ( 0 ... N
) ( H `  j )  =  w  ->  w  =/=  (/) ) )
346345adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  w  e.  ran  H )  ->  ( E. j  e.  (
0 ... N ) ( H `  j )  =  w  ->  w  =/=  (/) ) )
34792, 346mpd 14 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  w  e.  ran  H )  ->  w  =/=  (/) )
34878, 347syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  w  e.  ran  H )  ->  w  =/=  (/) )
34976, 348jca 518 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  w  e.  ran  H )  ->  ( ( A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )  /\  w  e.  ran  H )  /\  w  =/=  (/) ) )
350 rsp 2616 . . . . . . . . . . . . . . . . . . 19  |-  ( A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )  ->  (
w  e.  ran  H  ->  ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )
351350imp 418 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )  /\  w  e.  ran  H )  -> 
( w  =/=  (/)  ->  (
h `  w )  e.  w ) )
352351imp 418 . . . . . . . . . . . . . . . . 17  |-  ( ( ( A. w  e. 
ran  H ( w  =/=  (/)  ->  ( h `  w )  e.  w
)  /\  w  e.  ran  H )  /\  w  =/=  (/) )  ->  (
h `  w )  e.  w )
353349, 352syl 15 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  w  e.  ran  H )  ->  ( h `  w )  e.  w
)
354353ex 423 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( w  e. 
ran  H  ->  ( h `
 w )  e.  w ) )
35573, 354ralrimi 2637 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  A. w  e.  ran  H ( h `  w
)  e.  w )
35653, 355jca 518 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( h  Fn 
ran  H  /\  A. w  e.  ran  H ( h `
 w )  e.  w ) )
357 chfnrn 5652 . . . . . . . . . . . . 13  |-  ( ( h  Fn  ran  H  /\  A. w  e.  ran  H ( h `  w
)  e.  w )  ->  ran  h  C_  U. ran  H )
358356, 357syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ran  h  C_  U. ran  H )
359 nfv 1609 . . . . . . . . . . . . . . . . 17  |-  F/ y
ph
360 nfcv 2432 . . . . . . . . . . . . . . . . . . 19  |-  F/_ y
h
361 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ y
( 0 ... N
)
362 nfrab1 2733 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ y { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }
363361, 362nfmpt 4124 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ y
( j  e.  ( 0 ... N ) 
|->  { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) } )
36441, 363nfcxfr 2429 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ y H
365364nfrn 4937 . . . . . . . . . . . . . . . . . . 19  |-  F/_ y ran  H
366360, 365nffn 5356 . . . . . . . . . . . . . . . . . 18  |-  F/ y  h  Fn  ran  H
367 nfv 1609 . . . . . . . . . . . . . . . . . . 19  |-  F/ y ( w  =/=  (/)  ->  (
h `  w )  e.  w )
368365, 367nfral 2609 . . . . . . . . . . . . . . . . . 18  |-  F/ y A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )
369366, 368nfan 1783 . . . . . . . . . . . . . . . . 17  |-  F/ y ( h  Fn  ran  H  /\  A. w  e. 
ran  H ( w  =/=  (/)  ->  ( h `  w )  e.  w
) )
370359, 369nfan 1783 . . . . . . . . . . . . . . . 16  |-  F/ y ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )
371 simpll 730 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  y  e.  U. ran  H )  ->  ph )
372 simpr 447 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  y  e.  U. ran  H )  ->  y  e.  U. ran  H )
373371, 372jca 518 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  y  e.  U. ran  H )  ->  ( ph  /\  y  e.  U. ran  H ) )
374 fnunirn 5794 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( H  Fn  ( 0 ... N )  ->  (
y  e.  U. ran  H  <->  E. z  e.  (
0 ... N ) y  e.  ( H `  z ) ) )
375 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ j
y
376 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ j
z
37782, 376nffv 5548 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ j
( H `  z
)
378375, 377nfel 2440 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ j  y  e.  ( H `
 z )
379 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ z  y  e.  ( H `
 j )
380 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =  j  ->  ( H `  z )  =  ( H `  j ) )
381380eleq2d 2363 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  =  j  ->  (
y  e.  ( H `
 z )  <->  y  e.  ( H `  j ) ) )
382378, 379, 381cbvrex 2774 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. z  e.  ( 0 ... N ) y  e.  ( H `  z )  <->  E. j  e.  ( 0 ... N
) y  e.  ( H `  j ) )
383382a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( H  Fn  ( 0 ... N )  ->  ( E. z  e.  (
0 ... N ) y  e.  ( H `  z )  <->  E. j  e.  ( 0 ... N
) y  e.  ( H `  j ) ) )
384374, 383bitrd 244 . . . . . . . . . . . . . . . . . . . . 21  |-  ( H  Fn  ( 0 ... N )  ->  (
y  e.  U. ran  H  <->  E. j  e.  (
0 ... N ) y  e.  ( H `  j ) ) )
38543, 384syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( y  e.  U. ran  H  <->  E. j  e.  ( 0 ... N ) y  e.  ( H `
 j ) ) )
386385biimpa 470 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  U.
ran  H )  ->  E. j  e.  (
0 ... N ) y  e.  ( H `  j ) )
387 nfv 1609 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ j
ph
38882nfrn 4937 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ j ran  H
389388nfuni 3849 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ j U. ran  H
390375, 389nfel 2440 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ j  y  e.  U. ran  H
391387, 390nfan 1783 . . . . . . . . . . . . . . . . . . . 20  |-  F/ j ( ph  /\  y  e.  U. ran  H )
392 nfv 1609 . . . . . . . . . . . . . . . . . . . 20  |-  F/ j  y  e.  Y
393 simp1l 979 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  ph )
394 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  j  e.  ( 0 ... N
) )
395393, 394jca 518 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  ( ph  /\  j  e.  ( 0 ... N ) ) )
396 simp3 957 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  y  e.  ( H `  j ) )
397395, 396jca 518 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  ( ( ph  /\  j  e.  ( 0 ... N ) )  /\  y  e.  ( H `  j
) ) )
398334eleq2d 2363 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
y  e.  ( H `
 j )  <->  y  e.  { y  e.  Y  | 
( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) } ) )
399398biimpa 470 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  ( H `  j
) )  ->  y  e.  { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) } )
400 rabid 2729 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  { y  e.  Y  |  ( A. t  e.  ( D `  j ) ( y `
 t )  < 
( E  /  N
)  /\  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
y `  t )
) }  <->  ( y  e.  Y  /\  ( A. t  e.  ( D `  j )
( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) ) )
401399, 400sylib 188 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  ( H `  j
) )  ->  (
y  e.  Y  /\  ( A. t  e.  ( D `  j ) ( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) ) )
402401simpld 445 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  ( H `  j
) )  ->  y  e.  Y )
403397, 402syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  y  e.  Y )
4044033exp 1150 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  U.
ran  H )  -> 
( j  e.  ( 0 ... N )  ->  ( y  e.  ( H `  j
)  ->  y  e.  Y ) ) )
405391, 392, 404rexlimd 2677 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  y  e.  U.
ran  H )  -> 
( E. j  e.  ( 0 ... N
) y  e.  ( H `  j )  ->  y  e.  Y
) )
406386, 405mpd 14 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  U.
ran  H )  -> 
y  e.  Y )
407373, 406syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  y  e.  U. ran  H )  ->  y  e.  Y )
408407ex 423 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( y  e. 
U. ran  H  ->  y  e.  Y ) )
409370, 408alrimi 1757 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  A. y ( y  e.  U. ran  H  ->  y  e.  Y ) )
410 dfss2 3182 . . . . . . . . . . . . . . . 16  |-  ( U. ran  H  C_  Y  <->  A. a
( a  e.  U. ran  H  ->  a  e.  Y ) )
411 nfcv 2432 . . . . . . . . . . . . . . . . . . 19  |-  F/_ y
a
412365nfuni 3849 . . . . . . . . . . . . . . . . . . 19  |-  F/_ y U. ran  H
413411, 412nfel 2440 . . . . . . . . . . . . . . . . . 18  |-  F/ y  a  e.  U. ran  H
414411, 3nfel 2440 . . . . . . . . . . . . . . . . . 18  |-  F/ y  a  e.  Y
415413, 414nfim 1781 . . . . . . . . . . . . . . . . 17  |-  F/ y ( a  e.  U. ran  H  ->  a  e.  Y )
416 nfv 1609 . . . . . . . . . . . . . . . . 17  |-  F/ a ( y  e.  U. ran  H  ->  y  e.  Y )
417 eleq1 2356 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  y  ->  (
a  e.  U. ran  H  <-> 
y  e.  U. ran  H ) )
418 eleq1 2356 . . . . . . . . . . . . . . . . . 18  |-  ( a  =  y  ->  (
a  e.  Y  <->  y  e.  Y ) )
419417, 418imbi12d 311 . . . . . . . . . . . . . . . . 17  |-  ( a  =  y  ->  (
( a  e.  U. ran  H  ->  a  e.  Y )  <->  ( y  e.  U. ran  H  -> 
y  e.  Y ) ) )
420415, 416, 419cbval 1937 . . . . . . . . . . . . . . . 16  |-  ( A. a ( a  e. 
U. ran  H  ->  a  e.  Y )  <->  A. y
( y  e.  U. ran  H  ->  y  e.  Y ) )
421410, 420bitri 240 . . . . . . . . . . . . . . 15  |-  ( U. ran  H  C_  Y  <->  A. y
( y  e.  U. ran  H  ->  y  e.  Y ) )
422409, 421sylibr 203 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  U. ran  H  C_  Y )
42315a1i 10 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  Y  C_  A
)
424422, 423jca 518 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( U. ran  H 
C_  Y  /\  Y  C_  A ) )
425 sstr 3200 . . . . . . . . . . . . 13  |-  ( ( U. ran  H  C_  Y  /\  Y  C_  A
)  ->  U. ran  H  C_  A )
426424, 425syl 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  U. ran  H  C_  A )
427358, 426jca 518 . . . . . . . . . . 11  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( ran  h  C_ 
U. ran  H  /\  U.
ran  H  C_  A ) )
428 sstr 3200 . . . . . . . . . . 11  |-  ( ( ran  h  C_  U. ran  H  /\  U. ran  H  C_  A )  ->  ran  h  C_  A )
429427, 428syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ran  h  C_  A
)
43068, 429jca 518 . . . . . . . . 9  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( h : ran  H --> ran  h  /\  ran  h  C_  A
) )
431 fss 5413 . . . . . . . . 9  |-  ( ( h : ran  H