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

Theorem stoweidlem59 27786
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 . . . . . . . . . 10  |-  Y  =  { y  e.  A  |  A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 ) }
2 nfrab1 2890 . . . . . . . . . 10  |-  F/_ y { y  e.  A  |  A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 ) }
31, 2nfcxfr 2571 . . . . . . . . 9  |-  F/_ y Y
4 nfcv 2574 . . . . . . . . 9  |-  F/_ z Y
5 nfv 1630 . . . . . . . . 9  |-  F/ z ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) )
6 nfv 1630 . . . . . . . . 9  |-  F/ y ( A. t  e.  ( D `  j
) ( z `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( z `  t ) )
7 fveq1 5729 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
y `  t )  =  ( z `  t ) )
87breq1d 4224 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( y `  t
)  <  ( E  /  N )  <->  ( z `  t )  <  ( E  /  N ) ) )
98ralbidv 2727 . . . . . . . . . 10  |-  ( y  =  z  ->  ( A. t  e.  ( D `  j )
( y `  t
)  <  ( E  /  N )  <->  A. t  e.  ( D `  j
) ( z `  t )  <  ( E  /  N ) ) )
107breq2d 4226 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( 1  -  ( E  /  N ) )  <  ( y `  t )  <->  ( 1  -  ( E  /  N ) )  < 
( z `  t
) ) )
1110ralbidv 2727 . . . . . . . . . 10  |-  ( y  =  z  ->  ( A. t  e.  ( B `  j )
( 1  -  ( E  /  N ) )  <  ( y `  t )  <->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
z `  t )
) )
129, 11anbi12d 693 . . . . . . . . 9  |-  ( 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 2956 . . . . . . . 8  |-  { 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 stoweidlem59.10 . . . . . . . . . . . . 13  |-  ( ph  ->  J  e.  Comp )
15 cmptop 17460 . . . . . . . . . . . . 13  |-  ( J  e.  Comp  ->  J  e. 
Top )
1614, 15syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  J  e.  Top )
17 stoweidlem59.3 . . . . . . . . . . . . 13  |-  K  =  ( topGen `  ran  (,) )
18 retop 18797 . . . . . . . . . . . . 13  |-  ( topGen ` 
ran  (,) )  e.  Top
1917, 18eqeltri 2508 . . . . . . . . . . . 12  |-  K  e. 
Top
20 cnfex 27677 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  K  e.  Top )  ->  ( J  Cn  K
)  e.  _V )
2116, 19, 20sylancl 645 . . . . . . . . . . 11  |-  ( ph  ->  ( J  Cn  K
)  e.  _V )
22 stoweidlem59.11 . . . . . . . . . . . 12  |-  ( ph  ->  A  C_  C )
23 stoweidlem59.5 . . . . . . . . . . . 12  |-  C  =  ( J  Cn  K
)
2422, 23syl6sseq 3396 . . . . . . . . . . 11  |-  ( ph  ->  A  C_  ( J  Cn  K ) )
2521, 24ssexd 4352 . . . . . . . . . 10  |-  ( ph  ->  A  e.  _V )
26 ssrab2 3430 . . . . . . . . . . . 12  |-  { y  e.  A  |  A. t  e.  T  (
0  <_  ( y `  t )  /\  (
y `  t )  <_  1 ) }  C_  A
271, 26eqsstri 3380 . . . . . . . . . . 11  |-  Y  C_  A
2827a1i 11 . . . . . . . . . 10  |-  ( ph  ->  Y  C_  A )
2925, 28ssexd 4352 . . . . . . . . 9  |-  ( ph  ->  Y  e.  _V )
30 rabexg 4355 . . . . . . . . 9  |-  ( 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 )
3129, 30syl 16 . . . . . . . 8  |-  ( 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 )
3213, 31syl5eqel 2522 . . . . . . 7  |-  ( 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 )
3332ralrimivw 2792 . . . . . 6  |-  ( 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 )
34 stoweidlem59.9 . . . . . . 7  |-  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 ) ) } )
3534fnmpt 5573 . . . . . 6  |-  ( 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
) )
3633, 35syl 16 . . . . 5  |-  ( ph  ->  H  Fn  ( 0 ... N ) )
37 fzfi 11313 . . . . 5  |-  ( 0 ... N )  e. 
Fin
38 fnfi 7386 . . . . 5  |-  ( ( H  Fn  ( 0 ... N )  /\  ( 0 ... N
)  e.  Fin )  ->  H  e.  Fin )
3936, 37, 38sylancl 645 . . . 4  |-  ( ph  ->  H  e.  Fin )
40 rnfi 7393 . . . 4  |-  ( H  e.  Fin  ->  ran  H  e.  Fin )
4139, 40syl 16 . . 3  |-  ( ph  ->  ran  H  e.  Fin )
42 fnchoice 27678 . . 3  |-  ( ran 
H  e.  Fin  ->  E. h ( h  Fn 
ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  ( h `  w )  e.  w
) ) )
4341, 42syl 16 . 2  |-  ( ph  ->  E. h ( h  Fn  ran  H  /\  A. w  e.  ran  H
( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )
44 simprl 734 . . . . 5  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  h  Fn  ran  H )
45 ovex 6108 . . . . . . . 8  |-  ( 0 ... N )  e. 
_V
4645mptex 5968 . . . . . . 7  |-  ( 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
4734, 46eqeltri 2508 . . . . . 6  |-  H  e. 
_V
4847rnex 5135 . . . . 5  |-  ran  H  e.  _V
49 fnex 5963 . . . . 5  |-  ( ( h  Fn  ran  H  /\  ran  H  e.  _V )  ->  h  e.  _V )
5044, 48, 49sylancl 645 . . . 4  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  h  e.  _V )
51 coexg 5414 . . . 4  |-  ( ( h  e.  _V  /\  H  e.  _V )  ->  ( h  o.  H
)  e.  _V )
5250, 47, 51sylancl 645 . . 3  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( h  o.  H )  e.  _V )
53 dffn3 5600 . . . . . . 7  |-  ( h  Fn  ran  H  <->  h : ran  H --> ran  h )
5444, 53sylib 190 . . . . . 6  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  h : ran  H --> ran  h )
55 nfv 1630 . . . . . . . . . 10  |-  F/ w ph
56 nfv 1630 . . . . . . . . . . 11  |-  F/ w  h  Fn  ran  H
57 nfra1 2758 . . . . . . . . . . 11  |-  F/ w A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )
5856, 57nfan 1847 . . . . . . . . . 10  |-  F/ w
( h  Fn  ran  H  /\  A. w  e. 
ran  H ( w  =/=  (/)  ->  ( h `  w )  e.  w
) )
5955, 58nfan 1847 . . . . . . . . 9  |-  F/ w
( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )
60 simplrr 739 . . . . . . . . . . 11  |-  ( ( ( 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
) )
61 simpr 449 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  w  e.  ran  H )  ->  w  e.  ran  H )
62 fvelrnb 5776 . . . . . . . . . . . . . . . 16  |-  ( H  Fn  ( 0 ... N )  ->  (
w  e.  ran  H  <->  E. a  e.  ( 0 ... N ) ( H `  a )  =  w ) )
63 nfv 1630 . . . . . . . . . . . . . . . . 17  |-  F/ a ( H `  j
)  =  w
64 nfmpt1 4300 . . . . . . . . . . . . . . . . . . . 20  |-  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 ) ) } )
6534, 64nfcxfr 2571 . . . . . . . . . . . . . . . . . . 19  |-  F/_ j H
66 nfcv 2574 . . . . . . . . . . . . . . . . . . 19  |-  F/_ j
a
6765, 66nffv 5737 . . . . . . . . . . . . . . . . . 18  |-  F/_ j
( H `  a
)
68 nfcv 2574 . . . . . . . . . . . . . . . . . 18  |-  F/_ j
w
6967, 68nfeq 2581 . . . . . . . . . . . . . . . . 17  |-  F/ j ( H `  a
)  =  w
70 fveq2 5730 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  a  ->  ( H `  j )  =  ( H `  a ) )
7170eqeq1d 2446 . . . . . . . . . . . . . . . . 17  |-  ( j  =  a  ->  (
( H `  j
)  =  w  <->  ( H `  a )  =  w ) )
7263, 69, 71cbvrex 2931 . . . . . . . . . . . . . . . 16  |-  ( E. j  e.  ( 0 ... N ) ( H `  j )  =  w  <->  E. a  e.  ( 0 ... N
) ( H `  a )  =  w )
7362, 72syl6bbr 256 . . . . . . . . . . . . . . 15  |-  ( H  Fn  ( 0 ... N )  ->  (
w  e.  ran  H  <->  E. j  e.  ( 0 ... N ) ( H `  j )  =  w ) )
7436, 73syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( w  e.  ran  H  <->  E. j  e.  (
0 ... N ) ( H `  j )  =  w ) )
7574biimpa 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  w  e.  ran  H )  ->  E. j  e.  ( 0 ... N
) ( H `  j )  =  w )
76 simp3 960 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  ( H `  j )  =  w )  ->  ( H `  j )  =  w )
77 simpr 449 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  j  e.  ( 0 ... N
) )
7832adantr 453 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
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 )
7934fvmpt2 5814 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 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
) ) } )
8077, 78, 79syl2anc 644 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 ) ) } )
81 stoweidlem59.6 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  D  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
82 nfcv 2574 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ t
( 0 ... N
)
83 nfrab1 2890 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ t { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) }
8482, 83nfmpt 4299 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ t
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
8581, 84nfcxfr 2571 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ t D
86 nfcv 2574 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ t
j
8785, 86nffv 5737 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ t
( D `  j
)
88 nfcv 2574 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ t T
89 stoweidlem59.7 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  B  =  ( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
90 nfrab1 2890 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ t { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) }
9182, 90nfmpt 4299 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ t
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
9289, 91nfcxfr 2571 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ t B
9392, 86nffv 5737 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ t
( B `  j
)
9488, 93nfdif 3470 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ t
( T  \  ( B `  j )
)
95 stoweidlem59.2 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ t
ph
96 nfv 1630 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ t  j  e.  ( 0 ... N )
9795, 96nfan 1847 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ t ( ph  /\  j  e.  ( 0 ... N
) )
98 stoweidlem59.4 . . . . . . . . . . . . . . . . . . . . . . 23  |-  T  = 
U. J
9914adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  J  e.  Comp )
10022adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  A  C_  C )
101 stoweidlem59.12 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  +  ( g `  t ) ) )  e.  A )
1021013adant1r 1178 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  f  e.  A  /\  g  e.  A )  ->  (
t  e.  T  |->  ( ( f `  t
)  +  ( g `
 t ) ) )  e.  A )
103 stoweidlem59.13 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  x.  ( g `  t ) ) )  e.  A )
1041033adant1r 1178 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  f  e.  A  /\  g  e.  A )  ->  (
t  e.  T  |->  ( ( f `  t
)  x.  ( g `
 t ) ) )  e.  A )
105 stoweidlem59.14 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  RR )  ->  ( t  e.  T  |->  y )  e.  A )
106105adantlr 697 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  RR )  ->  (
t  e.  T  |->  y )  e.  A )
107 stoweidlem59.15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  ( r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
108107adantlr 697 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
109 uniexg 4708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( J  e.  Comp  ->  U. J  e.  _V )
11014, 109syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  U. J  e.  _V )
11198, 110syl5eqel 2522 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  T  e.  _V )
112111adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  T  e.  _V )
113 rabexg 4355 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( T  e.  _V  ->  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  e.  _V )
114112, 113syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  e.  _V )
11589fvmpt2 5814 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 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 ) } )
11677, 114, 115syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( B `  j )  =  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
117 stoweidlem59.1 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ t F
118 eqid 2438 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  =  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) }
119 elfzelz 11061 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  e.  ( 0 ... N )  ->  j  e.  ZZ )
120119zred 10377 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  e.  ( 0 ... N )  ->  j  e.  RR )
121 3re 10073 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  3  e.  RR
122 3ne0 10087 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  3  =/=  0
123121, 122rereccli 9781 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 1  /  3 )  e.  RR
124 readdcl 9075 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  RR  /\  ( 1  /  3
)  e.  RR )  ->  ( j  +  ( 1  /  3
) )  e.  RR )
125120, 123, 124sylancl 645 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  ( 1  /  3 ) )  e.  RR )
126125adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
j  +  ( 1  /  3 ) )  e.  RR )
127 stoweidlem59.17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  E  e.  RR+ )
128127rpred 10650 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  E  e.  RR )
129128adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  E  e.  RR )
130126, 129remulcld 9118 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  +  ( 1  /  3 ) )  x.  E )  e.  RR )
131 stoweidlem59.16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  F  e.  C )
132131, 23syl6eleq 2528 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  F  e.  ( J  Cn  K ) )
133132adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  F  e.  ( J  Cn  K
) )
134117, 17, 98, 118, 130, 133rfcnpre3 27682 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  e.  ( Clsd `  J )
)
135116, 134eqeltrd 2512 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( B `  j )  e.  ( Clsd `  J
) )
136 rabexg 4355 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( T  e.  _V  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
137112, 136syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  e.  _V )
13881fvmpt2 5814 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 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 ) } )
13977, 137, 138syl2anc 644 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( D `  j )  =  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
140 eqid 2438 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) }
141 resubcl 9367 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  RR  /\  ( 1  /  3
)  e.  RR )  ->  ( j  -  ( 1  /  3
) )  e.  RR )
142120, 123, 141sylancl 645 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  e.  ( 0 ... N )  ->  (
j  -  ( 1  /  3 ) )  e.  RR )
143142adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
j  -  ( 1  /  3 ) )  e.  RR )
144143, 129remulcld 9118 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  e.  RR )
145117, 17, 98, 140, 144, 133rfcnpre4 27683 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  e.  ( Clsd `  J )
)
146139, 145eqeltrd 2512 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( D `  j )  e.  ( Clsd `  J
) )
147144adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  e.  RR )
148130adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  +  ( 1  /  3 ) )  x.  E )  e.  RR )
14917, 98, 23, 131fcnre 27674 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  F : T --> RR )
150149ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  F : T --> RR )
151 ssrab2 3430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  C_  T
152116, 151syl6eqss 3400 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( B `  j )  C_  T )
153152sselda 3350 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  t  e.  T )
154150, 153ffvelrnd 5873 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  ( F `  t )  e.  RR )
155123, 141mpan2 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  RR  ->  (
j  -  ( 1  /  3 ) )  e.  RR )
156 id 21 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  RR  ->  j  e.  RR )
157123, 124mpan2 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  RR  ->  (
j  +  ( 1  /  3 ) )  e.  RR )
158 3pos 10086 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  0  <  3
159121, 158recgt0ii 9918 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  0  <  ( 1  /  3
)
160123, 159elrpii 10617 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( 1  /  3 )  e.  RR+
161 ltsubrp 10645 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( j  e.  RR  /\  ( 1  /  3
)  e.  RR+ )  ->  ( j  -  (
1  /  3 ) )  <  j )
162160, 161mpan2 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  RR  ->  (
j  -  ( 1  /  3 ) )  <  j )
163 ltaddrp 10646 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( j  e.  RR  /\  ( 1  /  3
)  e.  RR+ )  ->  j  <  ( j  +  ( 1  / 
3 ) ) )
164160, 163mpan2 654 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  RR  ->  j  <  ( j  +  ( 1  /  3 ) ) )
165155, 156, 157, 162, 164lttrd 9233 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( j  e.  RR  ->  (
j  -  ( 1  /  3 ) )  <  ( j  +  ( 1  /  3
) ) )
166120, 165syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( j  e.  ( 0 ... N )  ->  (
j  -  ( 1  /  3 ) )  <  ( j  +  ( 1  /  3
) ) )
167166adantl 454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
j  -  ( 1  /  3 ) )  <  ( j  +  ( 1  /  3
) ) )
168127rpregt0d 10656 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( E  e.  RR  /\  0  <  E ) )
169168adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( E  e.  RR  /\  0  <  E ) )
170 ltmul1 9862 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( 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
) ) )
171143, 126, 169, 170syl3anc 1185 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  -  (
1  /  3 ) )  <  ( j  +  ( 1  / 
3 ) )  <->  ( (
j  -  ( 1  /  3 ) )  x.  E )  < 
( ( j  +  ( 1  /  3
) )  x.  E
) ) )
172167, 171mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E ) )
173172adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E ) )
174116eleq2d 2505 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
t  e.  ( B `
 j )  <->  t  e.  { t  e.  T  | 
( ( j  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t ) } ) )
175174biimpa 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  t  e.  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
176 rabid 2886 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( t  e.  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_ 
( F `  t
) }  <->  ( t  e.  T  /\  (
( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) ) )
177175, 176sylib 190 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
t  e.  T  /\  ( ( j  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t ) ) )
178177simprd 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) )
179147, 148, 154, 173, 178ltletrd 9232 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  <  ( F `  t ) )
180147, 154ltnled 9222 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( ( j  -  ( 1  /  3
) )  x.  E
)  <  ( F `  t )  <->  -.  ( F `  t )  <_  ( ( j  -  ( 1  /  3
) )  x.  E
) ) )
181179, 180mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  -.  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) )
182181intnand 884 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  -.  ( t  e.  T  /\  ( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E ) ) )
183 rabid 2886 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  e.  { t  e.  T  |  ( F `
 t )  <_ 
( ( j  -  ( 1  /  3
) )  x.  E
) }  <->  ( t  e.  T  /\  ( F `  t )  <_  ( ( j  -  ( 1  /  3
) )  x.  E
) ) )
184182, 183sylnibr 298 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  -.  t  e.  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  /  3
) )  x.  E
) } )
185139adantr 453 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  ( D `  j )  =  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
186184, 185neleqtrrd 2534 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  -.  t  e.  ( D `  j ) )
187186ex 425 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
t  e.  ( B `
 j )  ->  -.  t  e.  ( D `  j )
) )
18897, 187ralrimi 2789 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  A. t  e.  ( B `  j
)  -.  t  e.  ( D `  j
) )
189 disj 3670 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( B `  j
)  i^i  ( D `  j ) )  =  (/) 
<-> 
A. a  e.  ( B `  j )  -.  a  e.  ( D `  j ) )
190 nfcv 2574 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ a
( B `  j
)
19187nfcri 2568 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/ t  a  e.  ( D `
 j )
192191nfn 1812 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ t  -.  a  e.  ( D `  j )
193 nfv 1630 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ a  -.  t  e.  ( D `  j )
194 eleq1 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  t  ->  (
a  e.  ( D `
 j )  <->  t  e.  ( D `  j ) ) )
195194notbid 287 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  t  ->  ( -.  a  e.  ( D `  j )  <->  -.  t  e.  ( D `
 j ) ) )
196190, 93, 192, 193, 195cbvralf 2928 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. a  e.  ( B `  j )  -.  a  e.  ( D `  j
)  <->  A. t  e.  ( B `  j )  -.  t  e.  ( D `  j ) )
197189, 196bitri 242 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( B `  j
)  i^i  ( D `  j ) )  =  (/) 
<-> 
A. t  e.  ( B `  j )  -.  t  e.  ( D `  j ) )
198188, 197sylibr 205 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( B `  j
)  i^i  ( D `  j ) )  =  (/) )
199 eqid 2438 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T 
\  ( B `  j ) )  =  ( T  \  ( B `  j )
)
200 stoweidlem59.19 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  N  e.  NN )
201200nnrpd 10649 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  N  e.  RR+ )
202127, 201rpdivcld 10667 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( E  /  N
)  e.  RR+ )
203202adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( E  /  N )  e.  RR+ )
204128, 200nndivred 10050 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( E  /  N
)  e.  RR )
205123a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( 1  /  3
)  e.  RR )
206200nnge1d 10044 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  1  <_  N )
207 1re 9092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  1  e.  RR
208 0lt1 9552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  0  <  1
209207, 208pm3.2i 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 1  e.  RR  /\  0  <  1 )
210209a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( 1  e.  RR  /\  0  <  1 ) )
211200nnred 10017 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  N  e.  RR )
212200nngt0d 10045 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  0  <  N )
213 lediv2 9902 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 1  e.  RR  /\  0  <  1 )  /\  ( N  e.  RR  /\  0  < 
N )  /\  ( E  e.  RR  /\  0  <  E ) )  -> 
( 1  <_  N  <->  ( E  /  N )  <_  ( E  / 
1 ) ) )
214210, 211, 212, 168, 213syl121anc 1190 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( 1  <_  N  <->  ( E  /  N )  <_  ( E  / 
1 ) ) )
215206, 214mpbid 203 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( E  /  N
)  <_  ( E  /  1 ) )
216127rpcnd 10652 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  E  e.  CC )
217216div1d 9784 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( E  /  1
)  =  E )
218215, 217breqtrd 4238 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( E  /  N
)  <_  E )
219 stoweidlem59.18 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  E  <  ( 1  /  3 ) )
220204, 128, 205, 218, 219lelttrd 9230 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( E  /  N
)  <  ( 1  /  3 ) )
221220adantr 453 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( E  /  N )  < 
( 1  /  3
) )
22287, 94, 97, 17, 98, 23, 99, 100, 102, 104, 106, 108, 135, 146, 198, 199, 203, 221stoweidlem58 27785 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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 )
) )
223 df-rex 2713 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 ) ) ) )
224222, 223sylib 190 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
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 ) ) ) )
225 simprl 734 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 )
226 simprr1 1006 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 ) )
227 fveq1 5729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  x  ->  (
y `  t )  =  ( x `  t ) )
228227breq2d 4226 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  =  x  ->  (
0  <_  ( y `  t )  <->  0  <_  ( x `  t ) ) )
229227breq1d 4224 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  =  x  ->  (
( y `  t
)  <_  1  <->  ( x `  t )  <_  1
) )
230228, 229anbi12d 693 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  x  ->  (
( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 )  <-> 
( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 ) ) )
231230ralbidv 2727 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  x  ->  ( A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 )  <->  A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 ) ) )
232231, 1elrab2 3096 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  Y  <->  ( x  e.  A  /\  A. t  e.  T  ( 0  <_  ( x `  t )  /\  (
x `  t )  <_  1 ) ) )
233225, 226, 232sylanbrc 647 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 )
234 simprr2 1007 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 ) )
235 simprr3 1008 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 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 )
)
236234, 235jca 520 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 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 )
) )
237 nfcv 2574 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ y
x
238 nfv 1630 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ y ( A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) )
239227breq1d 4224 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  x  ->  (
( y `  t
)  <  ( E  /  N )  <->  ( x `  t )  <  ( E  /  N ) ) )
240239ralbidv 2727 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  x  ->  ( A. t  e.  ( D `  j )
( y `  t
)  <  ( E  /  N )  <->  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N ) ) )
241227breq2d 4226 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  x  ->  (
( 1  -  ( E  /  N ) )  <  ( y `  t )  <->  ( 1  -  ( E  /  N ) )  < 
( x `  t
) ) )
242241ralbidv 2727 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  x  ->  ( A. t  e.  ( B `  j )
( 1  -  ( E  /  N ) )  <  ( y `  t )  <->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
x `  t )
) )
243240, 242anbi12d 693 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 )
) ) )
244237, 3, 238, 243elrabf 3093 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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
) ) ) )
245233, 236, 244sylanbrc 647 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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 ) ) } )
246245ex 425 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
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 ) ) } ) )
247246eximdv 1633 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
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
) ) } ) )
248224, 247mpd 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
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
) ) } )
249 ne0i 3636 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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
) ) }  =/=  (/) )
250249exlimiv 1645 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 )
) }  =/=  (/) )
251248, 250syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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
) ) }  =/=  (/) )
25280, 251eqnetrd 2621 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( H `  j )  =/=  (/) )
2532523adant3 978 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  ( H `  j )  =  w )  ->  ( H `  j )  =/=  (/) )
25476, 253eqnetrrd 2623 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  ( H `  j )  =  w )  ->  w  =/=  (/) )
2552543exp 1153 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( j  e.  ( 0 ... N )  ->  ( ( H `
 j )  =  w  ->  w  =/=  (/) ) ) )
256255rexlimdv 2831 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E. j  e.  ( 0 ... N
) ( H `  j )  =  w  ->  w  =/=  (/) ) )
257256adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  w  e.  ran  H )  ->  ( E. j  e.  (
0 ... N ) ( H `  j )  =  w  ->  w  =/=  (/) ) )
25875, 257mpd 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  w  e.  ran  H )  ->  w  =/=  (/) )
259258adantlr 697 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  w  e.  ran  H )  ->  w  =/=  (/) )
260 rsp 2768 . . . . . . . . . . 11  |-  ( A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )  ->  (
w  e.  ran  H  ->  ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )
26160, 61, 259, 260syl3c 60 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  w  e.  ran  H )  ->  ( h `  w )  e.  w
)
262261ex 425 . . . . . . . . 9  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( w  e. 
ran  H  ->  ( h `
 w )  e.  w ) )
26359, 262ralrimi 2789 . . . . . . . 8  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  A. w  e.  ran  H ( h `  w
)  e.  w )
264 chfnrn 5843 . . . . . . . 8  |-  ( ( h  Fn  ran  H  /\  A. w  e.  ran  H ( h `  w
)  e.  w )  ->  ran  h  C_  U. ran  H )
26544, 263, 264syl2anc 644 . . . . . . 7  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ran  h  C_  U. ran  H )
266 nfv 1630 . . . . . . . . . . 11  |-  F/ y
ph
267 nfcv 2574 . . . . . . . . . . . . 13  |-  F/_ y
h
268 nfcv 2574 . . . . . . . . . . . . . . . 16  |-  F/_ y
( 0 ... N
)
269 nfrab1 2890 . . . . . . . . . . . . . . . 16  |-  F/_ y { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }
270268, 269nfmpt 4299 . . . . . . . . . . . . . . 15  |-  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 ) ) } )
27134, 270nfcxfr 2571 . . . . . . . . . . . . . 14  |-  F/_ y H
272271nfrn 5114 . . . . . . . . . . . . 13  |-  F/_ y ran  H
273267, 272nffn 5543 . . . . . . . . . . . 12  |-  F/ y  h  Fn  ran  H
274 nfv 1630 . . . . . . . . . . . . 13  |-  F/ y ( w  =/=  (/)  ->  (
h `  w )  e.  w )
275272, 274nfral 2761 . . . . . . . . . . . 12  |-  F/ y A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )
276273, 275nfan 1847 . . . . . . . . . . 11  |-  F/ y ( h  Fn  ran  H  /\  A. w  e. 
ran  H ( w  =/=  (/)  ->  ( h `  w )  e.  w
) )
277266, 276nfan 1847 . . . . . . . . . 10  |-  F/ y ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )
278 fnunirn 6001 . . . . . . . . . . . . . . . 16  |-  ( H  Fn  ( 0 ... N )  ->  (
y  e.  U. ran  H  <->  E. z  e.  (
0 ... N ) y  e.  ( H `  z ) ) )
279 nfcv 2574 . . . . . . . . . . . . . . . . . . 19  |-  F/_ j
z
28065, 279nffv 5737 . . . . . . . . . . . . . . . . . 18  |-  F/_ j
( H `  z
)
281280nfcri 2568 . . . . . . . . . . . . . . . . 17  |-  F/ j  y  e.  ( H `
 z )
282 nfv 1630 . . . . . . . . . . . . . . . . 17  |-  F/ z  y  e.  ( H `
 j )
283 fveq2 5730 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  j  ->  ( H `  z )  =  ( H `  j ) )
284283eleq2d 2505 . . . . . . . . . . . . . . . . 17  |-  ( z  =  j  ->  (
y  e.  ( H `
 z )  <->  y  e.  ( H `  j ) ) )
285281, 282, 284cbvrex 2931 . . . . . . . . . . . . . . . 16  |-  ( E. z  e.  ( 0 ... N ) y  e.  ( H `  z )  <->  E. j  e.  ( 0 ... N
) y  e.  ( H `  j ) )
286278, 285syl6bb 254 . . . . . . . . . . . . . . 15  |-  ( H  Fn  ( 0 ... N )  ->  (
y  e.  U. ran  H  <->  E. j  e.  (
0 ... N ) y  e.  ( H `  j ) ) )
28736, 286syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( y  e.  U. ran  H  <->  E. j  e.  ( 0 ... N ) y  e.  ( H `
 j ) ) )
288287biimpa 472 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  U.
ran  H )  ->  E. j  e.  (
0 ... N ) y  e.  ( H `  j ) )
289 nfv 1630 . . . . . . . . . . . . . . 15  |-  F/ j
ph
29065nfrn 5114 . . . . . . . . . . . . . . . . 17  |-  F/_ j ran  H
291290nfuni 4023 . . . . . . . . . . . . . . . 16  |-  F/_ j U. ran  H
292291nfcri 2568 . . . . . . . . . . . . . . 15  |-  F/ j  y  e.  U. ran  H
293289, 292nfan 1847 . . . . . . . . . . . . . 14  |-  F/ j ( ph  /\  y  e.  U. ran  H )
294 nfv 1630 . . . . . . . . . . . . . 14  |-  F/ j  y  e.  Y
295 simp1l 982 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  ph )
296 simp2 959 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  j  e.  ( 0 ... N
) )
297 simp3 960 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  y  e.  ( H `  j ) )
29880eleq2d 2505 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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 ) ) } ) )
299298biimpa 472 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 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 ) ) } )
300 rabid 2886 . . . . . . . . . . . . . . . . . 18  |-  ( 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
) ) ) )
301299, 300sylib 190 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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
) ) ) )
302301simpld 447 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  ( H `  j
) )  ->  y  e.  Y )
303295, 296, 297, 302syl21anc 1184 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  y  e.  Y )
3043033exp 1153 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  U.
ran  H )  -> 
( j  e.  ( 0 ... N )  ->  ( y  e.  ( H `  j
)  ->  y  e.  Y ) ) )
305293, 294, 304rexlimd 2829 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  U.
ran  H )  -> 
( E. j  e.  ( 0 ... N
) y  e.  ( H `  j )  ->  y  e.  Y
) )
306288, 305mpd 15 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  U.
ran  H )  -> 
y  e.  Y )
307306adantlr 697 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  y  e.  U. ran  H )  ->  y  e.  Y )
308307ex 425 . . . . . . . . . 10  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( y  e. 
U. ran  H  ->  y  e.  Y ) )
309277, 308alrimi 1782 . . . . . . . . 9  |-  ( (
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 ) )
310272nfuni 4023 . . . . . . . . . 10  |-  F/_ y U. ran  H
311310, 3dfss2f 3341 . . . . . . . . 9  |-  ( U. ran  H  C_  Y  <->  A. y
( y  e.  U. ran  H  ->  y  e.  Y ) )
312309, 311sylibr 205 . . . . . . . 8  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  U. ran  H  C_  Y )
313312, 27syl6ss 3362 . . . . . . 7  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  U. ran  H  C_  A )
314265, 313sstrd 3360 . . . . . 6  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ran  h  C_  A
)
315 fss 5601 . . . . . 6  |-  ( ( h : ran  H --> ran  h  /\  ran  h  C_  A )  ->  h : ran  H --> A )
31654, 314, 315syl2anc 644 . . . . 5  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  h : ran  H --> A )
317 dffn3 5600 . . . . . . 7  |-  ( H  Fn  ( 0 ... N )  <->  H :
( 0 ... N
) --> ran  H )
31836, 317sylib 190 . . . . . 6  |-  ( ph  ->  H : ( 0 ... N ) --> ran 
H )
319318adantr 453 . . . . 5  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  H : ( 0 ... N ) --> ran  H )
320 fco 5602 . . . . 5  |-  ( ( h : ran  H --> A  /\  H : ( 0 ... N ) --> ran  H )  -> 
( h  o.  H
) : ( 0 ... N ) --> A )
321316, 319, 320syl2anc 644 . . . 4  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( h  o.  H ) : ( 0 ... N ) --> A )
322 nfcv 2574 . . . . . . . 8  |-  F/_ j
h
323322, 290nffn 5543 . . . . . . 7  |-  F/ j  h  Fn  ran  H
324 nfv 1630 . . . . . . . 8  |-  F/ j ( w  =/=  (/)  ->  (
h `  w )  e.  w )
325290, 324nfral 2761 . . . . . . 7  |-  F/ j A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )
326323, 325nfan 1847 . . . . . 6  |-  F/ j ( h  Fn  ran  H  /\  A. w  e. 
ran  H ( w  =/=  (/)  ->  ( h `  w )  e.  w
) )
327289, 326nfan 1847 . . . . 5  |-  F/ j ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )
328 simpll 732 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  ph )
329 simpr 449 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  j  e.  ( 0 ... N
) )
33036ad2antrr 708 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  H  Fn  ( 0 ... N
) )
331 fvco2 5800 . . . . . . . . . . . 12  |-  ( ( H  Fn  ( 0 ... N )  /\  j  e.  ( 0 ... N ) )  ->  ( ( h  o.  H ) `  j )  =  ( h `  ( H `
 j ) ) )
332330, 331sylancom 650 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  ( (
h  o.  H ) `
 j )  =  ( h `  ( H `  j )
) )
333 simplrr 739 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  A. w  e.  ran  H ( w  =/=  (/)  ->  ( h `  w )  e.  w
) )
334 fnfun 5544 . . . . . . . . . . . . . . . 16  |-  ( H  Fn  ( 0 ... N )  ->  Fun  H )
33536, 334syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Fun  H )
336335ad2antrr 708 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  Fun  H )
337 fndm 5546 . . . . . . . . . . . . . . . . . 18  |-  ( H  Fn  ( 0 ... N )  ->  dom  H  =  ( 0 ... N ) )
33836, 337syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  H  =  ( 0 ... N ) )
339338adantr 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  dom  H  =  ( 0 ... N ) )
34077, 339eleqtrrd 2515 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  j  e.  dom  H )
341340adantlr 697 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  j  e.  dom  H )
342 fvelrn 5868 . . . . . . . . . . . . . 14  |-  ( ( Fun  H  /\  j  e.  dom  H )  -> 
( H `  j
)  e.  ran  H
)
343336, 341, 342syl2anc 644 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  ( H `  j )  e.  ran  H )
344333, 343jca 520 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  ( A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )  /\  ( H `  j )  e.  ran  H ) )
345252adantlr 697 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  ( H `  j )  =/=  (/) )
346 neeq1 2611 . . . . . . . . . . . . . 14  |-  ( w  =  ( H `  j )  ->  (
w  =/=  (/)  <->  ( H `  j )  =/=  (/) ) )
347 fveq2 5730 . . . . . . . . . . . . . . 15  |-  ( w  =  ( H `  j )  ->  (
h `  w )  =  ( h `  ( H `  j ) ) )
348 id 21 . . . . . . . . . . . . . . 15  |-  ( w  =  ( H `  j )  ->  w  =  ( H `  j ) )
349347, 348eleq12d 2506 . . . . . . . . . . . . . 14  |-  ( w  =  ( H `  j )  ->  (
( h `  w
)  e.  w  <->  ( h `  ( H `  j
) )  e.  ( H `  j ) ) )
350346, 349imbi12d 313 . . . . . . . . . . . . 13  |-  ( w  =  ( H `  j )  ->  (
( w  =/=  (/)  ->  (
h `  w )  e.  w )  <->  ( ( H `  j )  =/=  (/)  ->  ( h `  ( H `  j
) )  e.  ( H `  j ) ) ) )
351350rspccva 3053 . . . . . . . . . . . 12  |-  ( ( A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )  /\  ( H `  j )  e.  ran  H )  -> 
( ( H `  j )  =/=  (/)  ->  (
h `  ( H `  j ) )  e.  ( H `  j
) ) )
352344, 345, 351sylc 59 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  ( h `  ( H `  j
) )  e.  ( H `  j ) )
353332, 352eqeltrd 2512 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  ( (
h  o.  H ) `
 j )  e.  ( H `  j
) )
354267, 271nfco 5040 . . . . . . . . . . . . 13  |-  F/_ y
( h  o.  H
)
355 nfcv 2574 . . . . . . . . . . . . 13  |-  F/_ y
j
356354, 355nffv 5737 . . . . . . . . . . . 12  |-  F/_ y
( ( h  o.  H ) `  j
)
357 nfv 1630 . . . . . . . . . . . . . 14  |-  F/ y ( ph  /\  j  e.  ( 0 ... N
) )
358271, 355nffv 5737 . . . . . . . . . . . . . . 15  |-  F/_ y
( H `  j
)
359356, 358nfel 2582 . . . . . . . . . . . . . 14  |-  F/ y ( ( h  o.  H ) `  j
)  e.  ( H `
 j )
360357, 359nfan 1847 . . . . . . . . . . . . 13  |-  F/ y ( ( ph  /\  j  e.  ( 0 ... N ) )  /\  ( ( h  o.  H ) `  j )  e.  ( H `  j ) )
361356, 3nfel 2582 . . . . . . . . . . . . 13  |-  F/ y ( ( h  o.  H ) `  j
)  e.  Y
362360, 361nfim 1833 . . . . . . . . . . . 12  |-  F/ y ( ( ( ph  /\  j  e.  ( 0 ... N ) )  /\  ( ( h  o.  H ) `  j )  e.  ( H `  j ) )  ->  ( (
h  o.  H ) `
 j )  e.  Y )
363 eleq1 2498 . . . . . . . . . . . . . 14  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
y  e.  ( H `
 j )  <->  ( (
h  o.  H ) `
 j )  e.  ( H `  j
) ) )
364363anbi2d 686 . . . . . . . . . . . . 13  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
( ( ph  /\  j  e.  ( 0 ... N ) )  /\  y  e.  ( H `  j ) )  <->  ( ( ph  /\  j  e.  ( 0 ... N ) )  /\  ( ( h  o.  H ) `  j )  e.  ( H `  j ) ) ) )
365 eleq1 2498 . . . . . . . . . . . . 13  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
y  e.  Y  <->  ( (
h  o.  H ) `
 j )  e.  Y ) )
366364, 365imbi12d 313 . . . . . . . . . . . 12  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
( ( ( ph  /\  j  e.  ( 0 ... N ) )  /\  y  e.  ( H `  j ) )  ->  y  e.  Y )  <->  ( (
( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( h  o.  H
) `  j )  e.  ( H `  j
) )  ->  (
( h  o.  H
) `  j )  e.  Y ) ) )
367356, 362, 366, 302vtoclgf 3012 . . . . . . . . . . 11  |-  ( ( ( h  o.  H
) `  j )  e.  ( H `  j
)  ->  ( (
( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( h  o.  H
) `  j )  e.  ( H `  j
) )  ->  (
( h  o.  H
) `  j )  e.  Y ) )
368367anabsi7 794 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( h  o.  H
) `  j )  e.  ( H `  j
) )  ->  (
( h  o.  H
) `  j )  e.  Y )
369328, 329, 353, 368syl21anc 1184 . . . . . . . . 9  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  ( (
h  o.  H ) `
 j )  e.  Y )
3701eleq2i 2502 . . . . . . . . . 10  |-  ( ( ( h  o.  H
) `  j )  e.  Y  <->  ( ( h  o.  H ) `  j )  e.  {
y  e.  A  |  A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 ) } )
371 nfcv 2574 . . . . . . . . . . 11  |-  F/_ y A
372 nfcv 2574 . . . . . . . . . . . 12  |-  F/_ y T
373 nfcv 2574 . . . . . . . . . . . . . 14  |-  F/_ y
0
374 nfcv 2574 . . . . . . . . . . . . . 14  |-  F/_ y  <_
375 nfcv 2574 . . . . . . . . . . . . . . 15  |-  F/_ y
t
376356, 375nffv 5737 . . . . . . . . . . . . . 14  |-  F/_ y
( ( ( h  o.  H ) `  j ) `  t
)
377373, 374, 376nfbr 4258 . . . . . . . . . . . . 13  |-  F/ y 0  <_  ( (
( h  o.  H
) `  j ) `  t )
378 nfcv 2574 . . . . . . . . . . . . . 14  |-  F/_ y
1
379376, 374, 378nfbr 4258 . . . . . . . . . . . . 13  |-  F/ y ( ( ( h  o.  H ) `  j ) `  t
)  <_  1
380377, 379nfan 1847 . . . . . . . . . . . 12  |-  F/ y ( 0  <_  (
( ( h  o.  H ) `  j
) `  t )  /\  ( ( ( h  o.  H ) `  j ) `  t
)  <_  1 )
381372, 380nfral 2761 . . . . . . . . . . 11  |-  F/ y A. t  e.  T  ( 0  <_  (
( ( h  o.  H ) `  j
) `  t )  /\  ( ( ( h  o.  H ) `  j ) `  t
)  <_  1 )
382 nfcv 2574 . . . . . . . . . . . . 13  |-  F/_ t
y
383 nfcv 2574 . . . . . . . . . . . . . . 15  |-  F/_ t
h
384 nfra1 2758 . . . . . . . . . . . . . . . . . . 19  |-  F/ t A. t  e.  ( D `  j ) ( y `  t
)  <  ( E  /  N )
385 nfra1 2758 . . . . . . . . . . . . . . . . . . 19  |-  F/ t A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  <  ( y `  t )
386384, 385nfan 1847 . . . . . . . . . . . . . . . . . 18  |-  F/ t ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) )
387 nfra1 2758 . . . . . . . . . . . . . . . . . . . 20  |-  F/ t A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 )
388 nfcv 2574 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ t A
389387, 388nfrab 2891 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t { y  e.  A  |  A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 ) }
3901, 389nfcxfr 2571 . . . . . . . . . . . . . . . . . 18  |-  F/_ t Y
391386, 390nfrab 2891 . . . . . . . . . . . . . . . . 17  |-  F/_ t { y  e.  Y  |  ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) ) }
39282, 391nfmpt 4299 . . . . . . . . . . . . . . . 16  |-  F/_ t
( 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 ) ) } )
39334, 392nfcxfr 2571 . . . . . . . . . . . . . . 15  |-  F/_ t H
394383, 393nfco 5040 . . . . . . . . . . . . . 14  |-  F/_ t
( h  o.  H
)
395394, 86nffv 5737 . . . . . . . . . . . . 13  |-  F/_ t
( ( h  o.  H ) `  j
)
396382, 395nfeq 2581 . . . . . . . . . . . 12  |-  F/ t  y  =  ( ( h  o.  H ) `
 j )
397 fveq1 5729 . . . . . . . . . . . . . 14  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
y `  t )  =  ( ( ( h  o.  H ) `
 j ) `  t ) )
398397breq2d 4226 . . . . . . . . . . . . 13  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
0  <_  ( y `  t )  <->  0  <_  ( ( ( h  o.  H ) `  j
) `  t )
) )
399397breq1d 4224 . . . . . . . . . . . . 13  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
( y `  t
)  <_  1  <->  ( (
( h  o.  H
) `  j ) `  t )  <_  1
) )
400398, 399anbi12d 693 . . . . . . . . . . . 12  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 )  <-> 
( 0  <_  (
( ( h  o.  H ) `  j
) `  t )  /\  ( ( ( h  o.  H ) `  j ) `  t
)  <_  1 ) ) )
401396, 400ralbid 2725 . . . . . . . . . . 11  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  ( A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 )  <->  A. t  e.  T  ( 0  <_  (
( ( h  o.  H ) `  j
) `  t )  /\  ( ( ( h  o.  H ) `  j ) `  t
)  <_  1 ) ) )
402356, 371, 381, 401elrabf 3093 . . . . . . . . . 10  |-  ( ( ( h  o.  H
) `  j )  e.  { y  e.  A  |  A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 ) }  <->  ( ( ( h  o.  H ) `
 j )  e.  A  /\  A. t  e.  T  ( 0  <_  ( ( ( h  o.  H ) `
 j ) `  t )  /\  (
( ( h  o.  H ) `  j
) `  t )  <_  1 ) ) )
403370, 402bitri 242 . . . . . . . . 9  |-  ( ( ( h  o.  H
) `  j )  e.  Y  <->  ( ( ( h  o.  H ) `
 j )  e.  A  /\  A. t  e.  T  ( 0  <_  ( ( ( h  o.  H ) `
 j ) `  t )  /\  (
( ( h  o.  H ) `  j
) `  t )  <_  1 ) ) )
404369, 403sylib 190 . . . . . . . 8  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  ( (
( h  o.  H
) `  j )  e.  A  /\  A. t  e.  T  ( 0  <_  ( ( ( h  o.  H ) `
 j ) `  t )  /\  (
( ( h  o.  H ) `  j
) `  t )  <_  1 ) ) )
405404simprd 451 . . . . . . 7  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  A. t  e.  T  ( 0  <_  ( ( ( h  o.  H ) `
 j ) `  t )  /\  (
( ( h  o.  H ) `  j
) `  t )  <_  1 ) )
406 nfcv 2574 . . . . . . . . . . . 12  |-  F/_ y
( D `  j
)
407 nfcv 2574 . . . . . . . . . . . . 13  |-  F/_ y  <
408 nfcv 2574 . . . . . . . . . . . . 13  |-  F/_ y
( E  /  N
)
409376, 407, 408nfbr 4258 . . . . . . . . . . . 12  |-  F/ y ( ( ( h  o.  H ) `  j ) `  t
)  <  ( E  /  N )
410406, 409nfral 2761 . . . . . . . . . . 11  |-  F/ y A. t  e.  ( D `  j ) ( ( ( h  o.  H ) `  j ) `  t
)  <  ( E  /  N )
411360, 410nfim 1833 . . . . . . . . . 10  |-  F/ y ( ( ( ph  /\  j  e.  ( 0 ... N ) )  /\  ( ( h  o.  H ) `  j )  e.  ( H `  j ) )  ->  A. t  e.  ( D `  j
) ( ( ( h  o.  H ) `
 j ) `  t )  <  ( E  /  N ) )
412397breq1d 4224 . . . . . . . . . . . 12  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
( y `  t
)  <  ( E  /  N )  <->  ( (
( h  o.  H
) `  j ) `  t )  <  ( E  /  N ) ) )
413396, 412ralbid 2725 . . . . . . . . . . 11  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  ( A. t  e.  ( D `  j )
( y `  t
)  <  ( E  /  N )  <->  A. t  e.  ( D `  j
) ( ( ( h  o.  H ) `
 j ) `  t )  <  ( E  /  N ) ) )
414364, 413imbi12d 313 . . . . . . . . . 10  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
( ( ( ph  /\  j  e.  ( 0 ... N ) )  /\  y  e.  ( H `  j ) )  ->  A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N ) )  <-> 
( ( ( ph  /\  j  e.  ( 0 ... N ) )  /\  ( ( h  o.  H ) `  j )  e.  ( H `  j ) )  ->  A. t  e.  ( D `  j
) ( ( ( h  o.  H ) `
 j ) `  t )  <  ( E  /  N ) ) ) )
415301simprd 451 . . . . . . . . . . 11  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  ( H `  j
) )  ->  ( A. t  e.  ( D `  j )
( y `  t
)  <  ( E  /  N )  /\  A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  < 
( y `  t
) ) )
416415simpld 447 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  ( H `  j
) )  ->  A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N ) )
417356, 411, 414, 416vtoclgf 3012 . . . . . . . . 9  |-  ( ( ( h  o.  H
) `  j )  e.  ( H `  j
)  ->  ( (
( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( h  o.  H
) `  j )  e.  ( H `  j
) )  ->  A. t  e.  ( D `  j
) ( ( ( h  o.  H ) `
 j ) `  t )  <  ( E  /  N ) ) )
418417anabsi7 794 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( h  o.  H
) `  j )  e.  ( H `  j
) )  ->  A. t  e.  ( D `  j
) ( ( ( h  o.  H ) `
 j ) `  t )  <  ( E  /  N ) )
419328, 329, 353, 418syl21anc 1184 . . . . . . 7  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  A. t  e.  ( D `  j
) ( ( ( h  o.  H ) `
 j ) `  t )  <  ( E  /  N ) )
420 nfcv 2574 . . . . . . . . . . . 12  |-  F/_ y
( B `  j
)
421 nfcv 2574 . . . . . . . . . . . . 13  |-  F/_ y
( 1  -  ( E  /  N ) )
422421, 407, 376nfbr 4258 . . . . . . . . . . . 12  |-  F/ y ( 1  -  ( E  /  N ) )  <  ( ( ( h  o.  H ) `
 j ) `  t )
423420, 422nfral 2761 . . . . . . . . . . 11  |-  F/ y A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  <  ( ( ( h  o.  H ) `
 j ) `  t )
424360, 423nfim 1833 . . . . . . . . . 10  |-  F/ y ( ( ( ph  /\  j  e.  ( 0 ... N ) )  /\  ( ( h  o.  H ) `  j )  e.  ( H `  j ) )  ->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
( ( h  o.  H ) `  j
) `  t )
)
425397breq2d 4226 . . . . . . . . . . . 12  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
( 1  -  ( E  /  N ) )  <  ( y `  t )  <->  ( 1  -  ( E  /  N ) )  < 
( ( ( h  o.  H ) `  j ) `  t
) ) )
426396, 425ralbid 2725 . . . . . . . . . . 11  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  ( A. t  e.  ( B `  j )
( 1  -  ( E  /  N ) )  <  ( y `  t )  <->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
( ( h  o.  H ) `  j
) `  t )
) )
427364, 426imbi12d 313 . . . . . . . . . 10  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
( ( ( ph  /\  j  e.  ( 0 ... N ) )  /\  y  e.  ( H `  j ) )  ->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
y `  t )
)  <->  ( ( (
ph  /\  j  e.  ( 0 ... N
) )  /\  (
( h  o.  H
) `  j )  e.  ( H `  j
) )  ->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
( ( h  o.  H ) `  j
) `  t )
) ) )
428415simprd 451 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  ( H `  j
) )  ->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
y `  t )
)
429356, 424, 427, 428vtoclgf 3012 . . . . . . . . 9  |-  ( ( ( h  o.  H
) `  j )  e.  ( H `  j
)  ->  ( (
( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( h  o.  H
) `  j )  e.  ( H `  j
) )  ->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
( ( h  o.  H ) `  j
) `  t )
) )
430429anabsi7 794 . . . . . . . 8  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( h  o.  H
) `  j )  e.  ( H `  j
) )  ->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
( ( h  o.  H ) `  j
) `  t )
)
431328, 329, 353, 430syl21anc 1184 . . . . . . 7  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
( ( h  o.  H ) `  j
) `  t )
)
432405, 419, 4313jca 1135 . . . . . 6  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  ( A. t  e.  T  (
0  <_  ( (
( h  o.  H
) `  j ) `  t )  /\  (
( ( h  o.  H ) `  j
) `  t )  <_  1 )  /\  A. t  e.  ( D `  j ) ( ( ( h  o.  H
) `  j ) `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( ( ( h  o.  H ) `
 j ) `  t ) ) )
433432ex 425 . . . . 5  |-  ( (
ph  /\  ( h  Fn  ran  H