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

Theorem stoweidlem31 29823
Description: This lemma is used to prove that there exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91: assuming that  R is a finite subset of  V,  x indexes a finite set of functions in the subalgebra (of the Stone Weierstrass theorem), such that for all  i ranging in the finite indexing set, 0 ≤ xi ≤ 1, xi < ε / m on V(ti), and xi > 1 - ε / m on  B. Here M is used to represent m in the paper,  E is used to represent ε in the paper, vi is used to represent V(ti). (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem31.1  |-  F/ h ph
stoweidlem31.2  |-  F/ t
ph
stoweidlem31.3  |-  F/ w ph
stoweidlem31.4  |-  Y  =  { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }
stoweidlem31.5  |-  V  =  { w  e.  J  |  A. e  e.  RR+  E. h  e.  A  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  e  /\  A. t  e.  ( T  \  U ) ( 1  -  e
)  <  ( h `  t ) ) }
stoweidlem31.6  |-  G  =  ( w  e.  R  |->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )
stoweidlem31.7  |-  ( ph  ->  R  C_  V )
stoweidlem31.8  |-  ( ph  ->  M  e.  NN )
stoweidlem31.9  |-  ( ph  ->  v : ( 1 ... M ) -1-1-onto-> R )
stoweidlem31.10  |-  ( ph  ->  E  e.  RR+ )
stoweidlem31.11  |-  ( ph  ->  B  C_  ( T  \  U ) )
stoweidlem31.12  |-  ( ph  ->  V  e.  _V )
stoweidlem31.13  |-  ( ph  ->  A  e.  _V )
stoweidlem31.14  |-  ( ph  ->  ran  G  e.  Fin )
Assertion
Ref Expression
stoweidlem31  |-  ( ph  ->  E. x ( x : ( 1 ... M ) --> Y  /\  A. i  e.  ( 1 ... M ) ( A. t  e.  ( v `  i ) ( ( x `  i ) `  t
)  <  ( E  /  M )  /\  A. t  e.  B  (
1  -  ( E  /  M ) )  <  ( ( x `
 i ) `  t ) ) ) )
Distinct variable groups:    h, i,
t, v, w    i, G    w, Y    ph, i    e, h, t, w, A    e, E, h, t, w    e, M, h, t, w    T, e, h, w    U, e, h, w    R, h, t, w    x, i, t, v    i, M   
x, B    x, E    x, G    x, M    x, Y
Allowed substitution hints:    ph( x, w, v, t, e, h)    A( x, v, i)    B( w, v, t, e, h, i)    R( x, v, e, i)    T( x, v, t, i)    U( x, v, t, i)    E( v, i)    G( w, v, t, e, h)    J( x, w, v, t, e, h, i)    M( v)    V( x, w, v, t, e, h, i)    Y( v, t, e, h, i)

Proof of Theorem stoweidlem31
Dummy variables  b 
l  u  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem31.14 . . 3  |-  ( ph  ->  ran  G  e.  Fin )
2 fnchoice 29748 . . 3  |-  ( ran 
G  e.  Fin  ->  E. l ( l  Fn 
ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )
31, 2syl 16 . 2  |-  ( ph  ->  E. l ( l  Fn  ran  G  /\  A. b  e.  ran  G
( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
4 vex 2973 . . . . 5  |-  l  e. 
_V
5 stoweidlem31.6 . . . . . . 7  |-  G  =  ( w  e.  R  |->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )
6 stoweidlem31.12 . . . . . . . . 9  |-  ( ph  ->  V  e.  _V )
7 stoweidlem31.7 . . . . . . . . 9  |-  ( ph  ->  R  C_  V )
86, 7ssexd 4437 . . . . . . . 8  |-  ( ph  ->  R  e.  _V )
9 mptexg 5945 . . . . . . . 8  |-  ( R  e.  _V  ->  (
w  e.  R  |->  { h  e.  A  | 
( A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
)  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } )  e.  _V )
108, 9syl 16 . . . . . . 7  |-  ( ph  ->  ( w  e.  R  |->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )  e. 
_V )
115, 10syl5eqel 2525 . . . . . 6  |-  ( ph  ->  G  e.  _V )
12 vex 2973 . . . . . 6  |-  v  e. 
_V
13 coexg 6526 . . . . . 6  |-  ( ( G  e.  _V  /\  v  e.  _V )  ->  ( G  o.  v
)  e.  _V )
1411, 12, 13sylancl 662 . . . . 5  |-  ( ph  ->  ( G  o.  v
)  e.  _V )
15 coexg 6526 . . . . 5  |-  ( ( l  e.  _V  /\  ( G  o.  v
)  e.  _V )  ->  ( l  o.  ( G  o.  v )
)  e.  _V )
164, 14, 15sylancr 663 . . . 4  |-  ( ph  ->  ( l  o.  ( G  o.  v )
)  e.  _V )
1716adantr 465 . . 3  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( l  o.  ( G  o.  v
) )  e.  _V )
18 simprl 755 . . . . . 6  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  l  Fn  ran  G )
19 stoweidlem31.1 . . . . . . . . 9  |-  F/ h ph
20 nfcv 2577 . . . . . . . . . . 11  |-  F/_ h
l
21 nfcv 2577 . . . . . . . . . . . . . 14  |-  F/_ h R
22 nfrab1 2899 . . . . . . . . . . . . . 14  |-  F/_ h { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }
2321, 22nfmpt 4378 . . . . . . . . . . . . 13  |-  F/_ h
( w  e.  R  |->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )
245, 23nfcxfr 2574 . . . . . . . . . . . 12  |-  F/_ h G
2524nfrn 5080 . . . . . . . . . . 11  |-  F/_ h ran  G
2620, 25nffn 5505 . . . . . . . . . 10  |-  F/ h  l  Fn  ran  G
27 nfv 1673 . . . . . . . . . . 11  |-  F/ h
( b  =/=  (/)  ->  (
l `  b )  e.  b )
2825, 27nfral 2767 . . . . . . . . . 10  |-  F/ h A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )
2926, 28nfan 1861 . . . . . . . . 9  |-  F/ h
( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
3019, 29nfan 1861 . . . . . . . 8  |-  F/ h
( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
31 fvelrnb 5737 . . . . . . . . . . . . 13  |-  ( l  Fn  ran  G  -> 
( h  e.  ran  l 
<->  E. b  e.  ran  G ( l `  b
)  =  h ) )
3218, 31syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( h  e. 
ran  l  <->  E. b  e.  ran  G ( l `
 b )  =  h ) )
3332biimpa 484 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  ->  E. b  e.  ran  G ( l `
 b )  =  h )
34 nfv 1673 . . . . . . . . . . . . . 14  |-  F/ b
ph
35 nfv 1673 . . . . . . . . . . . . . . 15  |-  F/ b  l  Fn  ran  G
36 nfra1 2764 . . . . . . . . . . . . . . 15  |-  F/ b A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )
3735, 36nfan 1861 . . . . . . . . . . . . . 14  |-  F/ b ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
3834, 37nfan 1861 . . . . . . . . . . . . 13  |-  F/ b ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
39 nfv 1673 . . . . . . . . . . . . 13  |-  F/ b  h  e.  ran  l
4038, 39nfan 1861 . . . . . . . . . . . 12  |-  F/ b ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  h  e.  ran  l )
41 simp3 990 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  /\  b  e.  ran  G  /\  ( l `  b )  =  h )  ->  ( l `  b )  =  h )
42 simp1ll 1051 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  /\  b  e.  ran  G  /\  ( l `  b )  =  h )  ->  ph )
43 simplrr 760 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  ->  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
44433ad2ant1 1009 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  /\  b  e.  ran  G  /\  ( l `  b )  =  h )  ->  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
45 simp2 989 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  /\  b  e.  ran  G  /\  ( l `  b )  =  h )  ->  b  e.  ran  G )
46 simp3 990 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
b  e.  ran  G
)
47 3simpc 987 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
( A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G ) )
48 simpr 461 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  b  e.  ran  G )  ->  b  e.  ran  G )
49 stoweidlem31.3 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ w ph
50 stoweidlem31.13 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  A  e.  _V )
51 rabexg 4440 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  e.  _V  ->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) }  e.  _V )
5250, 51syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  e.  _V )
5352a1d 25 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( w  e.  R  ->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  e.  _V ) )
5449, 53ralrimi 2795 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  A. w  e.  R  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  e.  _V )
555fnmpt 5535 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( A. w  e.  R  {
h  e.  A  | 
( A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
)  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) }  e.  _V  ->  G  Fn  R )
5654, 55syl 16 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  G  Fn  R )
5756adantr 465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  b  e.  ran  G )  ->  G  Fn  R )
58 fvelrnb 5737 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( G  Fn  R  ->  (
b  e.  ran  G  <->  E. u  e.  R  ( G `  u )  =  b ) )
59 nfmpt1 4379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  F/_ w
( w  e.  R  |->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )
605, 59nfcxfr 2574 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ w G
61 nfcv 2577 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ w u
6260, 61nffv 5696 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ w
( G `  u
)
63 nfcv 2577 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ w
b
6462, 63nfeq 2584 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ w
( G `  u
)  =  b
65 nfv 1673 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ u
( G `  w
)  =  b
66 fveq2 5689 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( u  =  w  ->  ( G `  u )  =  ( G `  w ) )
6766eqeq1d 2449 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( u  =  w  ->  (
( G `  u
)  =  b  <->  ( G `  w )  =  b ) )
6864, 65, 67cbvrex 2942 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. u  e.  R  ( G `  u )  =  b  <->  E. w  e.  R  ( G `  w )  =  b )
6958, 68syl6bb 261 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( G  Fn  R  ->  (
b  e.  ran  G  <->  E. w  e.  R  ( G `  w )  =  b ) )
7057, 69syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  b  e.  ran  G )  ->  (
b  e.  ran  G  <->  E. w  e.  R  ( G `  w )  =  b ) )
7148, 70mpbid 210 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  b  e.  ran  G )  ->  E. w  e.  R  ( G `  w )  =  b )
7260nfrn 5080 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ w ran  G
7372nfcri 2571 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ w  b  e.  ran  G
7449, 73nfan 1861 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ w
( ph  /\  b  e.  ran  G )
75 nfv 1673 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ w  b  =/=  (/)
76 simp3 990 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  ( G `  w )  =  b )
77 simpr 461 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  w  e.  R )  ->  w  e.  R )
7850adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  w  e.  R )  ->  A  e.  _V )
7978, 51syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  w  e.  R )  ->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) }  e.  _V )
805fvmpt2 5779 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( w  e.  R  /\  { h  e.  A  | 
( A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
)  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) }  e.  _V )  -> 
( G `  w
)  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } )
8177, 79, 80syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  w  e.  R )  ->  ( G `  w )  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )
827sselda 3354 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  w  e.  R )  ->  w  e.  V )
83 stoweidlem31.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  V  =  { w  e.  J  |  A. e  e.  RR+  E. h  e.  A  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  e  /\  A. t  e.  ( T  \  U ) ( 1  -  e
)  <  ( h `  t ) ) }
8483rabeq2i 2967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( w  e.  V  <->  ( w  e.  J  /\  A. e  e.  RR+  E. h  e.  A  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  e  /\  A. t  e.  ( T  \  U
) ( 1  -  e )  <  (
h `  t )
) ) )
8582, 84sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  w  e.  R )  ->  (
w  e.  J  /\  A. e  e.  RR+  E. h  e.  A  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  e  /\  A. t  e.  ( T  \  U
) ( 1  -  e )  <  (
h `  t )
) ) )
8685simprd 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  w  e.  R )  ->  A. e  e.  RR+  E. h  e.  A  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  e  /\  A. t  e.  ( T  \  U
) ( 1  -  e )  <  (
h `  t )
) )
87 stoweidlem31.10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  E  e.  RR+ )
88 stoweidlem31.8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  M  e.  NN )
8988nnrpd 11024 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  M  e.  RR+ )
9087, 89rpdivcld 11042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( E  /  M
)  e.  RR+ )
9190adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  w  e.  R )  ->  ( E  /  M )  e.  RR+ )
92 breq2 4294 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( e  =  ( E  /  M )  ->  (
( h `  t
)  <  e  <->  ( h `  t )  <  ( E  /  M ) ) )
9392ralbidv 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( e  =  ( E  /  M )  ->  ( A. t  e.  w  ( h `  t
)  <  e  <->  A. t  e.  w  ( h `  t )  <  ( E  /  M ) ) )
94 oveq2 6097 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( e  =  ( E  /  M )  ->  (
1  -  e )  =  ( 1  -  ( E  /  M
) ) )
9594breq1d 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( e  =  ( E  /  M )  ->  (
( 1  -  e
)  <  ( h `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( h `  t
) ) )
9695ralbidv 2733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( e  =  ( E  /  M )  ->  ( A. t  e.  ( T  \  U ) ( 1  -  e )  <  ( h `  t )  <->  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) )
9793, 963anbi23d 1292 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( e  =  ( E  /  M )  ->  (
( A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
)  /\  A. t  e.  w  ( h `  t )  <  e  /\  A. t  e.  ( T  \  U ) ( 1  -  e
)  <  ( h `  t ) )  <->  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) ) )
9897rexbidv 2734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( e  =  ( E  /  M )  ->  ( E. h  e.  A  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  e  /\  A. t  e.  ( T  \  U ) ( 1  -  e
)  <  ( h `  t ) )  <->  E. h  e.  A  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) ) )
9998rspccva 3070 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( A. e  e.  RR+  E. h  e.  A  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  e  /\  A. t  e.  ( T  \  U ) ( 1  -  e
)  <  ( h `  t ) )  /\  ( E  /  M
)  e.  RR+ )  ->  E. h  e.  A  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) )
10086, 91, 99syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  w  e.  R )  ->  E. h  e.  A  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) )
101 nfv 1673 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/ h  w  e.  R
10219, 101nfan 1861 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/ h
( ph  /\  w  e.  R )
103 nfcv 2577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/_ h (/)
10422, 103nfne 2701 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/ h { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  =/=  (/)
105 3simpc 987 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ph  /\  w  e.  R )  /\  h  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) )  ->  ( h  e.  A  /\  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) ) )
106 rabid 2895 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( h  e.  { h  e.  A  |  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  <->  ( h  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) ) )
107105, 106sylibr 212 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ph  /\  w  e.  R )  /\  h  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) )  ->  h  e.  {
h  e.  A  | 
( A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
)  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } )
108 ne0i 3641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( h  e.  { h  e.  A  |  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  ->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) }  =/=  (/) )
109107, 108syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ph  /\  w  e.  R )  /\  h  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) )  ->  { h  e.  A  |  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  =/=  (/) )
1101093exp 1186 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  w  e.  R )  ->  (
h  e.  A  -> 
( ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
)  ->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) }  =/=  (/) ) ) )
111102, 104, 110rexlimd 2836 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  w  e.  R )  ->  ( E. h  e.  A  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) )  ->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  =/=  (/) ) )
112100, 111mpd 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  w  e.  R )  ->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) }  =/=  (/) )
11381, 112eqnetrd 2624 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  w  e.  R )  ->  ( G `  w )  =/=  (/) )
1141133adant3 1008 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  ( G `  w )  =/=  (/) )
11576, 114eqnetrrd 2626 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  b  =/=  (/) )
1161153adant1r 1211 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  b  e.  ran  G )  /\  w  e.  R  /\  ( G `  w )  =  b )  -> 
b  =/=  (/) )
1171163exp 1186 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  b  e.  ran  G )  ->  (
w  e.  R  -> 
( ( G `  w )  =  b  ->  b  =/=  (/) ) ) )
11874, 75, 117rexlimd 2836 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  b  e.  ran  G )  ->  ( E. w  e.  R  ( G `  w )  =  b  ->  b  =/=  (/) ) )
11971, 118mpd 15 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  b  e.  ran  G )  ->  b  =/=  (/) )
1201193adant2 1007 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
b  =/=  (/) )
121 rsp 2774 . . . . . . . . . . . . . . . . . . 19  |-  ( A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  ->  (
b  e.  ran  G  ->  ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
122121imp 429 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  b  e.  ran  G )  -> 
( b  =/=  (/)  ->  (
l `  b )  e.  b ) )
12347, 120, 122sylc 60 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
( l `  b
)  e.  b )
12446, 123jca 532 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
( b  e.  ran  G  /\  ( l `  b )  e.  b ) )
125 vex 2973 . . . . . . . . . . . . . . . . . 18  |-  b  e. 
_V
1265elrnmpt 5084 . . . . . . . . . . . . . . . . . 18  |-  ( b  e.  _V  ->  (
b  e.  ran  G  <->  E. w  e.  R  b  =  { h  e.  A  |  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } ) )
127125, 126ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( b  e.  ran  G  <->  E. w  e.  R  b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )
12846, 127sylib 196 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  ->  E. w  e.  R  b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } )
129 nfv 1673 . . . . . . . . . . . . . . . . . 18  |-  F/ w
( l `  b
)  e.  b
13073, 129nfan 1861 . . . . . . . . . . . . . . . . 17  |-  F/ w
( b  e.  ran  G  /\  ( l `  b )  e.  b )
131 nfv 1673 . . . . . . . . . . . . . . . . 17  |-  F/ w
( l `  b
)  e.  Y
132 simp1r 1013 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( b  e.  ran  G  /\  ( l `  b )  e.  b )  /\  w  e.  R  /\  b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )  -> 
( l `  b
)  e.  b )
133 simp3 990 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( b  e.  ran  G  /\  ( l `  b )  e.  b )  /\  w  e.  R  /\  b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )  -> 
b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } )
134 simpl 457 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( l `  b
)  e.  b  /\  b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } )  ->  ( l `  b )  e.  b )
135 simpr 461 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( l `  b
)  e.  b  /\  b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } )  ->  b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )
136134, 135eleqtrd 2517 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( l `  b
)  e.  b  /\  b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } )  ->  ( l `  b )  e.  {
h  e.  A  | 
( A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
)  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } )
137 elrabi 3112 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( l `  b )  e.  { h  e.  A  |  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  ->  (
l `  b )  e.  A )
138 fveq1 5688 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( h  =  ( l `  b )  ->  (
h `  t )  =  ( ( l `
 b ) `  t ) )
139138breq2d 4302 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( h  =  ( l `  b )  ->  (
0  <_  ( h `  t )  <->  0  <_  ( ( l `  b
) `  t )
) )
140138breq1d 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( h  =  ( l `  b )  ->  (
( h `  t
)  <_  1  <->  ( (
l `  b ) `  t )  <_  1
) )
141139, 140anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  =  ( l `  b )  ->  (
( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  <-> 
( 0  <_  (
( l `  b
) `  t )  /\  ( ( l `  b ) `  t
)  <_  1 ) ) )
142141ralbidv 2733 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( h  =  ( l `  b )  ->  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  <->  A. t  e.  T  ( 0  <_  (
( l `  b
) `  t )  /\  ( ( l `  b ) `  t
)  <_  1 ) ) )
143138breq1d 4300 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  =  ( l `  b )  ->  (
( h `  t
)  <  ( E  /  M )  <->  ( (
l `  b ) `  t )  <  ( E  /  M ) ) )
144143ralbidv 2733 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( h  =  ( l `  b )  ->  ( A. t  e.  w  ( h `  t
)  <  ( E  /  M )  <->  A. t  e.  w  ( (
l `  b ) `  t )  <  ( E  /  M ) ) )
145138breq2d 4302 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  =  ( l `  b )  ->  (
( 1  -  ( E  /  M ) )  <  ( h `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( ( l `  b ) `  t
) ) )
146145ralbidv 2733 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( h  =  ( l `  b )  ->  ( A. t  e.  ( T  \  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t )  <->  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
( l `  b
) `  t )
) )
147142, 144, 1463anbi123d 1289 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( h  =  ( l `  b )  ->  (
( A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
)  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) )  <->  ( A. t  e.  T  (
0  <_  ( (
l `  b ) `  t )  /\  (
( l `  b
) `  t )  <_  1 )  /\  A. t  e.  w  (
( l `  b
) `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
( l `  b
) `  t )
) ) )
148147elrab 3115 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( l `  b )  e.  { h  e.  A  |  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  <->  ( (
l `  b )  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
( l `  b
) `  t )  /\  ( ( l `  b ) `  t
)  <_  1 )  /\  A. t  e.  w  ( ( l `
 b ) `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( ( l `
 b ) `  t ) ) ) )
149148simprbi 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( l `  b )  e.  { h  e.  A  |  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  ->  ( A. t  e.  T  ( 0  <_  (
( l `  b
) `  t )  /\  ( ( l `  b ) `  t
)  <_  1 )  /\  A. t  e.  w  ( ( l `
 b ) `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( ( l `
 b ) `  t ) ) )
150149simp1d 1000 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( l `  b )  e.  { h  e.  A  |  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  ->  A. t  e.  T  ( 0  <_  ( ( l `
 b ) `  t )  /\  (
( l `  b
) `  t )  <_  1 ) )
151142elrab 3115 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( l `  b )  e.  { h  e.  A  |  A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) }  <->  ( (
l `  b )  e.  A  /\  A. t  e.  T  ( 0  <_  ( ( l `
 b ) `  t )  /\  (
( l `  b
) `  t )  <_  1 ) ) )
152137, 150, 151sylanbrc 664 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( l `  b )  e.  { h  e.  A  |  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  ->  (
l `  b )  e.  { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) } )
153136, 152syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( l `  b
)  e.  b  /\  b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } )  ->  ( l `  b )  e.  {
h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) } )
154 stoweidlem31.4 . . . . . . . . . . . . . . . . . . . 20  |-  Y  =  { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }
155153, 154syl6eleqr 2532 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( l `  b
)  e.  b  /\  b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } )  ->  ( l `  b )  e.  Y
)
156132, 133, 155syl2anc 661 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( b  e.  ran  G  /\  ( l `  b )  e.  b )  /\  w  e.  R  /\  b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )  -> 
( l `  b
)  e.  Y )
1571563exp 1186 . . . . . . . . . . . . . . . . 17  |-  ( ( b  e.  ran  G  /\  ( l `  b
)  e.  b )  ->  ( w  e.  R  ->  ( b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  ->  (
l `  b )  e.  Y ) ) )
158130, 131, 157rexlimd 2836 . . . . . . . . . . . . . . . 16  |-  ( ( b  e.  ran  G  /\  ( l `  b
)  e.  b )  ->  ( E. w  e.  R  b  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  ->  (
l `  b )  e.  Y ) )
159124, 128, 158sylc 60 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
( l `  b
)  e.  Y )
16042, 44, 45, 159syl3anc 1218 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  /\  b  e.  ran  G  /\  ( l `  b )  =  h )  ->  ( l `  b )  e.  Y
)
16141, 160eqeltrrd 2516 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  /\  b  e.  ran  G  /\  ( l `  b )  =  h )  ->  h  e.  Y )
1621613exp 1186 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  ->  (
b  e.  ran  G  ->  ( ( l `  b )  =  h  ->  h  e.  Y
) ) )
16340, 162reximdai 2822 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  ->  ( E. b  e.  ran  G ( l `  b
)  =  h  ->  E. b  e.  ran  G  h  e.  Y ) )
16433, 163mpd 15 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  ->  E. b  e.  ran  G  h  e.  Y )
165 nfv 1673 . . . . . . . . . . 11  |-  F/ b  h  e.  Y
166 idd 24 . . . . . . . . . . . 12  |-  ( b  e.  ran  G  -> 
( h  e.  Y  ->  h  e.  Y ) )
167166a1i 11 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  ->  (
b  e.  ran  G  ->  ( h  e.  Y  ->  h  e.  Y ) ) )
16840, 165, 167rexlimd 2836 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  ->  ( E. b  e.  ran  G  h  e.  Y  ->  h  e.  Y )
)
169164, 168mpd 15 . . . . . . . . 9  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  ->  h  e.  Y )
170169ex 434 . . . . . . . 8  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( h  e. 
ran  l  ->  h  e.  Y ) )
17130, 170ralrimi 2795 . . . . . . 7  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  A. h  e.  ran  l  h  e.  Y
)
172 dfss3 3344 . . . . . . . 8  |-  ( ran  l  C_  Y  <->  A. z  e.  ran  l  z  e.  Y )
173 nfrab1 2899 . . . . . . . . . . 11  |-  F/_ h { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }
174154, 173nfcxfr 2574 . . . . . . . . . 10  |-  F/_ h Y
175174nfcri 2571 . . . . . . . . 9  |-  F/ h  z  e.  Y
176 nfv 1673 . . . . . . . . 9  |-  F/ z  h  e.  Y
177 eleq1 2501 . . . . . . . . 9  |-  ( z  =  h  ->  (
z  e.  Y  <->  h  e.  Y ) )
178175, 176, 177cbvral 2941 . . . . . . . 8  |-  ( A. z  e.  ran  l  z  e.  Y  <->  A. h  e.  ran  l  h  e.  Y )
179172, 178bitri 249 . . . . . . 7  |-  ( ran  l  C_  Y  <->  A. h  e.  ran  l  h  e.  Y )
180171, 179sylibr 212 . . . . . 6  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ran  l  C_  Y )
181 df-f 5420 . . . . . 6  |-  ( l : ran  G --> Y  <->  ( l  Fn  ran  G  /\  ran  l  C_  Y ) )
18218, 180, 181sylanbrc 664 . . . . 5  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  l : ran  G --> Y )
183 dffn3 5564 . . . . . . . 8  |-  ( G  Fn  R  <->  G : R
--> ran  G )
18456, 183sylib 196 . . . . . . 7  |-  ( ph  ->  G : R --> ran  G
)
185184adantr 465 . . . . . 6  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  G : R --> ran  G )
186 stoweidlem31.9 . . . . . . . 8  |-  ( ph  ->  v : ( 1 ... M ) -1-1-onto-> R )
187 f1of 5639 . . . . . . . 8  |-  ( v : ( 1 ... M ) -1-1-onto-> R  ->  v :
( 1 ... M
) --> R )
188186, 187syl 16 . . . . . . 7  |-  ( ph  ->  v : ( 1 ... M ) --> R )
189188adantr 465 . . . . . 6  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  v : ( 1 ... M ) --> R )
190 fco 5566 . . . . . 6  |-  ( ( G : R --> ran  G  /\  v : ( 1 ... M ) --> R )  ->  ( G  o.  v ) : ( 1 ... M ) --> ran  G )
191185, 189, 190syl2anc 661 . . . . 5  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( G  o.  v ) : ( 1 ... M ) --> ran  G )
192 fco 5566 . . . . 5  |-  ( ( l : ran  G --> Y  /\  ( G  o.  v ) : ( 1 ... M ) --> ran  G )  -> 
( l  o.  ( G  o.  v )
) : ( 1 ... M ) --> Y )
193182, 191, 192syl2anc 661 . . . 4  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( l  o.  ( G  o.  v
) ) : ( 1 ... M ) --> Y )
194 fvco3 5766 . . . . . . . . 9  |-  ( ( ( G  o.  v
) : ( 1 ... M ) --> ran 
G  /\  i  e.  ( 1 ... M
) )  ->  (
( l  o.  ( G  o.  v )
) `  i )  =  ( l `  ( ( G  o.  v ) `  i
) ) )
195191, 194sylan 471 . . . . . . . 8  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( (
l  o.  ( G  o.  v ) ) `
 i )  =  ( l `  (
( G  o.  v
) `  i )
) )
196 simpll 753 . . . . . . . . 9  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ph )
197 simplrr 760 . . . . . . . . 9  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
198191fnvinran 29733 . . . . . . . . 9  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( ( G  o.  v ) `  i )  e.  ran  G )
199 simp3 990 . . . . . . . . . 10  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  ( ( G  o.  v ) `
 i )  e. 
ran  G )  -> 
( ( G  o.  v ) `  i
)  e.  ran  G
)
200 nfv 1673 . . . . . . . . . . . . 13  |-  F/ b ( ( G  o.  v ) `  i
)  e.  ran  G
20134, 36, 200nf3an 1863 . . . . . . . . . . . 12  |-  F/ b ( ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  (
( G  o.  v
) `  i )  e.  ran  G )
202 nfv 1673 . . . . . . . . . . . 12  |-  F/ b ( l `  (
( G  o.  v
) `  i )
)  e.  ( ( G  o.  v ) `
 i )
203201, 202nfim 1853 . . . . . . . . . . 11  |-  F/ b ( ( ph  /\  A. b  e.  ran  G
( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  (
( G  o.  v
) `  i )  e.  ran  G )  -> 
( l `  (
( G  o.  v
) `  i )
)  e.  ( ( G  o.  v ) `
 i ) )
204 eleq1 2501 . . . . . . . . . . . . 13  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
b  e.  ran  G  <->  ( ( G  o.  v
) `  i )  e.  ran  G ) )
2052043anbi3d 1295 . . . . . . . . . . . 12  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
( ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  <->  ( ph  /\ 
A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  (
( G  o.  v
) `  i )  e.  ran  G ) ) )
206 fveq2 5689 . . . . . . . . . . . . 13  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
l `  b )  =  ( l `  ( ( G  o.  v ) `  i
) ) )
207 id 22 . . . . . . . . . . . . 13  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  b  =  ( ( G  o.  v ) `  i ) )
208206, 207eleq12d 2509 . . . . . . . . . . . 12  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
( l `  b
)  e.  b  <->  ( l `  ( ( G  o.  v ) `  i
) )  e.  ( ( G  o.  v
) `  i )
) )
209205, 208imbi12d 320 . . . . . . . . . . 11  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
( ( ph  /\  A. b  e.  ran  G
( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  b  e.  ran  G )  -> 
( l `  b
)  e.  b )  <-> 
( ( ph  /\  A. b  e.  ran  G
( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  (
( G  o.  v
) `  i )  e.  ran  G )  -> 
( l `  (
( G  o.  v
) `  i )
)  e.  ( ( G  o.  v ) `
 i ) ) ) )
210203, 209, 123vtoclg1f 3027 . . . . . . . . . 10  |-  ( ( ( G  o.  v
) `  i )  e.  ran  G  ->  (
( ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  ( ( G  o.  v ) `
 i )  e. 
ran  G )  -> 
( l `  (
( G  o.  v
) `  i )
)  e.  ( ( G  o.  v ) `
 i ) ) )
211199, 210mpcom 36 . . . . . . . . 9  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  ( ( G  o.  v ) `
 i )  e. 
ran  G )  -> 
( l `  (
( G  o.  v
) `  i )
)  e.  ( ( G  o.  v ) `
 i ) )
212196, 197, 198, 211syl3anc 1218 . . . . . . . 8  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( l `  ( ( G  o.  v ) `  i
) )  e.  ( ( G  o.  v
) `  i )
)
213195, 212eqeltrd 2515 . . . . . . 7  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( (
l  o.  ( G  o.  v ) ) `
 i )  e.  ( ( G  o.  v ) `  i
) )
214 fvco3 5766 . . . . . . . . . . . 12  |-  ( ( v : ( 1 ... M ) --> R  /\  i  e.  ( 1 ... M ) )  ->  ( ( G  o.  v ) `  i )  =  ( G `  ( v `
 i ) ) )
215188, 214sylan 471 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( G  o.  v
) `  i )  =  ( G `  ( v `  i
) ) )
216188fnvinran 29733 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
v `  i )  e.  R )
21750adantr 465 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  A  e.  _V )
218 rabexg 4440 . . . . . . . . . . . . 13  |-  ( A  e.  _V  ->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  ( v `  i
) ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) }  e.  _V )
219217, 218syl 16 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  ( v `  i
) ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) }  e.  _V )
220 raleq 2915 . . . . . . . . . . . . . . 15  |-  ( w  =  ( v `  i )  ->  ( A. t  e.  w  ( h `  t
)  <  ( E  /  M )  <->  A. t  e.  ( v `  i
) ( h `  t )  <  ( E  /  M ) ) )
2212203anbi2d 1294 . . . . . . . . . . . . . 14  |-  ( w  =  ( v `  i )  ->  (
( A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
)  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) )  <->  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  ( v `  i ) ( h `
 t )  < 
( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) ) )
222221rabbidv 2962 . . . . . . . . . . . . 13  |-  ( w  =  ( v `  i )  ->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) }  =  { h  e.  A  |  ( A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  ( v `  i ) ( h `
 t )  < 
( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )
223222, 5fvmptg 5770 . . . . . . . . . . . 12  |-  ( ( ( v `  i
)  e.  R  /\  { h  e.  A  | 
( A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
)  /\  A. t  e.  ( v `  i
) ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) }  e.  _V )  -> 
( G `  (
v `  i )
)  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  /\  A. t  e.  ( v `  i
) ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } )
224216, 219, 223syl2anc 661 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  ( G `  ( v `  i ) )  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  ( v `  i ) ( h `
 t )  < 
( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )
225215, 224eqtrd 2473 . . . . . . . . . 10  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( G  o.  v
) `  i )  =  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  ( v `  i ) ( h `
 t )  < 
( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )
226225adantlr 714 . . . . . . . . 9  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( ( G  o.  v ) `  i )  =  {
h  e.  A  | 
( A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
)  /\  A. t  e.  ( v `  i
) ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } )
227226eleq2d 2508 . . . . . . . 8  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( (
( l  o.  ( G  o.  v )
) `  i )  e.  ( ( G  o.  v ) `  i
)  <->  ( ( l  o.  ( G  o.  v ) ) `  i )  e.  {
h  e.  A  | 
( A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
)  /\  A. t  e.  ( v `  i
) ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) ) } ) )
228 nfcv 2577 . . . . . . . . . . . . . 14  |-  F/_ h
v
22924, 228nfco 5003 . . . . . . . . . . . . 13  |-  F/_ h
( G  o.  v
)
23020, 229nfco 5003 . . . . . . . . . . . 12  |-  F/_ h
( l  o.  ( G  o.  v )
)
231 nfcv 2577 . . . . . . . . . . . 12  |-  F/_ h
i
232230, 231nffv 5696 . . . . . . . . . . 11  |-  F/_ h
( ( l  o.  ( G  o.  v
) ) `  i
)
233 nfcv 2577 . . . . . . . . . . 11  |-  F/_ h A
234 nfcv 2577 . . . . . . . . . . . . 13  |-  F/_ h T
235 nfcv 2577 . . . . . . . . . . . . . . 15  |-  F/_ h
0
236 nfcv 2577 . . . . . . . . . . . . . . 15  |-  F/_ h  <_
237 nfcv 2577 . . . . . . . . . . . . . . . 16  |-  F/_ h
t
238232, 237nffv 5696 . . . . . . . . . . . . . . 15  |-  F/_ h
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)
239235, 236, 238nfbr 4334 . . . . . . . . . . . . . 14  |-  F/ h
0  <_  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )
240 nfcv 2577 . . . . . . . . . . . . . . 15  |-  F/_ h
1
241238, 236, 240nfbr 4334 . . . . . . . . . . . . . 14  |-  F/ h
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1
242239, 241nfan 1861 . . . . . . . . . . . . 13  |-  F/ h
( 0  <_  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )  /\  ( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1 )
243234, 242nfral 2767 . . . . . . . . . . . 12  |-  F/ h A. t  e.  T  ( 0  <_  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )  /\  ( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1 )
244 nfcv 2577 . . . . . . . . . . . . 13  |-  F/_ h
( v `  i
)
245 nfcv 2577 . . . . . . . . . . . . . 14  |-  F/_ h  <
246 nfcv 2577 . . . . . . . . . . . . . 14  |-  F/_ h
( E  /  M
)
247238, 245, 246nfbr 4334 . . . . . . . . . . . . 13  |-  F/ h
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <  ( E  /  M )
248244, 247nfral 2767 . . . . . . . . . . . 12  |-  F/ h A. t  e.  (
v `  i )
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <  ( E  /  M )
249 nfcv 2577 . . . . . . . . . . . . 13  |-  F/_ h
( T  \  U
)
250 nfcv 2577 . . . . . . . . . . . . . 14  |-  F/_ h
( 1  -  ( E  /  M ) )
251250, 245, 238nfbr 4334 . . . . . . . . . . . . 13  |-  F/ h
( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )
252249, 251nfral 2767 . . . . . . . . . . . 12  |-  F/ h A. t  e.  ( T  \  U ) ( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )
253243, 248, 252nf3an 1863 . . . . . . . . . . 11  |-  F/ h
( A. t  e.  T  ( 0  <_ 
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  /\  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )  <_  1
)  /\  A. t  e.  ( v `  i
) ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t ) )
254 nfcv 2577 . . . . . . . . . . . . . 14  |-  F/_ t
h
255 nfcv 2577 . . . . . . . . . . . . . . . 16  |-  F/_ t
l
256 nfcv 2577 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t R
257 nfra1 2764 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ t A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )
258 nfra1 2764 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ t A. t  e.  w  ( h `  t
)  <  ( E  /  M )
259 nfra1 2764 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ t A. t  e.  ( T  \  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t )
260257, 258, 259nf3an 1863 . . . . . . . . . . . . . . . . . . . 20  |-  F/ t ( A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
)  /\  A. t  e.  w  ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) )
261 nfcv 2577 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ t A
262260, 261nfrab 2900 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }
263256, 262nfmpt 4378 . . . . . . . . . . . . . . . . . 18  |-  F/_ t
( w  e.  R  |->  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  w  (
h `  t )  <  ( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) } )
2645, 263nfcxfr 2574 . . . . . . . . . . . . . . . . 17  |-  F/_ t G
265 nfcv 2577 . . . . . . . . . . . . . . . . 17  |-  F/_ t
v
266264, 265nfco 5003 . . . . . . . . . . . . . . . 16  |-  F/_ t
( G  o.  v
)
267255, 266nfco 5003 . . . . . . . . . . . . . . 15  |-  F/_ t
( l  o.  ( G  o.  v )
)
268 nfcv 2577 . . . . . . . . . . . . . . 15  |-  F/_ t
i
269267, 268nffv 5696 . . . . . . . . . . . . . 14  |-  F/_ t
( ( l  o.  ( G  o.  v
) ) `  i
)
270254, 269nfeq 2584 . . . . . . . . . . . . 13  |-  F/ t  h  =  ( ( l  o.  ( G  o.  v ) ) `
 i )
271 fveq1 5688 . . . . . . . . . . . . . . 15  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
h `  t )  =  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t ) )
272271breq2d 4302 . . . . . . . . . . . . . 14  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
0  <_  ( h `  t )  <->  0  <_  ( ( ( l  o.  ( G  o.  v
) ) `  i
) `  t )
) )
273271breq1d 4300 . . . . . . . . . . . . . 14  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
( h `  t
)  <_  1  <->  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )  <_  1
) )
274272, 273anbi12d 710 . . . . . . . . . . . . 13  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  <-> 
( 0  <_  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )  /\  ( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1 ) ) )
275270, 274ralbid 2731 . . . . . . . . . . . 12  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  ( A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  <->  A. t  e.  T  ( 0  <_  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )  /\  ( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1 ) ) )
276271breq1d 4300 . . . . . . . . . . . . 13  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
( h `  t
)  <  ( E  /  M )  <->  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )  <  ( E  /  M ) ) )
277270, 276ralbid 2731 . . . . . . . . . . . 12  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  ( A. t  e.  (
v `  i )
( h `  t
)  <  ( E  /  M )  <->  A. t  e.  ( v `  i
) ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )  <  ( E  /  M ) ) )
278271breq2d 4302 . . . . . . . . . . . . 13  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
( 1  -  ( E  /  M ) )  <  ( h `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
) ) )
279270, 278ralbid 2731 . . . . . . . . . . . 12  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  ( A. t  e.  ( T  \  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t )  <->  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )
) )
280275, 277, 2793anbi123d 1289 . . . . . . . . . . 11  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
( A. t  e.  T  ( 0  <_ 
( h `  t
)  /\  ( h `  t )  <_  1
)  /\  A. t  e.  ( v `  i
) ( h `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t ) )  <->  ( A. t  e.  T  (
0  <_  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )  /\  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )  <_  1 )  /\  A. t  e.  ( v `  i ) ( ( ( l  o.  ( G  o.  v )
) `  i ) `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t ) ) ) )
281232, 233, 253, 280elrabf 3113 . . . . . . . . . 10  |-  ( ( ( l  o.  ( G  o.  v )
) `  i )  e.  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  ( v `  i ) ( h `
 t )  < 
( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  <->  ( (
( l  o.  ( G  o.  v )
) `  i )  e.  A  /\  ( A. t  e.  T  ( 0  <_  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )  /\  ( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1 )  /\  A. t  e.  ( v `  i
) ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t ) ) ) )
282281simprbi 464 . . . . . . . . 9  |-  ( ( ( l  o.  ( G  o.  v )
) `  i )  e.  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  ( v `  i ) ( h `
 t )  < 
( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  ->  ( A. t  e.  T  ( 0  <_  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )  /\  ( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1 )  /\  A. t  e.  ( v `  i
) ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )  <  ( E  /  M )  /\  A. t  e.  ( T 
\  U ) ( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t ) ) )
283282simp2d 1001 . . . . . . . 8  |-  ( ( ( l  o.  ( G  o.  v )
) `  i )  e.  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  ( v `  i ) ( h `
 t )  < 
( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  ->  A. t  e.  ( v `  i
) ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )  <  ( E  /  M ) )
284227, 283syl6bi 228 . . . . . . 7  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( (
( l  o.  ( G  o.  v )
) `  i )  e.  ( ( G  o.  v ) `  i
)  ->  A. t  e.  ( v `  i
) ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )  <  ( E  /  M ) ) )
285213, 284mpd 15 . . . . . 6  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  A. t  e.  ( v `  i
) ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )  <  ( E  /  M ) )
286 stoweidlem31.2 . . . . . . . . 9  |-  F/ t
ph
287264nfrn 5080 . . . . . . . . . . 11  |-  F/_ t ran  G
288255, 287nffn 5505 . . . . . . . . . 10  |-  F/ t  l  Fn  ran  G
289 nfv 1673 . . . . . . . . . . 11  |-  F/ t ( b  =/=  (/)  ->  (
l `  b )  e.  b )
290287, 289nfral 2767 . . . . . . . . . 10  |-  F/ t A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )
291288, 290nfan 1861 . . . . . . . . 9  |-  F/ t ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
292286, 291nfan 1861 . . . . . . . 8  |-  F/ t ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
293 nfv 1673 . . . . . . . 8  |-  F/ t  i  e.  ( 1 ... M )
294292, 293nfan 1861 . . . . . . 7  |-  F/ t ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )
295 stoweidlem31.11 . . . . . . . . . . 11  |-  ( ph  ->  B  C_  ( T  \  U ) )
296295ad3antrrr 729 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  /\  t  e.  B
)  ->  B  C_  ( T  \  U ) )
297 simpr 461 . . . . . . . . . 10  |-  ( ( ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  /\  t  e.  B
)  ->  t  e.  B )
298296, 297sseldd 3355 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  /\  t  e.  B
)  ->  t  e.  ( T  \  U ) )
299282simp3d 1002 . . . . . . . . . . . 12  |-  ( ( ( l  o.  ( G  o.  v )
) `  i )  e.  { h  e.  A  |  ( A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 )  /\  A. t  e.  ( v `  i ) ( h `
 t )  < 
( E  /  M
)  /\  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) }  ->  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )
)
300227, 299syl6bi 228 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( (
( l  o.  ( G  o.  v )
) `  i )  e.  ( ( G  o.  v ) `  i
)  ->  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )
) )
301213, 300mpd 15 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )
)
302301r19.21bi 2812 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  /\  t  e.  ( T  \  U ) )  ->  ( 1  -  ( E  /  M ) )  < 
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
) )
303298, 302syldan 470 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  /\  t  e.  B
)  ->  ( 1  -  ( E  /  M ) )  < 
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
) )
304303ex 434 . . . . . . 7  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( t  e.  B  ->  ( 1  -  ( E  /  M ) )  < 
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
) ) )
305294, 304ralrimi 2795 . . . . . 6  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  A. t  e.  B  ( 1  -  ( E  /  M ) )  < 
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
) )
306285, 305jca 532 . . . . 5  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( A. t  e.  ( v `  i ) ( ( ( l  o.  ( G  o.  v )
) `  i ) `  t )  <  ( E  /  M )  /\  A. t  e.  B  ( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t ) ) )
307306ralrimiva 2797 . . . 4  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  A. i  e.  ( 1 ... M ) ( A. t  e.  ( v `  i
) ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )  <  ( E  /  M )  /\  A. t  e.  B  ( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t ) ) )
308193, 307jca 532 . . 3  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( ( l  o.  ( G  o.  v ) ) : ( 1 ... M
) --> Y  /\  A. i  e.  ( 1 ... M ) ( A. t  e.  ( v `  i ) ( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <  ( E  /  M )  /\  A. t  e.  B  (
1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t ) ) ) )
309 feq1 5540 . . . . 5  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
x : ( 1 ... M ) --> Y  <-> 
( l  o.  ( G  o.  v )
) : ( 1 ... M ) --> Y ) )
310 nfcv 2577 . . . . . . . . 9  |-  F/_ t
x
311310, 267nfeq 2584 . . . . . . . 8  |-  F/ t  x  =  ( l  o.  ( G  o.  v ) )
312 fveq1 5688 . . . . . . . . . 10  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
x `  i )  =  ( ( l  o.  ( G  o.  v ) ) `  i ) )
313312fveq1d 5691 . . . . . . . . 9  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
( x `  i
) `  t )  =  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t ) )
314313breq1d 4300 . . . . . . . 8  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
( ( x `  i ) `  t
)  <  ( E  /  M )  <->  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )  <  ( E  /  M ) ) )
315311, 314ralbid 2731 . . . . . . 7  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  ( A. t  e.  (
v `  i )
( ( x `  i ) `  t
)  <  ( E  /  M )  <->  A. t  e.  ( v `  i
) ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )  <  ( E  /  M ) ) )
316313breq2d 4302 . . . . . . . 8  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
( 1  -  ( E  /  M ) )  <  ( ( x `
 i ) `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
) ) )
317311, 316ralbid 2731 . . . . . . 7  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  ( A. t  e.  B  ( 1  -  ( E  /  M ) )  <  ( ( x `
 i ) `  t )  <->  A. t  e.  B  ( 1  -  ( E  /  M ) )  < 
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
) ) )
318315, 317anbi12d 710 . . . . . 6  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
( A. t  e.  ( v `  i
) ( ( x `
 i ) `  t )