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

Theorem stoweidlem31 37451
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 36980 . . 3  |-  ( ran 
G  e.  Fin  ->  E. l ( l  Fn 
ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )
31, 2syl 17 . 2  |-  ( ph  ->  E. l ( l  Fn  ran  G  /\  A. b  e.  ran  G
( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
4 vex 3090 . . . . 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 4572 . . . . . . . 8  |-  ( ph  ->  R  e.  _V )
9 mptexg 6150 . . . . . . . 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 17 . . . . . . 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 2521 . . . . . 6  |-  ( ph  ->  G  e.  _V )
12 vex 3090 . . . . . 6  |-  v  e. 
_V
13 coexg 6758 . . . . . 6  |-  ( ( G  e.  _V  /\  v  e.  _V )  ->  ( G  o.  v
)  e.  _V )
1411, 12, 13sylancl 666 . . . . 5  |-  ( ph  ->  ( G  o.  v
)  e.  _V )
15 coexg 6758 . . . . 5  |-  ( ( l  e.  _V  /\  ( G  o.  v
)  e.  _V )  ->  ( l  o.  ( G  o.  v )
)  e.  _V )
164, 14, 15sylancr 667 . . . 4  |-  ( ph  ->  ( l  o.  ( G  o.  v )
)  e.  _V )
1716adantr 466 . . 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 762 . . . . . 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 2591 . . . . . . . . . . 11  |-  F/_ h
l
21 nfcv 2591 . . . . . . . . . . . . . 14  |-  F/_ h R
22 nfrab1 3016 . . . . . . . . . . . . . 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 4514 . . . . . . . . . . . . 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 2589 . . . . . . . . . . . 12  |-  F/_ h G
2524nfrn 5097 . . . . . . . . . . 11  |-  F/_ h ran  G
2620, 25nffn 5690 . . . . . . . . . 10  |-  F/ h  l  Fn  ran  G
27 nfv 1754 . . . . . . . . . . 11  |-  F/ h
( b  =/=  (/)  ->  (
l `  b )  e.  b )
2825, 27nfral 2818 . . . . . . . . . 10  |-  F/ h A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )
2926, 28nfan 1986 . . . . . . . . 9  |-  F/ h
( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
3019, 29nfan 1986 . . . . . . . 8  |-  F/ h
( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
31 fvelrnb 5928 . . . . . . . . . . . . 13  |-  ( l  Fn  ran  G  -> 
( h  e.  ran  l 
<->  E. b  e.  ran  G ( l `  b
)  =  h ) )
3218, 31syl 17 . . . . . . . . . . . 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 486 . . . . . . . . . . 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 1754 . . . . . . . . . . . . . 14  |-  F/ b
ph
35 nfv 1754 . . . . . . . . . . . . . . 15  |-  F/ b  l  Fn  ran  G
36 nfra1 2813 . . . . . . . . . . . . . . 15  |-  F/ b A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )
3735, 36nfan 1986 . . . . . . . . . . . . . 14  |-  F/ b ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
3834, 37nfan 1986 . . . . . . . . . . . . 13  |-  F/ b ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
39 nfv 1754 . . . . . . . . . . . . 13  |-  F/ b  h  e.  ran  l
4038, 39nfan 1986 . . . . . . . . . . . 12  |-  F/ b ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  h  e.  ran  l )
41 simp3 1007 . . . . . . . . . . . . . 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 1068 . . . . . . . . . . . . . . 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 769 . . . . . . . . . . . . . . . 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 1026 . . . . . . . . . . . . . . 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 1006 . . . . . . . . . . . . . . 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 1007 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
b  e.  ran  G
)
47 3simpc 1004 . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . . . . . 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 4575 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . . . . . . 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 26 . . . . . . . . . . . . . . . . . . . . . . . . 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 2832 . . . . . . . . . . . . . . . . . . . . . . . 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 5722 . . . . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  G  Fn  R )
5756adantr 466 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  b  e.  ran  G )  ->  G  Fn  R )
58 fvelrnb 5928 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( G  Fn  R  ->  (
b  e.  ran  G  <->  E. u  e.  R  ( G `  u )  =  b ) )
59 nfmpt1 4515 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2589 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ w G
61 nfcv 2591 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/_ w u
6260, 61nffv 5888 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ w
( G `  u
)
63 nfcv 2591 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ w
b
6462, 63nfeq 2602 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ w
( G `  u
)  =  b
65 nfv 1754 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ u
( G `  w
)  =  b
66 fveq2 5881 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( u  =  w  ->  ( G `  u )  =  ( G `  w ) )
6766eqeq1d 2431 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( u  =  w  ->  (
( G `  u
)  =  b  <->  ( G `  w )  =  b ) )
6864, 65, 67cbvrex 3059 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. u  e.  R  ( G `  u )  =  b  <->  E. w  e.  R  ( G `  w )  =  b )
6958, 68syl6bb 264 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( G  Fn  R  ->  (
b  e.  ran  G  <->  E. w  e.  R  ( G `  w )  =  b ) )
7057, 69syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  b  e.  ran  G )  ->  (
b  e.  ran  G  <->  E. w  e.  R  ( G `  w )  =  b ) )
7148, 70mpbid 213 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  b  e.  ran  G )  ->  E. w  e.  R  ( G `  w )  =  b )
7260nfrn 5097 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ w ran  G
7372nfcri 2584 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ w  b  e.  ran  G
7449, 73nfan 1986 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ w
( ph  /\  b  e.  ran  G )
75 nfv 1754 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ w  b  =/=  (/)
76 simp3 1007 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  ( G `  w )  =  b )
77 simpr 462 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  w  e.  R )  ->  w  e.  R )
7850adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  w  e.  R )  ->  A  e.  _V )
7978, 51syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5973 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . . . . . . 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 3470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3084 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 464 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  M  e.  RR+ )
9087, 89rpdivcld 11358 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( E  /  M
)  e.  RR+ )
9190adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  w  e.  R )  ->  ( E  /  M )  e.  RR+ )
92 breq2 4430 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( e  =  ( E  /  M )  ->  (
( h `  t
)  <  e  <->  ( h `  t )  <  ( E  /  M ) ) )
9392ralbidv 2871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( e  =  ( E  /  M )  ->  ( A. t  e.  w  ( h `  t
)  <  e  <->  A. t  e.  w  ( h `  t )  <  ( E  /  M ) ) )
94 oveq2 6313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( e  =  ( E  /  M )  ->  (
1  -  e )  =  ( 1  -  ( E  /  M
) ) )
9594breq1d 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( e  =  ( E  /  M )  ->  (
( 1  -  e
)  <  ( h `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( h `  t
) ) )
9695ralbidv 2871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1338 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2946 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3187 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 665 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1754 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/ h  w  e.  R
10219, 101nfan 1986 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/ h
( ph  /\  w  e.  R )
103 nfcv 2591 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/_ h (/)
10422, 103nfne 2763 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1004 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3012 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 215 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3773 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 1204 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2916 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2724 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  w  e.  R )  ->  ( G `  w )  =/=  (/) )
1141133adant3 1025 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  ( G `  w )  =/=  (/) )
11576, 114eqnetrrd 2725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  b  =/=  (/) )
1161153adant1r 1257 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  b  e.  ran  G )  /\  w  e.  R  /\  ( G `  w )  =  b )  -> 
b  =/=  (/) )
1171163exp 1204 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  b  e.  ran  G )  ->  (
w  e.  R  -> 
( ( G `  w )  =  b  ->  b  =/=  (/) ) ) )
11874, 75, 117rexlimd 2916 . . . . . . . . . . . . . . . . . . . 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 1024 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
b  =/=  (/) )
121 rspa 2799 . . . . . . . . . . . . . . . . . 18  |-  ( ( A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  b  e.  ran  G )  -> 
( b  =/=  (/)  ->  (
l `  b )  e.  b ) )
12247, 120, 121sylc 62 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
( l `  b
)  e.  b )
12346, 122jca 534 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
( b  e.  ran  G  /\  ( l `  b )  e.  b ) )
124 vex 3090 . . . . . . . . . . . . . . . . . 18  |-  b  e. 
_V
1255elrnmpt 5101 . . . . . . . . . . . . . . . . . 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 )
) } ) )
126124, 125ax-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 )
) } )
12746, 126sylib 199 . . . . . . . . . . . . . . . 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 ) ) } )
128 nfv 1754 . . . . . . . . . . . . . . . . . 18  |-  F/ w
( l `  b
)  e.  b
12973, 128nfan 1986 . . . . . . . . . . . . . . . . 17  |-  F/ w
( b  e.  ran  G  /\  ( l `  b )  e.  b )
130 nfv 1754 . . . . . . . . . . . . . . . . 17  |-  F/ w
( l `  b
)  e.  Y
131 simp1r 1030 . . . . . . . . . . . . . . . . . . 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 )
132 simp3 1007 . . . . . . . . . . . . . . . . . . 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 ) ) } )
133 simpl 458 . . . . . . . . . . . . . . . . . . . . . 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 )
134 simpr 462 . . . . . . . . . . . . . . . . . . . . . 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 )
) } )
135133, 134eleqtrd 2519 . . . . . . . . . . . . . . . . . . . . 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 ) ) } )
136 elrabi 3232 . . . . . . . . . . . . . . . . . . . . . 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 )
137 fveq1 5880 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( h  =  ( l `  b )  ->  (
h `  t )  =  ( ( l `
 b ) `  t ) )
138137breq2d 4438 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( h  =  ( l `  b )  ->  (
0  <_  ( h `  t )  <->  0  <_  ( ( l `  b
) `  t )
) )
139137breq1d 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( h  =  ( l `  b )  ->  (
( h `  t
)  <_  1  <->  ( (
l `  b ) `  t )  <_  1
) )
140138, 139anbi12d 715 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  =  ( l `  b )  ->  (
( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  <-> 
( 0  <_  (
( l `  b
) `  t )  /\  ( ( l `  b ) `  t
)  <_  1 ) ) )
141140ralbidv 2871 . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
142137breq1d 4436 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  =  ( l `  b )  ->  (
( h `  t
)  <  ( E  /  M )  <->  ( (
l `  b ) `  t )  <  ( E  /  M ) ) )
143142ralbidv 2871 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( h  =  ( l `  b )  ->  ( A. t  e.  w  ( h `  t
)  <  ( E  /  M )  <->  A. t  e.  w  ( (
l `  b ) `  t )  <  ( E  /  M ) ) )
144137breq2d 4438 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( h  =  ( l `  b )  ->  (
( 1  -  ( E  /  M ) )  <  ( h `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( ( l `  b ) `  t
) ) )
145144ralbidv 2871 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) )
146141, 143, 1453anbi123d 1335 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
) ) )
147146elrab 3235 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
148147simprbi 465 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
149148simp1d 1017 . . . . . . . . . . . . . . . . . . . . . 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 ) )
150141elrab 3235 . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
151136, 149, 150sylanbrc 668 . . . . . . . . . . . . . . . . . . . . 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 ) } )
152135, 151syl 17 . . . . . . . . . . . . . . . . . . . 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 ) } )
153 stoweidlem31.4 . . . . . . . . . . . . . . . . . . . 20  |-  Y  =  { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }
154152, 153syl6eleqr 2528 . . . . . . . . . . . . . . . . . . 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
)
155131, 132, 154syl2anc 665 . . . . . . . . . . . . . . . . . 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 )
1561553exp 1204 . . . . . . . . . . . . . . . . 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 ) ) )
157129, 130, 156rexlimd 2916 . . . . . . . . . . . . . . . 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 ) )
158123, 127, 157sylc 62 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
( l `  b
)  e.  Y )
15942, 44, 45, 158syl3anc 1264 . . . . . . . . . . . . . 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
)
16041, 159eqeltrrd 2518 . . . . . . . . . . . . 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 )
1611603exp 1204 . . . . . . . . . . . 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
) ) )
16240, 161reximdai 2901 . . . . . . . . . . 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 ) )
16333, 162mpd 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 )
164 nfv 1754 . . . . . . . . . . 11  |-  F/ b  h  e.  Y
165 idd 25 . . . . . . . . . . . 12  |-  ( b  e.  ran  G  -> 
( h  e.  Y  ->  h  e.  Y ) )
166165a1i 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 ) ) )
16740, 164, 166rexlimd 2916 . . . . . . . . . 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 )
)
168163, 167mpd 15 . . . . . . . . 9  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  ->  h  e.  Y )
169168ex 435 . . . . . . . 8  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( h  e. 
ran  l  ->  h  e.  Y ) )
17030, 169ralrimi 2832 . . . . . . 7  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  A. h  e.  ran  l  h  e.  Y
)
171 dfss3 3460 . . . . . . . 8  |-  ( ran  l  C_  Y  <->  A. z  e.  ran  l  z  e.  Y )
172 nfrab1 3016 . . . . . . . . . . 11  |-  F/_ h { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }
173153, 172nfcxfr 2589 . . . . . . . . . 10  |-  F/_ h Y
174173nfcri 2584 . . . . . . . . 9  |-  F/ h  z  e.  Y
175 nfv 1754 . . . . . . . . 9  |-  F/ z  h  e.  Y
176 eleq1 2501 . . . . . . . . 9  |-  ( z  =  h  ->  (
z  e.  Y  <->  h  e.  Y ) )
177174, 175, 176cbvral 3058 . . . . . . . 8  |-  ( A. z  e.  ran  l  z  e.  Y  <->  A. h  e.  ran  l  h  e.  Y )
178171, 177bitri 252 . . . . . . 7  |-  ( ran  l  C_  Y  <->  A. h  e.  ran  l  h  e.  Y )
179170, 178sylibr 215 . . . . . 6  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ran  l  C_  Y )
180 df-f 5605 . . . . . 6  |-  ( l : ran  G --> Y  <->  ( l  Fn  ran  G  /\  ran  l  C_  Y ) )
18118, 179, 180sylanbrc 668 . . . . 5  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  l : ran  G --> Y )
182 dffn3 5753 . . . . . . . 8  |-  ( G  Fn  R  <->  G : R
--> ran  G )
18356, 182sylib 199 . . . . . . 7  |-  ( ph  ->  G : R --> ran  G
)
184183adantr 466 . . . . . 6  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  G : R --> ran  G )
185 stoweidlem31.9 . . . . . . . 8  |-  ( ph  ->  v : ( 1 ... M ) -1-1-onto-> R )
186 f1of 5831 . . . . . . . 8  |-  ( v : ( 1 ... M ) -1-1-onto-> R  ->  v :
( 1 ... M
) --> R )
187185, 186syl 17 . . . . . . 7  |-  ( ph  ->  v : ( 1 ... M ) --> R )
188187adantr 466 . . . . . 6  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  v : ( 1 ... M ) --> R )
189 fco 5756 . . . . . 6  |-  ( ( G : R --> ran  G  /\  v : ( 1 ... M ) --> R )  ->  ( G  o.  v ) : ( 1 ... M ) --> ran  G )
190184, 188, 189syl2anc 665 . . . . 5  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( G  o.  v ) : ( 1 ... M ) --> ran  G )
191 fco 5756 . . . . 5  |-  ( ( l : ran  G --> Y  /\  ( G  o.  v ) : ( 1 ... M ) --> ran  G )  -> 
( l  o.  ( G  o.  v )
) : ( 1 ... M ) --> Y )
192181, 190, 191syl2anc 665 . . . 4  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( l  o.  ( G  o.  v
) ) : ( 1 ... M ) --> Y )
193 fvco3 5958 . . . . . . . . 9  |-  ( ( ( G  o.  v
) : ( 1 ... M ) --> ran 
G  /\  i  e.  ( 1 ... M
) )  ->  (
( l  o.  ( G  o.  v )
) `  i )  =  ( l `  ( ( G  o.  v ) `  i
) ) )
194190, 193sylan 473 . . . . . . . 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 )
) )
195 simpll 758 . . . . . . . . 9  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ph )
196 simplrr 769 . . . . . . . . 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 ) )
197190fnvinran 36965 . . . . . . . . 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 )
198 simp3 1007 . . . . . . . . . 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
)
199 nfv 1754 . . . . . . . . . . . . 13  |-  F/ b ( ( G  o.  v ) `  i
)  e.  ran  G
20034, 36, 199nf3an 1988 . . . . . . . . . . . 12  |-  F/ b ( ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  (
( G  o.  v
) `  i )  e.  ran  G )
201 nfv 1754 . . . . . . . . . . . 12  |-  F/ b ( l `  (
( G  o.  v
) `  i )
)  e.  ( ( G  o.  v ) `
 i )
202200, 201nfim 1978 . . . . . . . . . . 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 ) )
203 eleq1 2501 . . . . . . . . . . . . 13  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
b  e.  ran  G  <->  ( ( G  o.  v
) `  i )  e.  ran  G ) )
2042033anbi3d 1341 . . . . . . . . . . . 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 ) ) )
205 fveq2 5881 . . . . . . . . . . . . 13  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
l `  b )  =  ( l `  ( ( G  o.  v ) `  i
) ) )
206 id 23 . . . . . . . . . . . . 13  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  b  =  ( ( G  o.  v ) `  i ) )
207205, 206eleq12d 2511 . . . . . . . . . . . 12  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
( l `  b
)  e.  b  <->  ( l `  ( ( G  o.  v ) `  i
) )  e.  ( ( G  o.  v
) `  i )
) )
208204, 207imbi12d 321 . . . . . . . . . . 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 ) ) ) )
209202, 208, 122vtoclg1f 3144 . . . . . . . . . 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 ) ) )
210198, 209mpcom 37 . . . . . . . . 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 ) )
211195, 196, 197, 210syl3anc 1264 . . . . . . . 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 )
)
212194, 211eqeltrd 2517 . . . . . . 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
) )
213 fvco3 5958 . . . . . . . . . . . 12  |-  ( ( v : ( 1 ... M ) --> R  /\  i  e.  ( 1 ... M ) )  ->  ( ( G  o.  v ) `  i )  =  ( G `  ( v `
 i ) ) )
214187, 213sylan 473 . . . . . . . . . . 11  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( G  o.  v
) `  i )  =  ( G `  ( v `  i
) ) )
215187fnvinran 36965 . . . . . . . . . . . 12  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
v `  i )  e.  R )
21650adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  A  e.  _V )
217 rabexg 4575 . . . . . . . . . . . . 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 )
218216, 217syl 17 . . . . . . . . . . . 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 )
219 raleq 3032 . . . . . . . . . . . . . . 15  |-  ( w  =  ( v `  i )  ->  ( A. t  e.  w  ( h `  t
)  <  ( E  /  M )  <->  A. t  e.  ( v `  i
) ( h `  t )  <  ( E  /  M ) ) )
2202193anbi2d 1340 . . . . . . . . . . . . . 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 )
) ) )
221220rabbidv 3079 . . . . . . . . . . . . 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 )
) } )
222221, 5fvmptg 5962 . . . . . . . . . . . 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 ) ) } )
223215, 218, 222syl2anc 665 . . . . . . . . . . 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 )
) } )
224214, 223eqtrd 2470 . . . . . . . . . 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 )
) } )
225224adantlr 719 . . . . . . . . 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 ) ) } )
226225eleq2d 2499 . . . . . . . 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 ) ) } ) )
227 nfcv 2591 . . . . . . . . . . . . . 14  |-  F/_ h
v
22824, 227nfco 5020 . . . . . . . . . . . . 13  |-  F/_ h
( G  o.  v
)
22920, 228nfco 5020 . . . . . . . . . . . 12  |-  F/_ h
( l  o.  ( G  o.  v )
)
230 nfcv 2591 . . . . . . . . . . . 12  |-  F/_ h
i
231229, 230nffv 5888 . . . . . . . . . . 11  |-  F/_ h
( ( l  o.  ( G  o.  v
) ) `  i
)
232 nfcv 2591 . . . . . . . . . . 11  |-  F/_ h A
233 nfcv 2591 . . . . . . . . . . . . 13  |-  F/_ h T
234 nfcv 2591 . . . . . . . . . . . . . . 15  |-  F/_ h
0
235 nfcv 2591 . . . . . . . . . . . . . . 15  |-  F/_ h  <_
236 nfcv 2591 . . . . . . . . . . . . . . . 16  |-  F/_ h
t
237231, 236nffv 5888 . . . . . . . . . . . . . . 15  |-  F/_ h
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)
238234, 235, 237nfbr 4470 . . . . . . . . . . . . . 14  |-  F/ h
0  <_  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )
239 nfcv 2591 . . . . . . . . . . . . . . 15  |-  F/_ h
1
240237, 235, 239nfbr 4470 . . . . . . . . . . . . . 14  |-  F/ h
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1
241238, 240nfan 1986 . . . . . . . . . . . . 13  |-  F/ h
( 0  <_  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )  /\  ( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1 )
242233, 241nfral 2818 . . . . . . . . . . . 12  |-  F/ h A. t  e.  T  ( 0  <_  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )  /\  ( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1 )
243 nfcv 2591 . . . . . . . . . . . . 13  |-  F/_ h
( v `  i
)
244 nfcv 2591 . . . . . . . . . . . . . 14  |-  F/_ h  <
245 nfcv 2591 . . . . . . . . . . . . . 14  |-  F/_ h
( E  /  M
)
246237, 244, 245nfbr 4470 . . . . . . . . . . . . 13  |-  F/ h
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <  ( E  /  M )
247243, 246nfral 2818 . . . . . . . . . . . 12  |-  F/ h A. t  e.  (
v `  i )
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <  ( E  /  M )
248 nfcv 2591 . . . . . . . . . . . . 13  |-  F/_ h
( T  \  U
)
249 nfcv 2591 . . . . . . . . . . . . . 14  |-  F/_ h
( 1  -  ( E  /  M ) )
250249, 244, 237nfbr 4470 . . . . . . . . . . . . 13  |-  F/ h
( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )
251248, 250nfral 2818 . . . . . . . . . . . 12  |-  F/ h A. t  e.  ( T  \  U ) ( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )
252242, 247, 251nf3an 1988 . . . . . . . . . . 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 ) )
253 nfcv 2591 . . . . . . . . . . . . . 14  |-  F/_ t
h
254 nfcv 2591 . . . . . . . . . . . . . . . 16  |-  F/_ t
l
255 nfcv 2591 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t R
256 nfra1 2813 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ t A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )
257 nfra1 2813 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ t A. t  e.  w  ( h `  t
)  <  ( E  /  M )
258 nfra1 2813 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ t A. t  e.  ( T  \  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t )
259256, 257, 258nf3an 1988 . . . . . . . . . . . . . . . . . . . 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 ) )
260 nfcv 2591 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ t A
261259, 260nfrab 3017 . . . . . . . . . . . . . . . . . . 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 )
) }
262255, 261nfmpt 4514 . . . . . . . . . . . . . . . . . 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 )
) } )
2635, 262nfcxfr 2589 . . . . . . . . . . . . . . . . 17  |-  F/_ t G
264 nfcv 2591 . . . . . . . . . . . . . . . . 17  |-  F/_ t
v
265263, 264nfco 5020 . . . . . . . . . . . . . . . 16  |-  F/_ t
( G  o.  v
)
266254, 265nfco 5020 . . . . . . . . . . . . . . 15  |-  F/_ t
( l  o.  ( G  o.  v )
)
267 nfcv 2591 . . . . . . . . . . . . . . 15  |-  F/_ t
i
268266, 267nffv 5888 . . . . . . . . . . . . . 14  |-  F/_ t
( ( l  o.  ( G  o.  v
) ) `  i
)
269253, 268nfeq 2602 . . . . . . . . . . . . 13  |-  F/ t  h  =  ( ( l  o.  ( G  o.  v ) ) `
 i )
270 fveq1 5880 . . . . . . . . . . . . . . 15  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
h `  t )  =  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t ) )
271270breq2d 4438 . . . . . . . . . . . . . 14  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
0  <_  ( h `  t )  <->  0  <_  ( ( ( l  o.  ( G  o.  v
) ) `  i
) `  t )
) )
272270breq1d 4436 . . . . . . . . . . . . . 14  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
( h `  t
)  <_  1  <->  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )  <_  1
) )
273271, 272anbi12d 715 . . . . . . . . . . . . 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 ) ) )
274269, 273ralbid 2866 . . . . . . . . . . . 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 ) ) )
275270breq1d 4436 . . . . . . . . . . . . 13  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
( h `  t
)  <  ( E  /  M )  <->  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )  <  ( E  /  M ) ) )
276269, 275ralbid 2866 . . . . . . . . . . . 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 ) ) )
277270breq2d 4438 . . . . . . . . . . . . 13  |-  ( h  =  ( ( l  o.  ( G  o.  v ) ) `  i )  ->  (
( 1  -  ( E  /  M ) )  <  ( h `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
) ) )
278269, 277ralbid 2866 . . . . . . . . . . . 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 )
) )
279274, 276, 2783anbi123d 1335 . . . . . . . . . . 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 ) ) ) )
280231, 232, 252, 279elrabf 3233 . . . . . . . . . 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 ) ) ) )
281280simprbi 465 . . . . . . . . 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 ) ) )
282281simp2d 1018 . . . . . . . 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 ) )
283226, 282syl6bi 231 . . . . . . 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 ) ) )
284212, 283mpd 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 ) )
285 stoweidlem31.2 . . . . . . . . 9  |-  F/ t
ph
286263nfrn 5097 . . . . . . . . . . 11  |-  F/_ t ran  G
287254, 286nffn 5690 . . . . . . . . . 10  |-  F/ t  l  Fn  ran  G
288 nfv 1754 . . . . . . . . . . 11  |-  F/ t ( b  =/=  (/)  ->  (
l `  b )  e.  b )
289286, 288nfral 2818 . . . . . . . . . 10  |-  F/ t A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )
290287, 289nfan 1986 . . . . . . . . 9  |-  F/ t ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
291285, 290nfan 1986 . . . . . . . 8  |-  F/ t ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
292 nfv 1754 . . . . . . . 8  |-  F/ t  i  e.  ( 1 ... M )
293291, 292nfan 1986 . . . . . . 7  |-  F/ t ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )
294 stoweidlem31.11 . . . . . . . . . . 11  |-  ( ph  ->  B  C_  ( T  \  U ) )
295294ad3antrrr 734 . . . . . . . . . 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 ) )
296 simpr 462 . . . . . . . . . 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 )
297295, 296sseldd 3471 . . . . . . . . 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 ) )
298281simp3d 1019 . . . . . . . . . . . 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 )
)
299226, 298syl6bi 231 . . . . . . . . . . 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 )
) )
300212, 299mpd 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 )
)
301300r19.21bi 2801 . . . . . . . . 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
) )
302297, 301syldan 472 . . . . . . . 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
) )
303302ex 435 . . . . . . 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
) ) )
304293, 303ralrimi 2832 . . . . . 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
) )
305284, 304jca 534 . . . . 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 ) ) )
306305ralrimiva 2846 . . . 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 ) ) )
307192, 306jca 534 . . 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 ) ) ) )
308 feq1 5728 . . . . 5  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
x : ( 1 ... M ) --> Y  <-> 
( l  o.  ( G  o.  v )
) : ( 1 ... M ) --> Y ) )
309 nfcv 2591 . . . . . . . . 9  |-  F/_ t
x
310309, 266nfeq 2602 . . . . . . . 8  |-  F/ t  x  =  ( l  o.  ( G  o.  v ) )
311 fveq1 5880 . . . . . . . . . 10  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
x `  i )  =  ( ( l  o.  ( G  o.  v ) ) `  i ) )
312311fveq1d 5883 . . . . . . . . 9  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
( x `  i
) `  t )  =  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t ) )
313312breq1d 4436 . . . . . . . 8  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
( ( x `  i ) `  t
)  <  ( E  /  M )  <->  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )  <  ( E  /  M ) ) )
314310, 313ralbid 2866 . . . . . . 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 ) ) )
315312breq2d 4438 . . . . . . . 8  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
( 1  -  ( E  /  M ) )  <  ( ( x `
 i ) `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
) ) )
316310, 315ralbid 2866 . . . . . . 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
) ) )
317314, 316anbi12d 715 . . . . . 6  |-  ( x  =  ( l  o.  ( G  o.  v
) )  ->  (
( A. t  e.  ( v `  i
) ( ( x `
 i ) `  t )  <  ( E  /  M )  /\  A. t  e.  B  ( 1  -  ( E  /  M ) )  <  ( ( x `
 i ) `  t ) )  <->  ( A. t  e.  ( v `  i ) ( ( ( l  o.  ( G