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

Theorem stoweidlem59 27675
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 2848 . . . . . . . . . 10  |-  F/_ y { y  e.  A  |  A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 ) }
31, 2nfcxfr 2537 . . . . . . . . 9  |-  F/_ y Y
4 nfcv 2540 . . . . . . . . 9  |-  F/_ z Y
5 nfv 1626 . . . . . . . . 9  |-  F/ z ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) )
6 nfv 1626 . . . . . . . . 9  |-  F/ y ( A. t  e.  ( D `  j
) ( z `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( z `  t ) )
7 fveq1 5686 . . . . . . . . . . . 12  |-  ( y  =  z  ->  (
y `  t )  =  ( z `  t ) )
87breq1d 4182 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( y `  t
)  <  ( E  /  N )  <->  ( z `  t )  <  ( E  /  N ) ) )
98ralbidv 2686 . . . . . . . . . 10  |-  ( y  =  z  ->  ( A. t  e.  ( D `  j )
( y `  t
)  <  ( E  /  N )  <->  A. t  e.  ( D `  j
) ( z `  t )  <  ( E  /  N ) ) )
107breq2d 4184 . . . . . . . . . . 11  |-  ( y  =  z  ->  (
( 1  -  ( E  /  N ) )  <  ( y `  t )  <->  ( 1  -  ( E  /  N ) )  < 
( z `  t
) ) )
1110ralbidv 2686 . . . . . . . . . 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 692 . . . . . . . . 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 2914 . . . . . . . 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 17412 . . . . . . . . . . . . 13  |-  ( J  e.  Comp  ->  J  e. 
Top )
1614, 15syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  J  e.  Top )
17 stoweidlem59.3 . . . . . . . . . . . . 13  |-  K  =  ( topGen `  ran  (,) )
18 retop 18748 . . . . . . . . . . . . 13  |-  ( topGen ` 
ran  (,) )  e.  Top
1917, 18eqeltri 2474 . . . . . . . . . . . 12  |-  K  e. 
Top
20 cnfex 27566 . . . . . . . . . . . 12  |-  ( ( J  e.  Top  /\  K  e.  Top )  ->  ( J  Cn  K
)  e.  _V )
2116, 19, 20sylancl 644 . . . . . . . . . . 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 3354 . . . . . . . . . . 11  |-  ( ph  ->  A  C_  ( J  Cn  K ) )
2521, 24ssexd 4310 . . . . . . . . . 10  |-  ( ph  ->  A  e.  _V )
26 ssrab2 3388 . . . . . . . . . . . 12  |-  { y  e.  A  |  A. t  e.  T  (
0  <_  ( y `  t )  /\  (
y `  t )  <_  1 ) }  C_  A
271, 26eqsstri 3338 . . . . . . . . . . 11  |-  Y  C_  A
2827a1i 11 . . . . . . . . . 10  |-  ( ph  ->  Y  C_  A )
2925, 28ssexd 4310 . . . . . . . . 9  |-  ( ph  ->  Y  e.  _V )
30 rabexg 4313 . . . . . . . . 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 2488 . . . . . . 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 2750 . . . . . 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 5530 . . . . . 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 11266 . . . . 5  |-  ( 0 ... N )  e. 
Fin
38 fnfi 7343 . . . . 5  |-  ( ( H  Fn  ( 0 ... N )  /\  ( 0 ... N
)  e.  Fin )  ->  H  e.  Fin )
3936, 37, 38sylancl 644 . . . 4  |-  ( ph  ->  H  e.  Fin )
40 rnfi 7350 . . . 4  |-  ( H  e.  Fin  ->  ran  H  e.  Fin )
4139, 40syl 16 . . 3  |-  ( ph  ->  ran  H  e.  Fin )
42 fnchoice 27567 . . 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 733 . . . . 5  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  h  Fn  ran  H )
45 ovex 6065 . . . . . . . 8  |-  ( 0 ... N )  e. 
_V
4645mptex 5925 . . . . . . 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 2474 . . . . . 6  |-  H  e. 
_V
4847rnex 5092 . . . . 5  |-  ran  H  e.  _V
49 fnex 5920 . . . . 5  |-  ( ( h  Fn  ran  H  /\  ran  H  e.  _V )  ->  h  e.  _V )
5044, 48, 49sylancl 644 . . . 4  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  h  e.  _V )
51 coexg 5371 . . . 4  |-  ( ( h  e.  _V  /\  H  e.  _V )  ->  ( h  o.  H
)  e.  _V )
5250, 47, 51sylancl 644 . . 3  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( h  o.  H )  e.  _V )
53 dffn3 5557 . . . . . . 7  |-  ( h  Fn  ran  H  <->  h : ran  H --> ran  h )
5444, 53sylib 189 . . . . . 6  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  h : ran  H --> ran  h )
55 nfv 1626 . . . . . . . . . 10  |-  F/ w ph
56 nfv 1626 . . . . . . . . . . 11  |-  F/ w  h  Fn  ran  H
57 nfra1 2716 . . . . . . . . . . 11  |-  F/ w A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )
5856, 57nfan 1842 . . . . . . . . . 10  |-  F/ w
( h  Fn  ran  H  /\  A. w  e. 
ran  H ( w  =/=  (/)  ->  ( h `  w )  e.  w
) )
5955, 58nfan 1842 . . . . . . . . 9  |-  F/ w
( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )
60 simplrr 738 . . . . . . . . . . 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 448 . . . . . . . . . . 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 5733 . . . . . . . . . . . . . . . 16  |-  ( H  Fn  ( 0 ... N )  ->  (
w  e.  ran  H  <->  E. a  e.  ( 0 ... N ) ( H `  a )  =  w ) )
63 nfv 1626 . . . . . . . . . . . . . . . . 17  |-  F/ a ( H `  j
)  =  w
64 nfmpt1 4258 . . . . . . . . . . . . . . . . . . . 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 2537 . . . . . . . . . . . . . . . . . . 19  |-  F/_ j H
66 nfcv 2540 . . . . . . . . . . . . . . . . . . 19  |-  F/_ j
a
6765, 66nffv 5694 . . . . . . . . . . . . . . . . . 18  |-  F/_ j
( H `  a
)
68 nfcv 2540 . . . . . . . . . . . . . . . . . 18  |-  F/_ j
w
6967, 68nfeq 2547 . . . . . . . . . . . . . . . . 17  |-  F/ j ( H `  a
)  =  w
70 fveq2 5687 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  a  ->  ( H `  j )  =  ( H `  a ) )
7170eqeq1d 2412 . . . . . . . . . . . . . . . . 17  |-  ( j  =  a  ->  (
( H `  j
)  =  w  <->  ( H `  a )  =  w ) )
7263, 69, 71cbvrex 2889 . . . . . . . . . . . . . . . 16  |-  ( E. j  e.  ( 0 ... N ) ( H `  j )  =  w  <->  E. a  e.  ( 0 ... N
) ( H `  a )  =  w )
7362, 72syl6bbr 255 . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . 13  |-  ( (
ph  /\  w  e.  ran  H )  ->  E. j  e.  ( 0 ... N
) ( H `  j )  =  w )
76 simp3 959 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  ( H `  j )  =  w )  ->  ( H `  j )  =  w )
77 simpr 448 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  j  e.  ( 0 ... N
) )
7832adantr 452 . . . . . . . . . . . . . . . . . . . 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 5771 . . . . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . . . . 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 2540 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ t
( 0 ... N
)
83 nfrab1 2848 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ t { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) }
8482, 83nfmpt 4257 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ t
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
8581, 84nfcxfr 2537 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ t D
86 nfcv 2540 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ t
j
8785, 86nffv 5694 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ t
( D `  j
)
88 nfcv 2540 . . . . . . . . . . . . . . . . . . . . . . . 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 2848 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ t { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) }
9182, 90nfmpt 4257 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ t
( j  e.  ( 0 ... N ) 
|->  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
9289, 91nfcxfr 2537 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ t B
9392, 86nffv 5694 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/_ t
( B `  j
)
9488, 93nfdif 3428 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ t
( T  \  ( B `  j )
)
95 stoweidlem59.2 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ t
ph
96 nfv 1626 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ t  j  e.  ( 0 ... N )
9795, 96nfan 1842 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ t ( ph  /\  j  e.  ( 0 ... N
) )
98 stoweidlem59.4 . . . . . . . . . . . . . . . . . . . . . . 23  |-  T  = 
U. J
9914adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  J  e.  Comp )
10022adantr 452 . . . . . . . . . . . . . . . . . . . . . . 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 1177 . . . . . . . . . . . . . . . . . . . . . . 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 1177 . . . . . . . . . . . . . . . . . . . . . . 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 696 . . . . . . . . . . . . . . . . . . . . . . 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 696 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
109 uniexg 4665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( J  e.  Comp  ->  U. J  e.  _V )
11014, 109syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  U. J  e.  _V )
11198, 110syl5eqel 2488 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  T  e.  _V )
112111adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  T  e.  _V )
113 rabexg 4313 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5771 . . . . . . . . . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . . . . . . . . . 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 2404 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  =  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) }
119 elfzelz 11015 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  e.  ( 0 ... N )  ->  j  e.  ZZ )
120119zred 10331 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  e.  ( 0 ... N )  ->  j  e.  RR )
121 3re 10027 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  3  e.  RR
122 3ne0 10041 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  3  =/=  0
123121, 122rereccli 9735 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 1  /  3 )  e.  RR
124 readdcl 9029 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  RR  /\  ( 1  /  3
)  e.  RR )  ->  ( j  +  ( 1  /  3
) )  e.  RR )
125120, 123, 124sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  ( 1  /  3 ) )  e.  RR )
126125adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
j  +  ( 1  /  3 ) )  e.  RR )
127 stoweidlem59.17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  E  e.  RR+ )
128127rpred 10604 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  E  e.  RR )
129128adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  E  e.  RR )
130126, 129remulcld 9072 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  +  ( 1  /  3 ) )  x.  E )  e.  RR )
131 stoweidlem59.16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  F  e.  C )
132131, 23syl6eleq 2494 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  F  e.  ( J  Cn  K ) )
133132adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  F  e.  ( J  Cn  K
) )
134117, 17, 98, 118, 130, 133rfcnpre3 27571 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  e.  ( Clsd `  J )
)
135116, 134eqeltrd 2478 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( B `  j )  e.  ( Clsd `  J
) )
136 rabexg 4313 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5771 . . . . . . . . . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( D `  j )  =  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
140 eqid 2404 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  =  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) }
141 resubcl 9321 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( j  e.  RR  /\  ( 1  /  3
)  e.  RR )  ->  ( j  -  ( 1  /  3
) )  e.  RR )
142120, 123, 141sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  e.  ( 0 ... N )  ->  (
j  -  ( 1  /  3 ) )  e.  RR )
143142adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
j  -  ( 1  /  3 ) )  e.  RR )
144143, 129remulcld 9072 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  e.  RR )
145117, 17, 98, 140, 144, 133rfcnpre4 27572 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) }  e.  ( Clsd `  J )
)
146139, 145eqeltrd 2478 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( D `  j )  e.  ( Clsd `  J
) )
147144adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  e.  RR )
148130adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  +  ( 1  /  3 ) )  x.  E )  e.  RR )
14917, 98, 23, 131fcnre 27563 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  F : T --> RR )
150149ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  F : T --> RR )
151 ssrab2 3388 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  { t  e.  T  |  ( ( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) }  C_  T
152116, 151syl6eqss 3358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( B `  j )  C_  T )
153152sselda 3308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  t  e.  T )
154150, 153ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  ( F `  t )  e.  RR )
155123, 141mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  RR  ->  (
j  -  ( 1  /  3 ) )  e.  RR )
156 id 20 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  RR  ->  j  e.  RR )
157123, 124mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  RR  ->  (
j  +  ( 1  /  3 ) )  e.  RR )
158 3pos 10040 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  0  <  3
159121, 158recgt0ii 9872 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  0  <  ( 1  /  3
)
160123, 159elrpii 10571 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( 1  /  3 )  e.  RR+
161 ltsubrp 10599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( j  e.  RR  /\  ( 1  /  3
)  e.  RR+ )  ->  ( j  -  (
1  /  3 ) )  <  j )
162160, 161mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  RR  ->  (
j  -  ( 1  /  3 ) )  <  j )
163 ltaddrp 10600 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( ( j  e.  RR  /\  ( 1  /  3
)  e.  RR+ )  ->  j  <  ( j  +  ( 1  / 
3 ) ) )
164160, 163mpan2 653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( j  e.  RR  ->  j  <  ( j  +  ( 1  /  3 ) ) )
165155, 156, 157, 162, 164lttrd 9187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
j  -  ( 1  /  3 ) )  <  ( j  +  ( 1  /  3
) ) )
168127rpregt0d 10610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ph  ->  ( E  e.  RR  /\  0  <  E ) )
169168adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( E  e.  RR  /\  0  <  E ) )
170 ltmul1 9816 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  -  (
1  /  3 ) )  <  ( j  +  ( 1  / 
3 ) )  <->  ( (
j  -  ( 1  /  3 ) )  x.  E )  < 
( ( j  +  ( 1  /  3
) )  x.  E
) ) )
172167, 171mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E ) )
173172adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  <  ( ( j  +  ( 1  / 
3 ) )  x.  E ) )
174116eleq2d 2471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
t  e.  ( B `
 j )  <->  t  e.  { t  e.  T  | 
( ( j  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t ) } ) )
175174biimpa 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  t  e.  { t  e.  T  |  ( ( j  +  ( 1  / 
3 ) )  x.  E )  <_  ( F `  t ) } )
176 rabid 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
t  e.  T  /\  ( ( j  +  ( 1  /  3
) )  x.  E
)  <_  ( F `  t ) ) )
178177simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  +  ( 1  /  3 ) )  x.  E )  <_  ( F `  t ) )
179147, 148, 154, 173, 178ltletrd 9186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  (
( j  -  (
1  /  3 ) )  x.  E )  <  ( F `  t ) )
180147, 154ltnled 9176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  -.  ( F `  t )  <_  ( ( j  -  ( 1  / 
3 ) )  x.  E ) )
182181intnand 883 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  -.  ( t  e.  T  /\  ( F `  t
)  <_  ( (
j  -  ( 1  /  3 ) )  x.  E ) ) )
183 rabid 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 297 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  -.  t  e.  { t  e.  T  |  ( F `  t )  <_  ( ( j  -  ( 1  /  3
) )  x.  E
) } )
185139adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  ( D `  j )  =  { t  e.  T  |  ( F `  t )  <_  (
( j  -  (
1  /  3 ) )  x.  E ) } )
186184, 185neleqtrrd 2500 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  t  e.  ( B `  j
) )  ->  -.  t  e.  ( D `  j ) )
187186ex 424 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
t  e.  ( B `
 j )  ->  -.  t  e.  ( D `  j )
) )
18897, 187ralrimi 2747 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  A. t  e.  ( B `  j
)  -.  t  e.  ( D `  j
) )
189 disj 3628 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( B `  j
)  i^i  ( D `  j ) )  =  (/) 
<-> 
A. a  e.  ( B `  j )  -.  a  e.  ( D `  j ) )
190 nfcv 2540 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ a
( B `  j
)
19187nfcri 2534 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/ t  a  e.  ( D `
 j )
192191nfn 1807 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ t  -.  a  e.  ( D `  j )
193 nfv 1626 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ a  -.  t  e.  ( D `  j )
194 eleq1 2464 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( a  =  t  ->  (
a  e.  ( D `
 j )  <->  t  e.  ( D `  j ) ) )
195194notbid 286 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( a  =  t  ->  ( -.  a  e.  ( D `  j )  <->  -.  t  e.  ( D `
 j ) ) )
196190, 93, 192, 193, 195cbvralf 2886 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. a  e.  ( B `  j )  -.  a  e.  ( D `  j
)  <->  A. t  e.  ( B `  j )  -.  t  e.  ( D `  j ) )
197189, 196bitri 241 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( B `  j
)  i^i  ( D `  j ) )  =  (/) 
<-> 
A. t  e.  ( B `  j )  -.  t  e.  ( D `  j ) )
198188, 197sylibr 204 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  (
( B `  j
)  i^i  ( D `  j ) )  =  (/) )
199 eqid 2404 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( T 
\  ( B `  j ) )  =  ( T  \  ( B `  j )
)
200 stoweidlem59.19 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  N  e.  NN )
201200nnrpd 10603 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  N  e.  RR+ )
202127, 201rpdivcld 10621 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( E  /  N
)  e.  RR+ )
203202adantr 452 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( E  /  N )  e.  RR+ )
204128, 200nndivred 10004 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( E  /  N
)  e.  RR )
205123a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( 1  /  3
)  e.  RR )
206200nnge1d 9998 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  1  <_  N )
207 1re 9046 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  1  e.  RR
208 0lt1 9506 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  0  <  1
209207, 208pm3.2i 442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 1  e.  RR  /\  0  <  1 )
210209a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( 1  e.  RR  /\  0  <  1 ) )
211200nnred 9971 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  N  e.  RR )
212200nngt0d 9999 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  0  <  N )
213 lediv2 9856 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( 1  <_  N  <->  ( E  /  N )  <_  ( E  / 
1 ) ) )
215206, 214mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( E  /  N
)  <_  ( E  /  1 ) )
216127rpcnd 10606 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  E  e.  CC )
217216div1d 9738 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( E  /  1
)  =  E )
218215, 217breqtrd 4196 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( E  /  N
)  <_  E )
219 stoweidlem59.18 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  E  <  ( 1  /  3 ) )
220204, 128, 205, 218, 219lelttrd 9184 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( E  /  N
)  <  ( 1  /  3 ) )
221220adantr 452 . . . . . . . . . . . . . . . . . . . . . . 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 27674 . . . . . . . . . . . . . . . . . . . . . 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 2672 . . . . . . . . . . . . . . . . . . . . . 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 189 . . . . . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . . . . . . . . . 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 1005 . . . . . . . . . . . . . . . . . . . . . . . . 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 5686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  =  x  ->  (
y `  t )  =  ( x `  t ) )
228227breq2d 4184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  =  x  ->  (
0  <_  ( y `  t )  <->  0  <_  ( x `  t ) ) )
229227breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  =  x  ->  (
( y `  t
)  <_  1  <->  ( x `  t )  <_  1
) )
230228, 229anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  x  ->  (
( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 )  <-> 
( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 ) ) )
231230ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3054 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  Y  <->  ( x  e.  A  /\  A. t  e.  T  ( 0  <_  ( x `  t )  /\  (
x `  t )  <_  1 ) ) )
233225, 226, 232sylanbrc 646 . . . . . . . . . . . . . . . . . . . . . . . 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 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.  ( D `  j
) ( x `  t )  <  ( E  /  N ) )
235 simprr3 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.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
x `  t )
)
236234, 235jca 519 . . . . . . . . . . . . . . . . . . . . . . . 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 2540 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ y
x
238 nfv 1626 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ y ( A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( x `  t ) )
239227breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  x  ->  (
( y `  t
)  <  ( E  /  N )  <->  ( x `  t )  <  ( E  /  N ) ) )
240239ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  x  ->  ( A. t  e.  ( D `  j )
( y `  t
)  <  ( E  /  N )  <->  A. t  e.  ( D `  j
) ( x `  t )  <  ( E  /  N ) ) )
241227breq2d 4184 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  =  x  ->  (
( 1  -  ( E  /  N ) )  <  ( y `  t )  <->  ( 1  -  ( E  /  N ) )  < 
( x `  t
) ) )
242241ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . 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 692 . . . . . . . . . . . . . . . . . . . . . . . . 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 3051 . . . . . . . . . . . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . . . . . . . . . . . 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 424 . . . . . . . . . . . . . . . . . . . . . 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 1629 . . . . . . . . . . . . . . . . . . . . 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 3594 . . . . . . . . . . . . . . . . . . . . 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 1641 . . . . . . . . . . . . . . . . . . . 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 2585 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( H `  j )  =/=  (/) )
2532523adant3 977 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  ( H `  j )  =  w )  ->  ( H `  j )  =/=  (/) )
25476, 253eqnetrrd 2587 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... N
)  /\  ( H `  j )  =  w )  ->  w  =/=  (/) )
2552543exp 1152 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( j  e.  ( 0 ... N )  ->  ( ( H `
 j )  =  w  ->  w  =/=  (/) ) ) )
256255rexlimdv 2789 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E. j  e.  ( 0 ... N
) ( H `  j )  =  w  ->  w  =/=  (/) ) )
257256adantr 452 . . . . . . . . . . . . 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 696 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  w  e.  ran  H )  ->  w  =/=  (/) )
260 rsp 2726 . . . . . . . . . . 11  |-  ( A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )  ->  (
w  e.  ran  H  ->  ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )
26160, 61, 259, 260syl3c 59 . . . . . . . . . 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 424 . . . . . . . . 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 2747 . . . . . . . 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 5800 . . . . . . . 8  |-  ( ( h  Fn  ran  H  /\  A. w  e.  ran  H ( h `  w
)  e.  w )  ->  ran  h  C_  U. ran  H )
26544, 263, 264syl2anc 643 . . . . . . 7  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ran  h  C_  U. ran  H )
266 nfv 1626 . . . . . . . . . . 11  |-  F/ y
ph
267 nfcv 2540 . . . . . . . . . . . . 13  |-  F/_ y
h
268 nfcv 2540 . . . . . . . . . . . . . . . 16  |-  F/_ y
( 0 ... N
)
269 nfrab1 2848 . . . . . . . . . . . . . . . 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 4257 . . . . . . . . . . . . . . 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 2537 . . . . . . . . . . . . . 14  |-  F/_ y H
272271nfrn 5071 . . . . . . . . . . . . 13  |-  F/_ y ran  H
273267, 272nffn 5500 . . . . . . . . . . . 12  |-  F/ y  h  Fn  ran  H
274 nfv 1626 . . . . . . . . . . . . 13  |-  F/ y ( w  =/=  (/)  ->  (
h `  w )  e.  w )
275272, 274nfral 2719 . . . . . . . . . . . 12  |-  F/ y A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )
276273, 275nfan 1842 . . . . . . . . . . 11  |-  F/ y ( h  Fn  ran  H  /\  A. w  e. 
ran  H ( w  =/=  (/)  ->  ( h `  w )  e.  w
) )
277266, 276nfan 1842 . . . . . . . . . 10  |-  F/ y ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )
278 fnunirn 5958 . . . . . . . . . . . . . . . 16  |-  ( H  Fn  ( 0 ... N )  ->  (
y  e.  U. ran  H  <->  E. z  e.  (
0 ... N ) y  e.  ( H `  z ) ) )
279 nfcv 2540 . . . . . . . . . . . . . . . . . . 19  |-  F/_ j
z
28065, 279nffv 5694 . . . . . . . . . . . . . . . . . 18  |-  F/_ j
( H `  z
)
281280nfcri 2534 . . . . . . . . . . . . . . . . 17  |-  F/ j  y  e.  ( H `
 z )
282 nfv 1626 . . . . . . . . . . . . . . . . 17  |-  F/ z  y  e.  ( H `
 j )
283 fveq2 5687 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  j  ->  ( H `  z )  =  ( H `  j ) )
284283eleq2d 2471 . . . . . . . . . . . . . . . . 17  |-  ( z  =  j  ->  (
y  e.  ( H `
 z )  <->  y  e.  ( H `  j ) ) )
285281, 282, 284cbvrex 2889 . . . . . . . . . . . . . . . 16  |-  ( E. z  e.  ( 0 ... N ) y  e.  ( H `  z )  <->  E. j  e.  ( 0 ... N
) y  e.  ( H `  j ) )
286278, 285syl6bb 253 . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  U.
ran  H )  ->  E. j  e.  (
0 ... N ) y  e.  ( H `  j ) )
289 nfv 1626 . . . . . . . . . . . . . . 15  |-  F/ j
ph
29065nfrn 5071 . . . . . . . . . . . . . . . . 17  |-  F/_ j ran  H
291290nfuni 3981 . . . . . . . . . . . . . . . 16  |-  F/_ j U. ran  H
292291nfcri 2534 . . . . . . . . . . . . . . 15  |-  F/ j  y  e.  U. ran  H
293289, 292nfan 1842 . . . . . . . . . . . . . 14  |-  F/ j ( ph  /\  y  e.  U. ran  H )
294 nfv 1626 . . . . . . . . . . . . . 14  |-  F/ j  y  e.  Y
295 simp1l 981 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  ph )
296 simp2 958 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  j  e.  ( 0 ... N
) )
297 simp3 959 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  y  e.  ( H `  j ) )
29880eleq2d 2471 . . . . . . . . . . . . . . . . . . 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 471 . . . . . . . . . . . . . . . . . 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 2844 . . . . . . . . . . . . . . . . . 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 189 . . . . . . . . . . . . . . . . 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 446 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  ( H `  j
) )  ->  y  e.  Y )
303295, 296, 297, 302syl21anc 1183 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  U. ran  H )  /\  j  e.  ( 0 ... N )  /\  y  e.  ( H `  j ) )  ->  y  e.  Y )
3043033exp 1152 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  U.
ran  H )  -> 
( j  e.  ( 0 ... N )  ->  ( y  e.  ( H `  j
)  ->  y  e.  Y ) ) )
305293, 294, 304rexlimd 2787 . . . . . . . . . . . . 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 696 . . . . . . . . . . 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 424 . . . . . . . . . 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 1777 . . . . . . . . 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 3981 . . . . . . . . . 10  |-  F/_ y U. ran  H
311310, 3dfss2f 3299 . . . . . . . . 9  |-  ( U. ran  H  C_  Y  <->  A. y
( y  e.  U. ran  H  ->  y  e.  Y ) )
312309, 311sylibr 204 . . . . . . . 8  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  U. ran  H  C_  Y )
313312, 27syl6ss 3320 . . . . . . 7  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  U. ran  H  C_  A )
314265, 313sstrd 3318 . . . . . 6  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ran  h  C_  A
)
315 fss 5558 . . . . . 6  |-  ( ( h : ran  H --> ran  h  /\  ran  h  C_  A )  ->  h : ran  H --> A )
31654, 314, 315syl2anc 643 . . . . 5  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  h : ran  H --> A )
317 dffn3 5557 . . . . . . 7  |-  ( H  Fn  ( 0 ... N )  <->  H :
( 0 ... N
) --> ran  H )
31836, 317sylib 189 . . . . . 6  |-  ( ph  ->  H : ( 0 ... N ) --> ran 
H )
319318adantr 452 . . . . 5  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  H : ( 0 ... N ) --> ran  H )
320 fco 5559 . . . . 5  |-  ( ( h : ran  H --> A  /\  H : ( 0 ... N ) --> ran  H )  -> 
( h  o.  H
) : ( 0 ... N ) --> A )
321316, 319, 320syl2anc 643 . . . 4  |-  ( (
ph  /\  ( h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  ->  ( h  o.  H ) : ( 0 ... N ) --> A )
322 nfcv 2540 . . . . . . . 8  |-  F/_ j
h
323322, 290nffn 5500 . . . . . . 7  |-  F/ j  h  Fn  ran  H
324 nfv 1626 . . . . . . . 8  |-  F/ j ( w  =/=  (/)  ->  (
h `  w )  e.  w )
325290, 324nfral 2719 . . . . . . 7  |-  F/ j A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w )
326323, 325nfan 1842 . . . . . 6  |-  F/ j ( h  Fn  ran  H  /\  A. w  e. 
ran  H ( w  =/=  (/)  ->  ( h `  w )  e.  w
) )
327289, 326nfan 1842 . . . . 5  |-  F/ j ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )
328 simpll 731 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  ph )
329 simpr 448 . . . . . . . . . 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 707 . . . . . . . . . . . 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 5757 . . . . . . . . . . . 12  |-  ( ( H  Fn  ( 0 ... N )  /\  j  e.  ( 0 ... N ) )  ->  ( ( h  o.  H ) `  j )  =  ( h `  ( H `
 j ) ) )
332330, 331sylancom 649 . . . . . . . . . . 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 738 . . . . . . . . . . . . 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 5501 . . . . . . . . . . . . . . . 16  |-  ( H  Fn  ( 0 ... N )  ->  Fun  H )
33536, 334syl 16 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Fun  H )
336335ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  Fun  H )
337 fndm 5503 . . . . . . . . . . . . . . . . . 18  |-  ( H  Fn  ( 0 ... N )  ->  dom  H  =  ( 0 ... N ) )
33836, 337syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  dom  H  =  ( 0 ... N ) )
339338adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  dom  H  =  ( 0 ... N ) )
34077, 339eleqtrrd 2481 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  j  e.  dom  H )
341340adantlr 696 . . . . . . . . . . . . . 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 5825 . . . . . . . . . . . . . 14  |-  ( ( Fun  H  /\  j  e.  dom  H )  -> 
( H `  j
)  e.  ran  H
)
343336, 341, 342syl2anc 643 . . . . . . . . . . . . 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 519 . . . . . . . . . . . 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 696 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
h  Fn  ran  H  /\  A. w  e.  ran  H ( w  =/=  (/)  ->  (
h `  w )  e.  w ) ) )  /\  j  e.  ( 0 ... N ) )  ->  ( H `  j )  =/=  (/) )
346 neeq1 2575 . . . . . . . . . . . . . 14  |-  ( w  =  ( H `  j )  ->  (
w  =/=  (/)  <->  ( H `  j )  =/=  (/) ) )
347 fveq2 5687 . . . . . . . . . . . . . . 15  |-  ( w  =  ( H `  j )  ->  (
h `  w )  =  ( h `  ( H `  j ) ) )
348 id 20 . . . . . . . . . . . . . . 15  |-  ( w  =  ( H `  j )  ->  w  =  ( H `  j ) )
349347, 348eleq12d 2472 . . . . . . . . . . . . . 14  |-  ( w  =  ( H `  j )  ->  (
( h `  w
)  e.  w  <->  ( h `  ( H `  j
) )  e.  ( H `  j ) ) )
350346, 349imbi12d 312 . . . . . . . . . . . . 13  |-  ( w  =  ( H `  j )  ->  (
( w  =/=  (/)  ->  (
h `  w )  e.  w )  <->  ( ( H `  j )  =/=  (/)  ->  ( h `  ( H `  j
) )  e.  ( H `  j ) ) ) )
351350rspccva 3011 . . . . . . . . . . . 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 58 . . . . . . . . . . 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 2478 . . . . . . . . . 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 4997 . . . . . . . . . . . . 13  |-  F/_ y
( h  o.  H
)
355 nfcv 2540 . . . . . . . . . . . . 13  |-  F/_ y
j
356354, 355nffv 5694 . . . . . . . . . . . 12  |-  F/_ y
( ( h  o.  H ) `  j
)
357 nfv 1626 . . . . . . . . . . . . . 14  |-  F/ y ( ph  /\  j  e.  ( 0 ... N
) )
358271, 355nffv 5694 . . . . . . . . . . . . . . 15  |-  F/_ y
( H `  j
)
359356, 358nfel 2548 . . . . . . . . . . . . . 14  |-  F/ y ( ( h  o.  H ) `  j
)  e.  ( H `
 j )
360357, 359nfan 1842 . . . . . . . . . . . . 13  |-  F/ y ( ( ph  /\  j  e.  ( 0 ... N ) )  /\  ( ( h  o.  H ) `  j )  e.  ( H `  j ) )
361356, 3nfel 2548 . . . . . . . . . . . . 13  |-  F/ y ( ( h  o.  H ) `  j
)  e.  Y
362360, 361nfim 1828 . . . . . . . . . . . 12  |-  F/ y ( ( ( ph  /\  j  e.  ( 0 ... N ) )  /\  ( ( h  o.  H ) `  j )  e.  ( H `  j ) )  ->  ( (
h  o.  H ) `
 j )  e.  Y )
363 eleq1 2464 . . . . . . . . . . . . . 14  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
y  e.  ( H `
 j )  <->  ( (
h  o.  H ) `
 j )  e.  ( H `  j
) ) )
364363anbi2d 685 . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . 13  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
y  e.  Y  <->  ( (
h  o.  H ) `
 j )  e.  Y ) )
366364, 365imbi12d 312 . . . . . . . . . . . 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 2970 . . . . . . . . . . 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 793 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  (
( h  o.  H
) `  j )  e.  ( H `  j
) )  ->  (
( h  o.  H
) `  j )  e.  Y )
369328, 329, 353, 368syl21anc 1183 . . . . . . . . 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 2468 . . . . . . . . . 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 2540 . . . . . . . . . . 11  |-  F/_ y A
372 nfcv 2540 . . . . . . . . . . . 12  |-  F/_ y T
373 nfcv 2540 . . . . . . . . . . . . . 14  |-  F/_ y
0
374 nfcv 2540 . . . . . . . . . . . . . 14  |-  F/_ y  <_
375 nfcv 2540 . . . . . . . . . . . . . . 15  |-  F/_ y
t
376356, 375nffv 5694 . . . . . . . . . . . . . 14  |-  F/_ y
( ( ( h  o.  H ) `  j ) `  t
)
377373, 374, 376nfbr 4216 . . . . . . . . . . . . 13  |-  F/ y 0  <_  ( (
( h  o.  H
) `  j ) `  t )
378 nfcv 2540 . . . . . . . . . . . . . 14  |-  F/_ y
1
379376, 374, 378nfbr 4216 . . . . . . . . . . . . 13  |-  F/ y ( ( ( h  o.  H ) `  j ) `  t
)  <_  1
380377, 379nfan 1842 . . . . . . . . . . . 12  |-  F/ y ( 0  <_  (
( ( h  o.  H ) `  j
) `  t )  /\  ( ( ( h  o.  H ) `  j ) `  t
)  <_  1 )
381372, 380nfral 2719 . . . . . . . . . . 11  |-  F/ y A. t  e.  T  ( 0  <_  (
( ( h  o.  H ) `  j
) `  t )  /\  ( ( ( h  o.  H ) `  j ) `  t
)  <_  1 )
382 nfcv 2540 . . . . . . . . . . . . 13  |-  F/_ t
y
383 nfcv 2540 . . . . . . . . . . . . . . 15  |-  F/_ t
h
384 nfra1 2716 . . . . . . . . . . . . . . . . . . 19  |-  F/ t A. t  e.  ( D `  j ) ( y `  t
)  <  ( E  /  N )
385 nfra1 2716 . . . . . . . . . . . . . . . . . . 19  |-  F/ t A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  <  ( y `  t )
386384, 385nfan 1842 . . . . . . . . . . . . . . . . . 18  |-  F/ t ( A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N )  /\  A. t  e.  ( B `
 j ) ( 1  -  ( E  /  N ) )  <  ( y `  t ) )
387 nfra1 2716 . . . . . . . . . . . . . . . . . . . 20  |-  F/ t A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 )
388 nfcv 2540 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ t A
389387, 388nfrab 2849 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t { y  e.  A  |  A. t  e.  T  ( 0  <_  (
y `  t )  /\  ( y `  t
)  <_  1 ) }
3901, 389nfcxfr 2537 . . . . . . . . . . . . . . . . . 18  |-  F/_ t Y
391386, 390nfrab 2849 . . . . . . . . . . . . . . . . 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 4257 . . . . . . . . . . . . . . . 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 2537 . . . . . . . . . . . . . . 15  |-  F/_ t H
394383, 393nfco 4997 . . . . . . . . . . . . . 14  |-  F/_ t
( h  o.  H
)
395394, 86nffv 5694 . . . . . . . . . . . . 13  |-  F/_ t
( ( h  o.  H ) `  j
)
396382, 395nfeq 2547 . . . . . . . . . . . 12  |-  F/ t  y  =  ( ( h  o.  H ) `
 j )
397 fveq1 5686 . . . . . . . . . . . . . 14  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
y `  t )  =  ( ( ( h  o.  H ) `
 j ) `  t ) )
398397breq2d 4184 . . . . . . . . . . . . 13  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
0  <_  ( y `  t )  <->  0  <_  ( ( ( h  o.  H ) `  j
) `  t )
) )
399397breq1d 4182 . . . . . . . . . . . . 13  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
( y `  t
)  <_  1  <->  ( (
( h  o.  H
) `  j ) `  t )  <_  1
) )
400398, 399anbi12d 692 . . . . . . . . . . . 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 2684 . . . . . . . . . . 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 3051 . . . . . . . . . 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 241 . . . . . . . . 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 189 . . . . . . . 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 450 . . . . . . 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 2540 . . . . . . . . . . . 12  |-  F/_ y
( D `  j
)
407 nfcv 2540 . . . . . . . . . . . . 13  |-  F/_ y  <
408 nfcv 2540 . . . . . . . . . . . . 13  |-  F/_ y
( E  /  N
)
409376, 407, 408nfbr 4216 . . . . . . . . . . . 12  |-  F/ y ( ( ( h  o.  H ) `  j ) `  t
)  <  ( E  /  N )
410406, 409nfral 2719 . . . . . . . . . . 11  |-  F/ y A. t  e.  ( D `  j ) ( ( ( h  o.  H ) `  j ) `  t
)  <  ( E  /  N )
411360, 410nfim 1828 . . . . . . . . . 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 4182 . . . . . . . . . . . 12  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
( y `  t
)  <  ( E  /  N )  <->  ( (
( h  o.  H
) `  j ) `  t )  <  ( E  /  N ) ) )
413396, 412ralbid 2684 . . . . . . . . . . 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 312 . . . . . . . . . 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 450 . . . . . . . . . . 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 446 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  ( H `  j
) )  ->  A. t  e.  ( D `  j
) ( y `  t )  <  ( E  /  N ) )
417356, 411, 414, 416vtoclgf 2970 . . . . . . . . 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 793 . . . . . . . 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 1183 . . . . . . 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 2540 . . . . . . . . . . . 12  |-  F/_ y
( B `  j
)
421 nfcv 2540 . . . . . . . . . . . . 13  |-  F/_ y
( 1  -  ( E  /  N ) )
422421, 407, 376nfbr 4216 . . . . . . . . . . . 12  |-  F/ y ( 1  -  ( E  /  N ) )  <  ( ( ( h  o.  H ) `
 j ) `  t )
423420, 422nfral 2719 . . . . . . . . . . 11  |-  F/ y A. t  e.  ( B `  j ) ( 1  -  ( E  /  N ) )  <  ( ( ( h  o.  H ) `
 j ) `  t )
424360, 423nfim 1828 . . . . . . . . . 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 4184 . . . . . . . . . . . 12  |-  ( y  =  ( ( h  o.  H ) `  j )  ->  (
( 1  -  ( E  /  N ) )  <  ( y `  t )  <->  ( 1  -  ( E  /  N ) )  < 
( ( ( h  o.  H ) `  j ) `  t
) ) )
426396, 425ralbid 2684 . . . . . . . . . . 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 312 . . . . . . . . . 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 450 . . . . . . . . . 10  |-  ( ( ( ph  /\  j  e.  ( 0 ... N
) )  /\  y  e.  ( H `  j
) )  ->  A. t  e.  ( B `  j
) ( 1  -  ( E  /  N
) )  <  (
y `  t )
)
429356, 424, 427, 428vtoclgf 2970 . . . . . . . . 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 793 . . . . . . . 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 1183 . . . . . . 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 1134 . . . . . 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 424 . . . . 5  |-  ( (
ph  /\  ( h  Fn  ran  H  /\