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

Theorem stoweidlem31 27883
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 27803 . . 3  |-  ( ran 
G  e.  Fin  ->  E. l ( l  Fn 
ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )
31, 2syl 15 . 2  |-  ( ph  ->  E. l ( l  Fn  ran  G  /\  A. b  e.  ran  G
( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
4 vex 2804 . . . . . . . . 9  |-  l  e. 
_V
54a1i 10 . . . . . . . 8  |-  ( ph  ->  l  e.  _V )
6 stoweidlem31.6 . . . . . . . . . . 11  |-  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 )
) } )
7 stoweidlem31.7 . . . . . . . . . . . . . 14  |-  ( ph  ->  R  C_  V )
8 stoweidlem31.12 . . . . . . . . . . . . . 14  |-  ( ph  ->  V  e.  _V )
97, 8jca 518 . . . . . . . . . . . . 13  |-  ( ph  ->  ( R  C_  V  /\  V  e.  _V ) )
10 ssexg 4176 . . . . . . . . . . . . 13  |-  ( ( R  C_  V  /\  V  e.  _V )  ->  R  e.  _V )
119, 10syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  R  e.  _V )
12 mptexg 5761 . . . . . . . . . . . 12  |-  ( 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 )
1311, 12syl 15 . . . . . . . . . . 11  |-  ( 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 )
146, 13syl5eqel 2380 . . . . . . . . . 10  |-  ( ph  ->  G  e.  _V )
15 vex 2804 . . . . . . . . . . 11  |-  v  e. 
_V
1615a1i 10 . . . . . . . . . 10  |-  ( ph  ->  v  e.  _V )
1714, 16jca 518 . . . . . . . . 9  |-  ( ph  ->  ( G  e.  _V  /\  v  e.  _V )
)
18 coexg 5231 . . . . . . . . 9  |-  ( ( G  e.  _V  /\  v  e.  _V )  ->  ( G  o.  v
)  e.  _V )
1917, 18syl 15 . . . . . . . 8  |-  ( ph  ->  ( G  o.  v
)  e.  _V )
205, 19jca 518 . . . . . . 7  |-  ( ph  ->  ( l  e.  _V  /\  ( G  o.  v
)  e.  _V )
)
21 coexg 5231 . . . . . . 7  |-  ( ( l  e.  _V  /\  ( G  o.  v
)  e.  _V )  ->  ( l  o.  ( G  o.  v )
)  e.  _V )
2220, 21syl 15 . . . . . 6  |-  ( ph  ->  ( l  o.  ( G  o.  v )
)  e.  _V )
2322adantr 451 . . . . 5  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( l  o.  ( G  o.  v
) )  e.  _V )
24 simprl 732 . . . . . . . . . 10  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  l  Fn  ran  G )
25 nfv 1609 . . . . . . . . . . . 12  |-  F/ b
ph
26 nfv 1609 . . . . . . . . . . . . 13  |-  F/ b  l  Fn  ran  G
27 nfra1 2606 . . . . . . . . . . . . 13  |-  F/ b A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )
2826, 27nfan 1783 . . . . . . . . . . . 12  |-  F/ b ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
2925, 28nfan 1783 . . . . . . . . . . 11  |-  F/ b ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
30 simplrl 736 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  b  e.  ran  G )  ->  l  Fn  ran  G )
31 stoweidlem31.1 . . . . . . . . . . . . . . . . . . . 20  |-  F/ h ph
32 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ h
l
33 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/_ h R
34 nfrab1 2733 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  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 )
) }
3533, 34nfmpt 4124 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  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 )
) } )
366, 35nfcxfr 2429 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/_ h G
3736nfrn 4937 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ h ran  G
3832, 37nffn 5356 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ h  l  Fn  ran  G
39 nfv 1609 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ h
( b  =/=  (/)  ->  (
l `  b )  e.  b )
4037, 39nfral 2609 . . . . . . . . . . . . . . . . . . . . 21  |-  F/ h A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )
4138, 40nfan 1783 . . . . . . . . . . . . . . . . . . . 20  |-  F/ h
( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
4231, 41nfan 1783 . . . . . . . . . . . . . . . . . . 19  |-  F/ h
( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
43 fvelrnb 5586 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( l  Fn  ran  G  -> 
( h  e.  ran  l 
<->  E. b  e.  ran  G ( l `  b
)  =  h ) )
4424, 43syl 15 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
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 ) )
4544biimpa 470 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 )
46 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  F/ b  h  e.  ran  l
4729, 46nfan 1783 . . . . . . . . . . . . . . . . . . . . . . 23  |-  F/ b ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  h  e.  ran  l )
48 simp3 957 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 )
49 simp1ll 1018 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 )
50 simplrr 737 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 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 ) )
51503ad2ant1 976 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 ) )
52 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 )
5349, 51, 523jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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  /\ 
A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  b  e.  ran  G ) )
54 simp3 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
b  e.  ran  G
)
55 3simpc 954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
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 ) )
56 3simpb 953 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
( ph  /\  b  e.  ran  G ) )
57 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  b  e.  ran  G )  ->  b  e.  ran  G )
58 stoweidlem31.3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/ w ph
59 stoweidlem31.13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ph  ->  A  e.  _V )
60 rabexg 4180 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( 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 )
6159, 60syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( 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 )
6261a1d 22 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( 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 ) )
6358, 62ralrimi 2637 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 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 )
646fnmpt 5386 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 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 )
6563, 64syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  G  Fn  R )
6665adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( (
ph  /\  b  e.  ran  G )  ->  G  Fn  R )
67 fvelrnb 5586 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( G  Fn  R  ->  (
b  e.  ran  G  <->  E. u  e.  R  ( G `  u )  =  b ) )
68 nfmpt1 4125 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  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 )
) } )
696, 68nfcxfr 2429 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  F/_ w G
70 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  F/_ w u
7169, 70nffv 5548 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/_ w
( G `  u
)
72 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  F/_ w
b
7371, 72nfeq 2439 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ w
( G `  u
)  =  b
74 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  F/ u
( G `  w
)  =  b
75 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( u  =  w  ->  ( G `  u )  =  ( G `  w ) )
7675eqeq1d 2304 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( u  =  w  ->  (
( G `  u
)  =  b  <->  ( G `  w )  =  b ) )
7773, 74, 76cbvrex 2774 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( E. u  e.  R  ( G `  u )  =  b  <->  E. w  e.  R  ( G `  w )  =  b )
7867, 77syl6bb 252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( G  Fn  R  ->  (
b  e.  ran  G  <->  E. w  e.  R  ( G `  w )  =  b ) )
7966, 78syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  b  e.  ran  G )  ->  (
b  e.  ran  G  <->  E. w  e.  R  ( G `  w )  =  b ) )
8057, 79mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  b  e.  ran  G )  ->  E. w  e.  R  ( G `  w )  =  b )
8169nfrn 4937 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  F/_ w ran  G
8272, 81nfel 2440 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  F/ w  b  e.  ran  G
8358, 82nfan 1783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  F/ w
( ph  /\  b  e.  ran  G )
84 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  F/ w  b  =/=  (/)
85 simp1l 979 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  b  e.  ran  G )  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  ph )
86 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  b  e.  ran  G )  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  w  e.  R )
87 simp3 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( ( ph  /\  b  e.  ran  G )  /\  w  e.  R  /\  ( G `  w )  =  b )  -> 
( G `  w
)  =  b )
8885, 86, 873jca 1132 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( ( ph  /\  b  e.  ran  G )  /\  w  e.  R  /\  ( G `  w )  =  b )  -> 
( ph  /\  w  e.  R  /\  ( G `  w )  =  b ) )
89 simp3 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  ( G `  w )  =  b )
90 simp1 955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  ph )
91 simp2 956 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  w  e.  R )
9290, 91jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  ( ph  /\  w  e.  R ) )
93 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
ph  /\  w  e.  R )  ->  w  e.  R )
9459adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  w  e.  R )  ->  A  e.  _V )
9594, 60syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
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 )
9693, 95jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
ph  /\  w  e.  R )  ->  (
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 ) )
976fvmpt2 5624 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( ( 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 ) ) } )
9896, 97syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
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 )
) } )
997sselda 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( (
ph  /\  w  e.  R )  ->  w  e.  V )
100 stoweidlem31.5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  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 ) ) }
101100eleq2i 2360 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( w  e.  V  <->  w  e.  { 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 )
) } )
102 rabid 2729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( w  e.  { 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 )
) }  <->  ( 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 )
) ) )
103101, 102bitri 240 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( 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 )
) ) )
10499, 103sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( (
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 )
) ) )
105104simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
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 )
) )
106 stoweidlem31.10 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ph  ->  E  e.  RR+ )
107 stoweidlem31.8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( ph  ->  M  e.  NN )
108 nnrp 10379 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( M  e.  NN  ->  M  e.  RR+ )
109107, 108syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( ph  ->  M  e.  RR+ )
110106, 109jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ph  ->  ( E  e.  RR+  /\  M  e.  RR+ )
)
111 rpdivcl 10392 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( E  e.  RR+  /\  M  e.  RR+ )  ->  ( E  /  M )  e.  RR+ )
112110, 111syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ph  ->  ( E  /  M
)  e.  RR+ )
113112adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( (
ph  /\  w  e.  R )  ->  ( E  /  M )  e.  RR+ )
114105, 113jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
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 )
)  /\  ( E  /  M )  e.  RR+ ) )
115 breq2 4043 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( e  =  ( E  /  M )  ->  (
( h `  t
)  <  e  <->  ( h `  t )  <  ( E  /  M ) ) )
116115ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( e  =  ( E  /  M )  ->  ( A. t  e.  w  ( h `  t
)  <  e  <->  A. t  e.  w  ( h `  t )  <  ( E  /  M ) ) )
117 oveq2 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44  |-  ( e  =  ( E  /  M )  ->  (
1  -  e )  =  ( 1  -  ( E  /  M
) ) )
118117breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43  |-  ( e  =  ( E  /  M )  ->  (
( 1  -  e
)  <  ( h `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( h `  t
) ) )
119118ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( e  =  ( E  /  M )  ->  ( A. t  e.  ( T  \  U ) ( 1  -  e )  <  ( h `  t )  <->  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
h `  t )
) )
120116, 1193anbi23d 1255 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( 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 )
) ) )
121120rexbidv 2577 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( 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 )
) ) )
122121rspccva 2896 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( ( 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 ) ) )
123114, 122syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
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 )
) )
124 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  F/ h  w  e.  R
12531, 124nfan 1783 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  F/ h
( ph  /\  w  e.  R )
126 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  F/_ h (/)
12734, 126nfne 2552 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  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 )
) }  =/=  (/)
128 3simpc 954 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( ( ( 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 )
) ) )
129 rabid 2729 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42  |-  ( 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 ) ) ) )
130128, 129sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( ( ( 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 ) ) } )
131 ne0i 3474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( 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 ) ) }  =/=  (/) )
132130, 131syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( ( ( 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 )
) }  =/=  (/) )
1331323exp 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( (
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 ) ) }  =/=  (/) ) ) )
134125, 127, 133rexlimd 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( (
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 )
) }  =/=  (/) ) )
135123, 134mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( (
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 ) ) }  =/=  (/) )
13698, 135eqnetrd 2477 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( (
ph  /\  w  e.  R )  ->  ( G `  w )  =/=  (/) )
13792, 136syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  ( G `  w )  =/=  (/) )
13889, 137eqnetrrd 2479 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( (
ph  /\  w  e.  R  /\  ( G `  w )  =  b )  ->  b  =/=  (/) )
13988, 138syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ph  /\  b  e.  ran  G )  /\  w  e.  R  /\  ( G `  w )  =  b )  -> 
b  =/=  (/) )
1401393exp 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( (
ph  /\  b  e.  ran  G )  ->  (
w  e.  R  -> 
( ( G `  w )  =  b  ->  b  =/=  (/) ) ) )
14183, 84, 140rexlimd 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  b  e.  ran  G )  ->  ( E. w  e.  R  ( G `  w )  =  b  ->  b  =/=  (/) ) )
14280, 141mpd 14 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  b  e.  ran  G )  ->  b  =/=  (/) )
14356, 142syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
b  =/=  (/) )
144 rsp 2616 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  ->  (
b  e.  ran  G  ->  ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
145144imp 418 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  b  e.  ran  G )  -> 
( b  =/=  (/)  ->  (
l `  b )  e.  b ) )
14655, 143, 145sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
( l `  b
)  e.  b )
14754, 146jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
( b  e.  ran  G  /\  ( l `  b )  e.  b ) )
148 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  b  e. 
_V
1496elrnmpt 4942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( 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 )
) } ) )
150148, 149ax-mp 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 )
) } )
151150biimpi 186 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 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 ) ) } )
15254, 151syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
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 ) ) } )
153 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  F/ w
( l `  b
)  e.  b
15482, 153nfan 1783 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/ w
( b  e.  ran  G  /\  ( l `  b )  e.  b )
155 nfv 1609 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  F/ w
( l `  b
)  e.  Y
156 simp1r 980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( 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 )
157 simp3 957 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( 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 ) ) } )
158156, 157jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( 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  /\  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 ) ) } ) )
159 simpl 443 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( 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 )
160 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( 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 )
) } )
161159, 160eleqtrd 2372 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( 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 ) ) } )
162 fveq1 5540 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41  |-  ( h  =  ( l `  b )  ->  (
h `  t )  =  ( ( l `
 b ) `  t ) )
163162breq2d 4051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( h  =  ( l `  b )  ->  (
0  <_  ( h `  t )  <->  0  <_  ( ( l `  b
) `  t )
) )
164162breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40  |-  ( h  =  ( l `  b )  ->  (
( h `  t
)  <_  1  <->  ( (
l `  b ) `  t )  <_  1
) )
165163, 164anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( h  =  ( l `  b )  ->  (
( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )  <-> 
( 0  <_  (
( l `  b
) `  t )  /\  ( ( l `  b ) `  t
)  <_  1 ) ) )
166165ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( 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 ) ) )
167162breq1d 4049 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( h  =  ( l `  b )  ->  (
( h `  t
)  <  ( E  /  M )  <->  ( (
l `  b ) `  t )  <  ( E  /  M ) ) )
168167ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( h  =  ( l `  b )  ->  ( A. t  e.  w  ( h `  t
)  <  ( E  /  M )  <->  A. t  e.  w  ( (
l `  b ) `  t )  <  ( E  /  M ) ) )
169162breq2d 4051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39  |-  ( h  =  ( l `  b )  ->  (
( 1  -  ( E  /  M ) )  <  ( h `  t )  <->  ( 1  -  ( E  /  M ) )  < 
( ( l `  b ) `  t
) ) )
170169ralbidv 2576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38  |-  ( h  =  ( l `  b )  ->  ( A. t  e.  ( T  \  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t )  <->  A. t  e.  ( T  \  U
) ( 1  -  ( E  /  M
) )  <  (
( l `  b
) `  t )
) )
171166, 168, 1703anbi123d 1252 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37  |-  ( 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 )
) ) )
172171elrab 2936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36  |-  ( ( 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 ) ) ) )
173172biimpi 186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 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 ) ) ) )
174173simpld 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( 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 )
175173simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 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 ) ) )
176175simp1d 967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( 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 ) )
177174, 176jca 518 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( 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 ) ) )
178166elrab 2936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( 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 ) ) )
179177, 178sylibr 203 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 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 ) } )
180161, 179syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( 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 ) } )
181 stoweidlem31.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  Y  =  { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }
182180, 181syl6eleqr 2387 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( 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
)
183158, 182syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( 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 )
1841833exp 1150 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 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 ) ) )
185154, 155, 184rexlimd 2677 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 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 ) )
186147, 152, 185sylc 56 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b )  /\  b  e. 
ran  G )  -> 
( l `  b
)  e.  Y )
18753, 186syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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
)
18848, 187eqeltrrd 2371 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( 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 )
1891883exp 1150 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 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
) ) )
19047, 189reximdai 2664 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) )
19145, 190mpd 14 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 )
192 nfv 1609 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ b  h  e.  Y
193 idd 21 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( b  e.  ran  G  -> 
( h  e.  Y  ->  h  e.  Y ) )
194193a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 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 ) ) )
19547, 192, 194rexlimd 2677 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( 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 )
)
196191, 195mpd 14 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  h  e.  ran  l )  ->  h  e.  Y )
197196ex 423 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( h  e. 
ran  l  ->  h  e.  Y ) )
19842, 197ralrimi 2637 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  A. h  e.  ran  l  h  e.  Y
)
199 dfss3 3183 . . . . . . . . . . . . . . . . . . 19  |-  ( ran  l  C_  Y  <->  A. z  e.  ran  l  z  e.  Y )
200 nfcv 2432 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ h
z
201 nfrab1 2733 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ h { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }
202181, 201nfcxfr 2429 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ h Y
203200, 202nfel 2440 . . . . . . . . . . . . . . . . . . . 20  |-  F/ h  z  e.  Y
204 nfv 1609 . . . . . . . . . . . . . . . . . . . 20  |-  F/ z  h  e.  Y
205 eleq1 2356 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  h  ->  (
z  e.  Y  <->  h  e.  Y ) )
206203, 204, 205cbvral 2773 . . . . . . . . . . . . . . . . . . 19  |-  ( A. z  e.  ran  l  z  e.  Y  <->  A. h  e.  ran  l  h  e.  Y )
207199, 206bitri 240 . . . . . . . . . . . . . . . . . 18  |-  ( ran  l  C_  Y  <->  A. h  e.  ran  l  h  e.  Y )
208198, 207sylibr 203 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ran  l  C_  Y )
209208adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  b  e.  ran  G )  ->  ran  l  C_  Y )
21030, 209jca 518 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  b  e.  ran  G )  ->  ( l  Fn  ran  G  /\  ran  l  C_  Y ) )
211 df-f 5275 . . . . . . . . . . . . . . 15  |-  ( l : ran  G --> Y  <->  ( l  Fn  ran  G  /\  ran  l  C_  Y ) )
212210, 211sylibr 203 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  b  e.  ran  G )  ->  l : ran  G --> Y )
213 simpr 447 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  b  e.  ran  G )  ->  b  e.  ran  G )
214212, 213jca 518 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  b  e.  ran  G )  ->  ( l : ran  G --> Y  /\  b  e.  ran  G ) )
215 ffvelrn 5679 . . . . . . . . . . . . 13  |-  ( ( l : ran  G --> Y  /\  b  e.  ran  G )  ->  ( l `  b )  e.  Y
)
216214, 215syl 15 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  b  e.  ran  G )  ->  ( l `  b )  e.  Y
)
217216ex 423 . . . . . . . . . . 11  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( b  e. 
ran  G  ->  ( l `
 b )  e.  Y ) )
21829, 217ralrimi 2637 . . . . . . . . . 10  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  A. b  e.  ran  G ( l `  b
)  e.  Y )
21924, 218jca 518 . . . . . . . . 9  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( l  Fn 
ran  G  /\  A. b  e.  ran  G ( l `
 b )  e.  Y ) )
220 ffnfv 5701 . . . . . . . . 9  |-  ( l : ran  G --> Y  <->  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( l `  b )  e.  Y ) )
221219, 220sylibr 203 . . . . . . . 8  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  l : ran  G --> Y )
222 dffn3 5412 . . . . . . . . . . . . 13  |-  ( G  Fn  R  <->  G : R
--> ran  G )
223222biimpi 186 . . . . . . . . . . . 12  |-  ( G  Fn  R  ->  G : R --> ran  G )
22465, 223syl 15 . . . . . . . . . . 11  |-  ( ph  ->  G : R --> ran  G
)
225224adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  G : R --> ran  G )
226 stoweidlem31.9 . . . . . . . . . . . 12  |-  ( ph  ->  v : ( 1 ... M ) -1-1-onto-> R )
227 f1of 5488 . . . . . . . . . . . 12  |-  ( v : ( 1 ... M ) -1-1-onto-> R  ->  v :
( 1 ... M
) --> R )
228226, 227syl 15 . . . . . . . . . . 11  |-  ( ph  ->  v : ( 1 ... M ) --> R )
229228adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  v : ( 1 ... M ) --> R )
230225, 229jca 518 . . . . . . . . 9  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( G : R
--> ran  G  /\  v : ( 1 ... M ) --> R ) )
231 fco 5414 . . . . . . . . 9  |-  ( ( G : R --> ran  G  /\  v : ( 1 ... M ) --> R )  ->  ( G  o.  v ) : ( 1 ... M ) --> ran  G )
232230, 231syl 15 . . . . . . . 8  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( G  o.  v ) : ( 1 ... M ) --> ran  G )
233221, 232jca 518 . . . . . . 7  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( l : ran  G --> Y  /\  ( G  o.  v
) : ( 1 ... M ) --> ran 
G ) )
234 fco 5414 . . . . . . 7  |-  ( ( l : ran  G --> Y  /\  ( G  o.  v ) : ( 1 ... M ) --> ran  G )  -> 
( l  o.  ( G  o.  v )
) : ( 1 ... M ) --> Y )
235233, 234syl 15 . . . . . 6  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( l  o.  ( G  o.  v
) ) : ( 1 ... M ) --> Y )
236 stoweidlem31.2 . . . . . . . . . . 11  |-  F/ t
ph
237 nfcv 2432 . . . . . . . . . . . . 13  |-  F/_ t
l
238 nfcv 2432 . . . . . . . . . . . . . . . 16  |-  F/_ t R
239 nfra1 2606 . . . . . . . . . . . . . . . . . 18  |-  F/ t A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )
240 nfra1 2606 . . . . . . . . . . . . . . . . . 18  |-  F/ t A. t  e.  w  ( h `  t
)  <  ( E  /  M )
241 nfra1 2606 . . . . . . . . . . . . . . . . . 18  |-  F/ t A. t  e.  ( T  \  U ) ( 1  -  ( E  /  M ) )  <  ( h `  t )
242239, 240, 241nf3an 1786 . . . . . . . . . . . . . . . . 17  |-  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 ) )
243 nfcv 2432 . . . . . . . . . . . . . . . . 17  |-  F/_ t A
244242, 243nfrab 2734 . . . . . . . . . . . . . . . 16  |-  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 )
) }
245238, 244nfmpt 4124 . . . . . . . . . . . . . . 15  |-  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 )
) } )
2466, 245nfcxfr 2429 . . . . . . . . . . . . . 14  |-  F/_ t G
247246nfrn 4937 . . . . . . . . . . . . 13  |-  F/_ t ran  G
248237, 247nffn 5356 . . . . . . . . . . . 12  |-  F/ t  l  Fn  ran  G
249 nfv 1609 . . . . . . . . . . . . 13  |-  F/ t ( b  =/=  (/)  ->  (
l `  b )  e.  b )
250247, 249nfral 2609 . . . . . . . . . . . 12  |-  F/ t A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )
251248, 250nfan 1783 . . . . . . . . . . 11  |-  F/ t ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) )
252236, 251nfan 1783 . . . . . . . . . 10  |-  F/ t ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )
253 nfv 1609 . . . . . . . . . 10  |-  F/ t  i  e.  ( 1 ... M )
254252, 253nfan 1783 . . . . . . . . 9  |-  F/ t ( ( ph  /\  ( l  Fn  ran  G  /\  A. b  e. 
ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )
255232adantr 451 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( G  o.  v ) : ( 1 ... M ) --> ran  G )
256 simpr 447 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  i  e.  ( 1 ... M
) )
257255, 256jca 518 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( ( G  o.  v ) : ( 1 ... M ) --> ran  G  /\  i  e.  (
1 ... M ) ) )
258 fvco3 5612 . . . . . . . . . . . . . 14  |-  ( ( ( G  o.  v
) : ( 1 ... M ) --> ran 
G  /\  i  e.  ( 1 ... M
) )  ->  (
( l  o.  ( G  o.  v )
) `  i )  =  ( l `  ( ( G  o.  v ) `  i
) ) )
259257, 258syl 15 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
) )
260 simpll 730 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ph )
261 simplrr 737 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) )
262 ffnfv 5701 . . . . . . . . . . . . . . . . . 18  |-  ( ( G  o.  v ) : ( 1 ... M ) --> ran  G  <->  ( ( G  o.  v
)  Fn  ( 1 ... M )  /\  A. i  e.  ( 1 ... M ) ( ( G  o.  v
) `  i )  e.  ran  G ) )
263232, 262sylib 188 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  ( ( G  o.  v )  Fn  ( 1 ... M
)  /\  A. i  e.  ( 1 ... M
) ( ( G  o.  v ) `  i )  e.  ran  G ) )
264263simprd 449 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  ->  A. i  e.  ( 1 ... M ) ( ( G  o.  v ) `  i
)  e.  ran  G
)
265264r19.21bi 2654 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
266260, 261, 2653jca 1132 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( ph  /\ 
A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  (
( G  o.  v
) `  i )  e.  ran  G ) )
267 simp3 957 . . . . . . . . . . . . . . 15  |-  ( (
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
)
268 nfcv 2432 . . . . . . . . . . . . . . . 16  |-  F/_ b
( ( G  o.  v ) `  i
)
269 nfv 1609 . . . . . . . . . . . . . . . . . 18  |-  F/ b ( ( G  o.  v ) `  i
)  e.  ran  G
27025, 27, 269nf3an 1786 . . . . . . . . . . . . . . . . 17  |-  F/ b ( ph  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  (
( G  o.  v
) `  i )  e.  ran  G )
271 nfv 1609 . . . . . . . . . . . . . . . . 17  |-  F/ b ( l `  (
( G  o.  v
) `  i )
)  e.  ( ( G  o.  v ) `
 i )
272270, 271nfim 1781 . . . . . . . . . . . . . . . 16  |-  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 ) )
273 biidd 228 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  ( A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b )  <->  A. b  e.  ran  G ( b  =/=  (/)  ->  ( l `  b )  e.  b ) ) )
274 eleq1 2356 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
b  e.  ran  G  <->  ( ( G  o.  v
) `  i )  e.  ran  G ) )
275273, 2743anbi23d 1255 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) )
276 fveq2 5541 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
l `  b )  =  ( l `  ( ( G  o.  v ) `  i
) ) )
277 id 19 . . . . . . . . . . . . . . . . . 18  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  b  =  ( ( G  o.  v ) `  i ) )
278276, 277eleq12d 2364 . . . . . . . . . . . . . . . . 17  |-  ( b  =  ( ( G  o.  v ) `  i )  ->  (
( l `  b
)  e.  b  <->  ( l `  ( ( G  o.  v ) `  i
) )  e.  ( ( G  o.  v
) `  i )
) )
279275, 278imbi12d 311 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) ) )
280146a1i 10 . . . . . . . . . . . . . . . 16  |-  ( b  e.  ran  G  -> 
( ( ph  /\  A. b  e.  ran  G
( b  =/=  (/)  ->  (
l `  b )  e.  b )  /\  b  e.  ran  G )  -> 
( l `  b
)  e.  b ) )
281268, 272, 279, 280vtoclgaf 2861 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 ) ) )
282267, 281mpcom 32 . . . . . . . . . . . . . 14  |-  ( (
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 ) )
283266, 282syl 15 . . . . . . . . . . . . 13  |-  ( ( ( 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 )
)
284259, 283eqeltrd 2370 . . . . . . . . . . . 12  |-  ( ( ( 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
) )
285260, 256jca 518 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  (
l  Fn  ran  G  /\  A. b  e.  ran  G ( b  =/=  (/)  ->  (
l `  b )  e.  b ) ) )  /\  i  e.  ( 1 ... M ) )  ->  ( ph  /\  i  e.  ( 1 ... M ) ) )
286228adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  v : ( 1 ... M ) --> R )
287 simpr 447 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  i  e.  ( 1 ... M
) )
288286, 287jca 518 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
v : ( 1 ... M ) --> R  /\  i  e.  ( 1 ... M ) ) )
289 fvco3 5612 . . . . . . . . . . . . . . . . 17  |-  ( ( v : ( 1 ... M ) --> R  /\  i  e.  ( 1 ... M ) )  ->  ( ( G  o.  v ) `  i )  =  ( G `  ( v `
 i ) ) )
290288, 289syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( G  o.  v
) `  i )  =  ( G `  ( v `  i
) ) )
291 ffvelrn 5679 . . . . . . . . . . . . . . . . . . 19  |-  ( ( v : ( 1 ... M ) --> R  /\  i  e.  ( 1 ... M ) )  ->  ( v `  i )  e.  R
)
292288, 291syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
v `  i )  e.  R )
29359adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  A  e.  _V )
294 rabexg 4180 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 )
295293, 294syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
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 )
296292, 295jca 518 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  i  e.  ( 1 ... M
) )  ->  (
( 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 ) )
297 eqidd 2297 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  ( v `  i )  ->  A  =  A )
298 raleq 2749 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  ( v `  i )  ->  ( A. t  e.  w  ( h `  t
)  <  ( E  /  M )  <->  A. t  e.  ( v `  i
) ( h `  t )  <  ( E  /  M ) ) )
2992983anbi2d 1257 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 )
) ) )
300297, 299rabeqbidv 2796 . . . . . . . . . . . . . . . . . 18  |-  ( 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 )
) } )
301300, 6fvmptg 5616 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 ) ) } )
302296, 301syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
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 )
) } )
303290, 302eqtrd 2328 . . . . . . . . . . . . . . 15  |-  ( (
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 )
) } )
304285, 303syl 15 . . . . . . . . . . . . . 14  |-  ( ( ( 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 ) ) } )
305304eleq2d 2363 . . . . . . . . . . . . 13  |-  ( ( ( 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 ) ) } ) )
306 nfcv 2432 . . . . . . . . . . . . . . . . . . 19  |-  F/_ h
v
30736, 306nfco 4865 . . . . . . . . . . . . . . . . . 18  |-  F/_ h
( G  o.  v
)
30832, 307nfco 4865 . . . . . . . . . . . . . . . . 17  |-  F/_ h
( l  o.  ( G  o.  v )
)
309 nfcv 2432 . . . . . . . . . . . . . . . . 17  |-  F/_ h
i
310308, 309nffv 5548 . . . . . . . . . . . . . . . 16  |-  F/_ h
( ( l  o.  ( G  o.  v
) ) `  i
)
311 nfcv 2432 . . . . . . . . . . . . . . . 16  |-  F/_ h A
312 nfcv 2432 . . . . . . . . . . . . . . . . . 18  |-  F/_ h T
313 nfcv 2432 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ h
0
314 nfcv 2432 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ h  <_
315 nfcv 2432 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ h
t
316310, 315nffv 5548 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ h
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)
317313, 314, 316nfbr 4083 . . . . . . . . . . . . . . . . . . 19  |-  F/ h
0  <_  ( (
( l  o.  ( G  o.  v )
) `  i ) `  t )
318 nfcv 2432 . . . . . . . . . . . . . . . . . . . 20  |-  F/_ h
1
319316, 314, 318nfbr 4083 . . . . . . . . . . . . . . . . . . 19  |-  F/ h
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1
320317, 319nfan 1783 . . . . . . . . . . . . . . . . . 18  |-  F/ h
( 0  <_  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )  /\  ( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1 )
321312, 320nfral 2609 . . . . . . . . . . . . . . . . 17  |-  F/ h A. t  e.  T  ( 0  <_  (
( ( l  o.  ( G  o.  v
) ) `  i
) `  t )  /\  ( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <_  1 )
322 nfcv 2432 . . . . . . . . . . . . . . . . . 18  |-  F/_ h
( v `  i
)
323 nfcv 2432 . . . . . . . . . . . . . . . . . . 19  |-  F/_ h  <
324 nfcv 2432 . . . . . . . . . . . . . . . . . . 19  |-  F/_ h
( E  /  M
)
325316, 323, 324nfbr 4083 . . . . . . . . . . . . . . . . . 18  |-  F/ h
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <  ( E  /  M )
326322, 325nfral 2609 . . . . . . . . . . . . . . . . 17  |-  F/ h A. t  e.  (
v `  i )
( ( ( l  o.  ( G  o.  v ) ) `  i ) `  t
)  <  ( E  /  M )
327 nfcv 2432 . . . . . . . . . . . . . . . . . 18  |-  F/_ h
( T  \  U
)
328 nfcv 2432 . . . . . . . . . . . . . . . . . . 19  |-  F/_ h
( 1  -  ( E  /  M ) )
329328, 323, 316nfbr 4083 . . . . . . . . . . . . . . . . . 18  |-  F/ h
( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )
330327, 329nfral 2609 . . . . . . . . . . . . . . . . 17  |-  F/ h A. t  e.  ( T  \  U ) ( 1  -  ( E  /  M ) )  <  ( ( ( l  o.  ( G  o.  v ) ) `
 i ) `  t )
331321, 326, 330nf3an 1786 . . . . . . . . . . . . . . . 16  |-  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 ) )
332 nfcv 2432 . . . . . . . . . . . . . . . . . . 19  |-  F/_ t
h
333 nfcv 2432 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/_ t
v
334246, 333nfco 4865 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ t
( G  o.  v
)
335237, 334nfco 4865 . . . . . . . . . . . . . . . . . . . 20