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

Theorem stoweidlem31 27647
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 27567 . . 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 2919 . . . . 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 4310 . . . . . . . 8  |-  ( ph  ->  R  e.  _V )
9 mptexg 5924 . . . . . . . 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 2488 . . . . . 6  |-  ( ph  ->  G  e.  _V )
12 vex 2919 . . . . . 6  |-  v  e. 
_V
13 coexg 5371 . . . . . 6  |-  ( ( G  e.  _V  /\  v  e.  _V )  ->  ( G  o.  v
)  e.  _V )
1411, 12, 13sylancl 644 . . . . 5  |-  ( ph  ->  ( G  o.  v
)  e.  _V )
15 coexg 5371 . . . . 5  |-  ( ( l  e.  _V  /\  ( G  o.  v
)  e.  _V )  ->  ( l  o.  ( G  o.  v )
)  e.  _V )
164, 14, 15sylancr 645 . . . 4  |-  ( ph  ->  ( l  o.  ( G  o.  v )
)  e.  _V )
1716adantr 452 . . 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 733 . . . . . 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 2540 . . . . . . . . . . 11  |-  F/_ h
l
21 nfcv 2540 . . . . . . . . . . . . . 14  |-  F/_ h R
22 nfrab1 2848 . . . . . . . . . . . . . 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 4257 . . . . . . . . . . . . 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 2537 . . . . . . . . . . . 12  |-  F/_ h G
2524nfrn 5071 . . . . . . . . . . 11  |-  F/_ h ran  G
2620, 25nffn 5500 . . . . . . . . . 10  |-  F/ h  l  Fn  ran  G
27 nfv 1626 . . . . . . . . . . 11  |-  F/ h
( b  =/=  (/)  ->  (
l `  b )  e.  b )
2825, 27nfral 2719 . . . . . . . . . 10  |-  F/ h A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )
2926, 28nfan 1842 . . . . . . . . 9  |-  F/ h
( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
3019, 29nfan 1842 . . . . . . . 8  |-  F/ h
( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
31 fvelrnb 5733 . . . . . . . . . . . . 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 471 . . . . . . . . . . 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 1626 . . . . . . . . . . . . . 14  |-  F/ b
ph
35 nfv 1626 . . . . . . . . . . . . . . 15  |-  F/ b  l  Fn  ran  G
36 nfra1 2716 . . . . . . . . . . . . . . 15  |-  F/ b A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )
3735, 36nfan 1842 . . . . . . . . . . . . . 14  |-  F/ b ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
3834, 37nfan 1842 . . . . . . . . . . . . 13  |-  F/ b ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
39 nfv 1626 . . . . . . . . . . . . 13  |-  F/ b  h  e.  ran  l
4038, 39nfan 1842 . . . . . . . . . . . 12  |-  F/ b ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  h  e.  ran  l )
41 simp3 959 . . . . . . . . . . . . . 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 1020 . . . . . . . . . . . . . . 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 738 . . . . . . . . . . . . . . . 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 978 . . . . . . . . . . . . . . 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 958 . . . . . . . . . . . . . . 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 959 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
b  e.  ran  G
)
47 3simpc 956 . . . . . . . . . . . . . . . . . 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 448 . . . . . . . . . . . . . . . . . . . . 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 4313 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 23 . . . . . . . . . . . . . . . . . . . . . . . . 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 2747 . . . . . . . . . . . . . . . . . . . . . . . 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 5530 . . . . . . . . . . . . . . . . . . . . . . . 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 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  b  e.  ran  G )  ->  G  Fn  R )
58 fvelrnb 5733 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( G  Fn  R  ->  (
b  e.  ran  G  <->  E. u  e.  R  ( G `  u )  =  b ) )
59 nfmpt1 4258 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2537 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ w G
61 nfcv 2540 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ w u
6260, 61nffv 5694 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ w
( G `  u
)
63 nfcv 2540 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ w
b
6462, 63nfeq 2547 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ w
( G `  u
)  =  b
65 nfv 1626 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ u
( G `  w
)  =  b
66 fveq2 5687 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( u  =  w  ->  ( G `  u )  =  ( G `  w ) )
6766eqeq1d 2412 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( u  =  w  ->  (
( G `  u
)  =  b  <->  ( G `  w )  =  b ) )
6864, 65, 67cbvrex 2889 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. u  e.  R  ( G `  u )  =  b  <->  E. w  e.  R  ( G `  w )  =  b )
6958, 68syl6bb 253 . . . . . . . . . . . . . . . . . . . . . 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 202 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  b  e.  ran  G )  ->  E. w  e.  R  ( G `  w )  =  b )
7260nfrn 5071 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ w ran  G
7372nfcri 2534 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ w  b  e.  ran  G
7449, 73nfan 1842 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ w
( ph  /\  b  e.  ran  G )
75 nfv 1626 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ w  b  =/=  (/)
76 simp3 959 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  ( G `  w )  =  b )
77 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  w  e.  R )  ->  w  e.  R )
7850adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5771 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3308 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2913 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  M  e.  RR+ )
9087, 89rpdivcld 10621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( E  /  M
)  e.  RR+ )
9190adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  w  e.  R )  ->  ( E  /  M )  e.  RR+ )
92 breq2 4176 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( e  =  ( E  /  M )  ->  (
( h `  t
)  <  e  <->  ( h `  t )  <  ( E  /  M ) ) )
9392ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( e  =  ( E  /  M )  ->  ( A. t  e.  w  ( h `  t
)  <  e  <->  A. t  e.  w  ( h `  t )  <  ( E  /  M ) ) )
94 oveq2 6048 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( e  =  ( E  /  M )  ->  (
1  -  e )  =  ( 1  -  ( E  /  M
) ) )
9594breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( e  =  ( E  /  M )  ->  (
( 1  -  e
)  <  ( h `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( h `  t
) ) )
9695ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1257 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2687 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3011 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1626 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/ h  w  e.  R
10219, 101nfan 1842 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/ h
( ph  /\  w  e.  R )
103 nfcv 2540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/_ h (/)
10422, 103nfne 2658 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3594 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1152 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2787 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2585 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  w  e.  R )  ->  ( G `  w )  =/=  (/) )
1141133adant3 977 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  ( G `  w )  =/=  (/) )
11576, 114eqnetrrd 2587 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  b  =/=  (/) )
1161153adant1r 1177 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  b  e.  ran  G )  /\  w  e.  R  /\  ( G `  w )  =  b )  -> 
b  =/=  (/) )
1171163exp 1152 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  b  e.  ran  G )  ->  (
w  e.  R  -> 
( ( G `  w )  =  b  ->  b  =/=  (/) ) ) )
11874, 75, 117rexlimd 2787 . . . . . . . . . . . . . . . . . . . 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 976 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
b  =/=  (/) )
121 rsp 2726 . . . . . . . . . . . . . . . . . . 19  |-  ( A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  ->  (
b  e.  ran  G  ->  ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
122121imp 419 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  b  e.  ran  G )  -> 
( b  =/=  (/)  ->  (
l `  b )  e.  b ) )
12347, 120, 122sylc 58 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
( l `  b
)  e.  b )
12446, 123jca 519 . . . . . . . . . . . . . . . 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 2919 . . . . . . . . . . . . . . . . . 18  |-  b  e. 
_V
1265elrnmpt 5076 . . . . . . . . . . . . . . . . . 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 8 . . . . . . . . . . . . . . . . 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 189 . . . . . . . . . . . . . . . 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 1626 . . . . . . . . . . . . . . . . . 18  |-  F/ w
( l `  b
)  e.  b
13073, 129nfan 1842 . . . . . . . . . . . . . . . . 17  |-  F/ w
( b  e.  ran  G  /\  ( l `  b )  e.  b )
131 nfv 1626 . . . . . . . . . . . . . . . . 17  |-  F/ w
( l `  b
)  e.  Y
132 simp1r 982 . . . . . . . . . . . . . . . . . . 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 959 . . . . . . . . . . . . . . . . . . 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 444 . . . . . . . . . . . . . . . . . . . . . 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 448 . . . . . . . . . . . . . . . . . . . . . 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 2480 . . . . . . . . . . . . . . . . . . . . 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 3050 . . . . . . . . . . . . . . . . . . . . . 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 5686 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( h  =  ( l `  b )  ->  (
h `  t )  =  ( ( l `
 b ) `  t ) )
139138breq2d 4184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( h  =  ( l `  b )  ->  (
0  <_  ( h `  t )  <->  0  <_  ( ( l `  b
) `  t )
) )
140138breq1d 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( h  =  ( l `  b )  ->  (
( h `  t
)  <_  1  <->  ( (
l `  b ) `  t )  <_  1
) )
141139, 140anbi12d 692 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  =  ( l `  b )  ->  (
( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  <-> 
( 0  <_  (
( l `  b
) `  t )  /\  ( ( l `  b ) `  t
)  <_  1 ) ) )
142141ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . 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 4182 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  =  ( l `  b )  ->  (
( h `  t
)  <  ( E  /  M )  <->  ( (
l `  b ) `  t )  <  ( E  /  M ) ) )
144143ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( h  =  ( l `  b )  ->  ( A. t  e.  w  ( h `  t
)  <  ( E  /  M )  <->  A. t  e.  w  ( (
l `  b ) `  t )  <  ( E  /  M ) ) )
145138breq2d 4184 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  =  ( l `  b )  ->  (
( 1  -  ( E  /  M ) )  <  ( h `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( ( l `  b ) `  t
) ) )
146145ralbidv 2686 . . . . . . . . . . . . . . . . . . . . . . . . . 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 1254 . . . . . . . . . . . . . . . . . . . . . . . . 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 3052 . . . . . . . . . . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . . . . . . . . . . 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 969 . . . . . . . . . . . . . . . . . . . . . 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 3052 . . . . . . . . . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . . . . . . . . . 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 2495 . . . . . . . . . . . . . . . . . . 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 643 . . . . . . . . . . . . . . . . . 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 1152 . . . . . . . . . . . . . . . . 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 2787 . . . . . . . . . . . . . . . 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 58 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
( l `  b
)  e.  Y )
16042, 44, 45, 159syl3anc 1184 . . . . . . . . . . . . . 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 2479 . . . . . . . . . . . . 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 1152 . . . . . . . . . . . 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 2774 . . . . . . . . . . 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 1626 . . . . . . . . . . 11  |-  F/ b  h  e.  Y
166 idd 22 . . . . . . . . . . . 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 2787 . . . . . . . . . 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 424 . . . . . . . 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 2747 . . . . . . 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 3298 . . . . . . . 8  |-  ( ran  l  C_  Y  <->  A. z  e.  ran  l  z  e.  Y )
173 nfrab1 2848 . . . . . . . . . . 11  |-  F/_ h { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }
174154, 173nfcxfr 2537 . . . . . . . . . 10  |-  F/_ h Y
175174nfcri 2534 . . . . . . . . 9  |-  F/ h  z  e.  Y
176 nfv 1626 . . . . . . . . 9  |-  F/ z  h  e.  Y
177 eleq1 2464 . . . . . . . . 9  |-  ( z  =  h  ->  (
z  e.  Y  <->  h  e.  Y ) )
178175, 176, 177cbvral 2888 . . . . . . . 8  |-  ( A. z  e.  ran  l  z  e.  Y  <->  A. h  e.  ran  l  h  e.  Y )
179172, 178bitri 241 . . . . . . 7  |-  ( ran  l  C_  Y  <->  A. h  e.  ran  l  h  e.  Y )
180171, 179sylibr 204 . . . . . 6  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ran  l  C_  Y )
181 df-f 5417 . . . . . 6  |-  ( l : ran  G --> Y  <->  ( l  Fn  ran  G  /\  ran  l  C_  Y ) )
18218, 180, 181sylanbrc 646 . . . . 5  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  l : ran  G --> Y )
183 dffn3 5557 . . . . . . . 8  |-  ( G  Fn  R  <->  G : R
--> ran  G )
18456, 183sylib 189 . . . . . . 7  |-  ( ph  ->  G : R --> ran  G
)
185184adantr 452 . . . . . 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 5633 . . . . . . . 8  |-  ( v : ( 1 ... M ) -1-1-onto-> R  ->  v :
( 1 ... M
) --> R )
188186, 187syl 16 . . . . . . 7  |-  ( ph  ->  v : ( 1 ... M ) --> R )
189188adantr 452 . . . . . 6  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  v : ( 1 ... M ) --> R )
190 fco 5559 . . . . . 6  |-  ( ( G : R --> ran  G  /\  v : ( 1 ... M ) --> R )  ->  ( G  o.  v ) : ( 1 ... M ) --> ran  G )
191185, 189, 190syl2anc 643 . . . . 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 5559 . . . . 5  |-  ( ( l : ran  G --> Y  /\  ( G  o.  v ) : ( 1 ... M ) --> ran  G )  -> 
( l  o.  ( G  o.  v )
) : ( 1 ... M ) --> Y )
193182, 191, 192syl2anc 643 . . . 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 5759 . . . . . . . . 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 458 . . . . . . . 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 731 . . . . . . . . 9  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ph )
197 simplrr 738 . . . . . . . . 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 27552 . . . . . . . . 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 959 . . . . . . . . . 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 nfcv 2540 . . . . . . . . . . 11  |-  F/_ b
( ( G  o.  v ) `  i
)
201 nfv 1626 . . . . . . . . . . . . 13  |-  F/ b ( ( G  o.  v ) `  i
)  e.  ran  G
20234, 36, 201nf3an 1845 . . . . . . . . . . . 12  |-  F/ b ( ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  (
( G  o.  v
) `  i )  e.  ran  G )
203 nfv 1626 . . . . . . . . . . . 12  |-  F/ b ( l `  (
( G  o.  v
) `  i )
)  e.  ( ( G  o.  v ) `
 i )
204202, 203nfim 1828 . . . . . . . . . . 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 ) )
205 eleq1 2464 . . . . . . . . . . . . 13  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
b  e.  ran  G  <->  ( ( G  o.  v
) `  i )  e.  ran  G ) )
2062053anbi3d 1260 . . . . . . . . . . . 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 ) ) )
207 fveq2 5687 . . . . . . . . . . . . 13  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
l `  b )  =  ( l `  ( ( G  o.  v ) `  i
) ) )
208 id 20 . . . . . . . . . . . . 13  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  b  =  ( ( G  o.  v ) `  i ) )
209207, 208eleq12d 2472 . . . . . . . . . . . 12  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
( l `  b
)  e.  b  <->  ( l `  ( ( G  o.  v ) `  i
) )  e.  ( ( G  o.  v
) `  i )
) )
210206, 209imbi12d 312 . . . . . . . . . . 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 ) ) ) )
211200, 204, 210, 123vtoclgf 2970 . . . . . . . . . 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 ) ) )
212199, 211mpcom 34 . . . . . . . . 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 ) )
213196, 197, 198, 212syl3anc 1184 . . . . . . . 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 )
)
214195, 213eqeltrd 2478 . . . . . . 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
) )
215 fvco3 5759 . . . . . . . . . . . 12  |-  ( ( v : ( 1 ... M ) --> R  /\  i  e.  ( 1 ... M ) )  ->  ( ( G  o.  v ) `  i )  =  ( G `  ( v `
 i ) ) )
216188, 215sylan 458 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( G  o.  v
) `  i )  =  ( G `  ( v `  i
) ) )
217188fnvinran 27552 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
v `  i )  e.  R )
21850adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  A  e.  _V )
219 rabexg 4313 . . . . . . . . . . . . 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 )
220218, 219syl 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 )
221 raleq 2864 . . . . . . . . . . . . . . 15  |-  ( w  =  ( v `  i )  ->  ( A. t  e.  w  ( h `  t
)  <  ( E  /  M )  <->  A. t  e.  ( v `  i
) ( h `  t )  <  ( E  /  M ) ) )
2222213anbi2d 1259 . . . . . . . . . . . . . 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 )
) ) )
223222rabbidv 2908 . . . . . . . . . . . . 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 )
) } )
224223, 5fvmptg 5763 . . . . . . . . . . . 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 ) ) } )
225217, 220, 224syl2anc 643 . . . . . . . . . . 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 )
) } )
226216, 225eqtrd 2436 . . . . . . . . . 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 )
) } )
227226adantlr 696 . . . . . . . . 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 ) ) } )
228227eleq2d 2471 . . . . . . . 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 ) ) } ) )
229 nfcv 2540 . . . . . . . . . . . . . 14  |-  F/_ h
v
23024, 229nfco 4997 . . . . . . . . . . . . 13  |-  F/_ h
( G  o.  v
)
23120, 230nfco 4997 . . . . . . . . . . . 12  |-  F/_ h
( l  o.  ( G  o.  v )
)
232 nfcv 2540 . . . . . . . . . . . 12  |-  F/_ h
i
233231, 232nffv 5694 . . . . . . . . . . 11  |-  F/_ h
( ( l  o.  ( G  o.  v
) ) `  i
)
234 nfcv 2540 . . . . . . . . . . 11  |-  F/_ h A
235 nfcv 2540 . . . . . . . . . . . . 13  |-  F/_ h T
236 nfcv 2540 . . . . . . . . . . . . . . 15  |-  F/_ h
0
237 nfcv 2540 . . . . . . . . . . . . . . 15  |-  F/_ h  <_
238 nfcv 2540 . . . . . . . . . . . . . . . 16  |-  F/_ h
t
239233, 238nffv 5694 . . . . . . . . . . . . . . 15  |-  F/_ h
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)
240236, 237, 239nfbr 4216 . . . . . . . . . . . . . 14  |-  F/ h
0  <_  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )
241 nfcv 2540 . . . . . . . . . . . . . . 15  |-  F/_ h
1
242239, 237, 241nfbr 4216 . . . . . . . . . . . . . 14  |-  F/ h
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1
243240, 242nfan 1842 . . . . . . . . . . . . 13  |-  F/ h
( 0  <_  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )  /\  ( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1 )
244235, 243nfral 2719 . . . . . . . . . . . 12  |-  F/ h A. t  e.  T  ( 0  <_  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )  /\  ( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1 )
245 nfcv 2540 . . . . . . . . . . . . 13  |-  F/_ h
( v `  i
)
246 nfcv 2540 . . . . . . . . . . . . . 14  |-  F/_ h  <
247 nfcv 2540 . . . . . . . . . . . . . 14  |-  F/_ h
( E  /  M
)
248239, 246, 247nfbr 4216 . . . . . . . . . . . . 13  |-  F/ h
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <  ( E  /  M )
249245, 248nfral 2719 . . . . . . . . . . . 12  |-  F/ h A. t  e.  (
v `  i )
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <  ( E  /  M )
250 nfcv 2540 . . . . . . . . . . . . 13  |-  F/_ h
( T  \  U
)
251 nfcv 2540 . . . . . . . . . . . . . 14  |-  F/_ h
( 1  -  ( E  /  M ) )
252251, 246, 239nfbr 4216 . . . . . . . . . . . . 13  |-  F/ h
( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )
253250, 252nfral 2719 . . . . . . . . . . . 12  |-  F/ h A. t  e.  ( T  \  U ) ( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )
254244, 249, 253nf3an 1845 . . . . . . . . . . 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 ) )
255 nfcv 2540 . . . . . . . . . . . . . 14  |-  F/_ t
h
256 nfcv 2540 . . . . . . . . . . . . . . . 16  |-  F/_ t
l
257 nfcv 2540 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t R
258 nfra1 2716 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ t A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )
259 nfra1 2716 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ t A. t  e.  w  ( h `  t
)  <  ( E  /  M )
260 nfra1 2716 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ t A. t  e.  ( T  \  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t )
261258, 259, 260nf3an 1845 . . . . . . . . . . . . . . . . . . . 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 ) )
262 nfcv 2540 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ t A
263261, 262nfrab 2849 . . . . . . . . . . . . . . . . . . 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 )
) }
264257, 263nfmpt 4257 . . . . . . . . . . . . . . . . . 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 )
) } )
2655, 264nfcxfr 2537 . . . . . . . . . . . . . . . . 17  |-  F/_ t G
266 nfcv 2540 . . . . . . . . . . . . . . . . 17  |-  F/_ t
v
267265, 266nfco 4997 . . . . . . . . . . . . . . . 16  |-  F/_ t
( G  o.  v
)
268256, 267nfco 4997 . . . . . . . . . . . . . . 15  |-  F/_ t
( l  o.  ( G  o.  v )
)
269 nfcv 2540 . . . . . . . . . . . . . . 15  |-  F/_ t
i
270268, 269nffv 5694 . . . . . . . . . . . . . 14  |-  F/_ t
( ( l  o.  ( G  o.  v
) ) `  i
)
271255, 270nfeq 2547 . . . . . . . . . . . . 13  |-  F/ t  h  =  ( ( l  o.  ( G  o.  v ) ) `
 i )
272 fveq1 5686 . . . . . . . . . . . . . . 15  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
h `  t )  =  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t ) )
273272breq2d 4184 . . . . . . . . . . . . . 14  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
0  <_  ( h `  t )  <->  0  <_  ( ( ( l  o.  ( G  o.  v
) ) `  i
) `  t )
) )
274272breq1d 4182 . . . . . . . . . . . . . 14  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
( h `  t
)  <_  1  <->  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )  <_  1
) )
275273, 274anbi12d 692 . . . . . . . . . . . . 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 ) ) )
276271, 275ralbid 2684 . . . . . . . . . . . 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 ) ) )
277272breq1d 4182 . . . . . . . . . . . . 13  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
( h `  t
)  <  ( E  /  M )  <->  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )  <  ( E  /  M ) ) )
278271, 277ralbid 2684 . . . . . . . . . . . 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 ) ) )
279272breq2d 4184 . . . . . . . . . . . . 13  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
( 1  -  ( E  /  M ) )  <  ( h `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
) ) )
280271, 279ralbid 2684 . . . . . . . . . . . 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 )
) )
281276, 278, 2803anbi123d 1254 . . . . . . . . . . 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 ) ) ) )
282233, 234, 254, 281elrabf 3051 . . . . . . . . . 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 ) ) ) )
283282simprbi 451 . . . . . . . . 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 ) ) )
284283simp2d 970 . . . . . . . 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 ) )
285228, 284syl6bi 220 . . . . . . 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 ) ) )
286214, 285mpd 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 ) )
287 stoweidlem31.2 . . . . . . . . 9  |-  F/ t
ph
288265nfrn 5071 . . . . . . . . . . 11  |-  F/_ t ran  G
289256, 288nffn 5500 . . . . . . . . . 10  |-  F/ t  l  Fn  ran  G
290 nfv 1626 . . . . . . . . . . 11  |-  F/ t ( b  =/=  (/)  ->  (
l `  b )  e.  b )
291288, 290nfral 2719 . . . . . . . . . 10  |-  F/ t A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )
292289, 291nfan 1842 . . . . . . . . 9  |-  F/ t ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
293287, 292nfan 1842 . . . . . . . 8  |-  F/ t ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
294 nfv 1626 . . . . . . . 8  |-  F/ t  i  e.  ( 1 ... M )
295293, 294nfan 1842 . . . . . . 7  |-  F/ t ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )
296 stoweidlem31.11 . . . . . . . . . . 11  |-  ( ph  ->  B  C_  ( T  \  U ) )
297296ad3antrrr 711 . . . . . . . . . 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 ) )
298 simpr 448 . . . . . . . . . 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 )
299297, 298sseldd 3309 . . . . . . . . 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 ) )
300283simp3d 971 . . . . . . . . . . . 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 )
)
301228, 300syl6bi 220 . . . . . . . . . . 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 )
) )
302214, 301mpd 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 )
)
303302r19.21bi 2764 . . . . . . . . 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
) )
304299, 303syldan 457 . . . . . . . 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
) )
305304ex 424 . . . . . . 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
) ) )
306295, 305ralrimi 2747 . . . . . 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
) )
307286, 306jca 519 . . . . 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 ) ) )
308307ralrimiva 2749 . . . 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 ) ) )
309193, 308jca 519 . . 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 ) ) ) )
310 feq1 5535 . . . . 5  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
x : ( 1 ... M ) --> Y  <-> 
( l  o.  ( G  o.  v )
) : ( 1 ... M ) --> Y ) )
311 nfcv 2540 . . . . . . . . 9  |-  F/_ t
x
312311, 268nfeq 2547 . . . . . . . 8  |-  F/ t  x  =  ( l  o.  ( G  o.  v ) )
313 fveq1 5686 . . . . . . . . . 10  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
x `  i )  =  ( ( l  o.  ( G  o.  v ) ) `  i ) )
314313fveq1d 5689 . . . . . . . . 9  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
( x `  i
) `  t )  =  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t ) )
315314breq1d 4182 . . . . . . . 8  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
( ( x `  i ) `  t
)  <  ( E  /  M )  <->  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )  <  ( E  /  M ) ) )
316312, 315ralbid 2684 . . . . . . 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 ) ) )
317314breq2d 4184 . . . . . . . 8  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
( 1  -  ( E  /  M ) )  <  ( ( x `
 i ) `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
) ) )
318312, 317ralbid 2684 . . . . . . 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
) ) )
319316, 318anbi12d 692 . . . . . 6  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
( A. t