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

Theorem stoweidlem57 31724
Description: There exists a function x as in the proof of Lemma 2 in [BrosowskiDeutsh] p. 91. In this theorem, it is proven the non-trivial case (the closed set D is nonempty). Here D is used to represent A in the paper, because the variable A is used for the subalgebra of functions. (Contributed by Glauco Siliprandi, 20-Apr-2017.)
Hypotheses
Ref Expression
stoweidlem57.1  |-  F/_ t D
stoweidlem57.2  |-  F/_ t U
stoweidlem57.3  |-  F/ t
ph
stoweidlem57.4  |-  Y  =  { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }
stoweidlem57.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 ) ) }
stoweidlem57.6  |-  K  =  ( topGen `  ran  (,) )
stoweidlem57.7  |-  T  = 
U. J
stoweidlem57.8  |-  C  =  ( J  Cn  K
)
stoweidlem57.9  |-  U  =  ( T  \  B
)
stoweidlem57.10  |-  ( ph  ->  J  e.  Comp )
stoweidlem57.11  |-  ( ph  ->  A  C_  C )
stoweidlem57.12  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  +  ( g `  t ) ) )  e.  A )
stoweidlem57.13  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  x.  ( g `  t ) ) )  e.  A )
stoweidlem57.14  |-  ( (
ph  /\  a  e.  RR )  ->  ( t  e.  T  |->  a )  e.  A )
stoweidlem57.15  |-  ( (
ph  /\  ( r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
stoweidlem57.16  |-  ( ph  ->  B  e.  ( Clsd `  J ) )
stoweidlem57.17  |-  ( ph  ->  D  e.  ( Clsd `  J ) )
stoweidlem57.18  |-  ( ph  ->  ( B  i^i  D
)  =  (/) )
stoweidlem57.19  |-  ( ph  ->  D  =/=  (/) )
stoweidlem57.20  |-  ( ph  ->  E  e.  RR+ )
stoweidlem57.21  |-  ( ph  ->  E  <  ( 1  /  3 ) )
Assertion
Ref Expression
stoweidlem57  |-  ( ph  ->  E. x  e.  A  ( A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 )  /\  A. t  e.  D  ( x `  t )  <  E  /\  A. t  e.  B  ( 1  -  E
)  <  ( x `  t ) ) )
Distinct variable groups:    e, a,
f, t    q, a,
r, f, t, A    A, e, f, t    D, a, e, f    T, a, e, f, t    U, a, e, f    ph, a,
e, f    e, g, h, f, t, A    w, e, h, t, A    e, E, f, g, h, t   
g, r, h, A   
x, f, g, h, t, A    B, f,
g, r    f, V, g, r    f, Y, g, r    g, q, D    D, h, r    g, J, h, t    T, g, h, r    U, g, h, r    ph, g, h, r    w, r, E    A, q    D, q    T, q    U, q    ph, q    w, D    w, B    t, K    ph, w    w, J    w, T    w, U    w, Y    x, B    x, D    x, E    x, T
Allowed substitution hints:    ph( x, t)    B( t, e, h, q, a)    C( x, w, t, e, f, g, h, r, q, a)    D( t)    U( x, t)    E( q, a)    J( x, e, f, r, q, a)    K( x, w, e, f, g, h, r, q, a)    V( x, w, t, e, h, q, a)    Y( x, t, e, h, q, a)

Proof of Theorem stoweidlem57
Dummy variables  s  m  i  v  y  u  k are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 stoweidlem57.2 . . . . . . . . . 10  |-  F/_ t U
2 stoweidlem57.3 . . . . . . . . . . 11  |-  F/ t
ph
3 stoweidlem57.1 . . . . . . . . . . . 12  |-  F/_ t D
43nfcri 2596 . . . . . . . . . . 11  |-  F/ t  s  e.  D
52, 4nfan 1912 . . . . . . . . . 10  |-  F/ t ( ph  /\  s  e.  D )
6 stoweidlem57.6 . . . . . . . . . 10  |-  K  =  ( topGen `  ran  (,) )
7 stoweidlem57.10 . . . . . . . . . . 11  |-  ( ph  ->  J  e.  Comp )
87adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  D )  ->  J  e.  Comp )
9 stoweidlem57.7 . . . . . . . . . 10  |-  T  = 
U. J
10 stoweidlem57.8 . . . . . . . . . 10  |-  C  =  ( J  Cn  K
)
11 stoweidlem57.11 . . . . . . . . . . 11  |-  ( ph  ->  A  C_  C )
1211adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  D )  ->  A  C_  C )
13 stoweidlem57.12 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  +  ( g `  t ) ) )  e.  A )
14133adant1r 1220 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  D )  /\  f  e.  A  /\  g  e.  A )  ->  (
t  e.  T  |->  ( ( f `  t
)  +  ( g `
 t ) ) )  e.  A )
15 stoweidlem57.13 . . . . . . . . . . 11  |-  ( (
ph  /\  f  e.  A  /\  g  e.  A
)  ->  ( t  e.  T  |->  ( ( f `  t )  x.  ( g `  t ) ) )  e.  A )
16153adant1r 1220 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  D )  /\  f  e.  A  /\  g  e.  A )  ->  (
t  e.  T  |->  ( ( f `  t
)  x.  ( g `
 t ) ) )  e.  A )
17 stoweidlem57.14 . . . . . . . . . . 11  |-  ( (
ph  /\  a  e.  RR )  ->  ( t  e.  T  |->  a )  e.  A )
1817adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  D )  /\  a  e.  RR )  ->  (
t  e.  T  |->  a )  e.  A )
19 stoweidlem57.15 . . . . . . . . . . 11  |-  ( (
ph  /\  ( r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
2019adantlr 714 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  D )  /\  (
r  e.  T  /\  t  e.  T  /\  r  =/=  t ) )  ->  E. q  e.  A  ( q `  r
)  =/=  ( q `
 t ) )
21 stoweidlem57.9 . . . . . . . . . . . 12  |-  U  =  ( T  \  B
)
22 stoweidlem57.16 . . . . . . . . . . . . . 14  |-  ( ph  ->  B  e.  ( Clsd `  J ) )
23 cmptop 19761 . . . . . . . . . . . . . . 15  |-  ( J  e.  Comp  ->  J  e. 
Top )
249iscld 19394 . . . . . . . . . . . . . . 15  |-  ( J  e.  Top  ->  ( B  e.  ( Clsd `  J )  <->  ( B  C_  T  /\  ( T 
\  B )  e.  J ) ) )
257, 23, 243syl 20 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  e.  (
Clsd `  J )  <->  ( B  C_  T  /\  ( T  \  B )  e.  J ) ) )
2622, 25mpbid 210 . . . . . . . . . . . . 13  |-  ( ph  ->  ( B  C_  T  /\  ( T  \  B
)  e.  J ) )
2726simprd 463 . . . . . . . . . . . 12  |-  ( ph  ->  ( T  \  B
)  e.  J )
2821, 27syl5eqel 2533 . . . . . . . . . . 11  |-  ( ph  ->  U  e.  J )
2928adantr 465 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  D )  ->  U  e.  J )
30 stoweidlem57.17 . . . . . . . . . . . . . 14  |-  ( ph  ->  D  e.  ( Clsd `  J ) )
319cldss 19396 . . . . . . . . . . . . . 14  |-  ( D  e.  ( Clsd `  J
)  ->  D  C_  T
)
3230, 31syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  D  C_  T )
3332sselda 3486 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  D )  ->  s  e.  T )
34 stoweidlem57.18 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( B  i^i  D
)  =  (/) )
35 disjr 3850 . . . . . . . . . . . . . 14  |-  ( ( B  i^i  D )  =  (/)  <->  A. s  e.  D  -.  s  e.  B
)
3634, 35sylib 196 . . . . . . . . . . . . 13  |-  ( ph  ->  A. s  e.  D  -.  s  e.  B
)
3736r19.21bi 2810 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  D )  ->  -.  s  e.  B )
3833, 37eldifd 3469 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  D )  ->  s  e.  ( T  \  B
) )
3938, 21syl6eleqr 2540 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  D )  ->  s  e.  U )
401, 5, 6, 8, 9, 10, 12, 14, 16, 18, 20, 29, 39stoweidlem56 31723 . . . . . . . . 9  |-  ( (
ph  /\  s  e.  D )  ->  E. w  e.  J  ( (
s  e.  w  /\  w  C_  U )  /\  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 )
) ) )
41 simpl 457 . . . . . . . . . . 11  |-  ( ( w  e.  J  /\  ( ( s  e.  w  /\  w  C_  U )  /\  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 )
42 simprll 761 . . . . . . . . . . 11  |-  ( ( w  e.  J  /\  ( ( s  e.  w  /\  w  C_  U )  /\  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 )
) ) )  -> 
s  e.  w )
43 simprr 756 . . . . . . . . . . . 12  |-  ( ( w  e.  J  /\  ( ( s  e.  w  /\  w  C_  U )  /\  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 )
) ) )  ->  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 )
) )
44 stoweidlem57.5 . . . . . . . . . . . . 13  |-  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 ) ) }
4544rabeq2i 3090 . . . . . . . . . . . 12  |-  ( 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 )
) ) )
4641, 43, 45sylanbrc 664 . . . . . . . . . . 11  |-  ( ( w  e.  J  /\  ( ( s  e.  w  /\  w  C_  U )  /\  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.  V )
4741, 42, 46jca32 535 . . . . . . . . . 10  |-  ( ( w  e.  J  /\  ( ( s  e.  w  /\  w  C_  U )  /\  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  /\  ( s  e.  w  /\  w  e.  V
) ) )
4847reximi2 2908 . . . . . . . . 9  |-  ( E. w  e.  J  ( ( s  e.  w  /\  w  C_  U )  /\  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. w  e.  J  ( s  e.  w  /\  w  e.  V
) )
49 rexex 2898 . . . . . . . . 9  |-  ( E. w  e.  J  ( s  e.  w  /\  w  e.  V )  ->  E. w ( s  e.  w  /\  w  e.  V ) )
5040, 48, 493syl 20 . . . . . . . 8  |-  ( (
ph  /\  s  e.  D )  ->  E. w
( s  e.  w  /\  w  e.  V
) )
51 nfcv 2603 . . . . . . . . 9  |-  F/_ w
s
52 nfrab1 3022 . . . . . . . . . 10  |-  F/_ w { 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 ) ) }
5344, 52nfcxfr 2601 . . . . . . . . 9  |-  F/_ w V
5451, 53elunif 31338 . . . . . . . 8  |-  ( s  e.  U. V  <->  E. w
( s  e.  w  /\  w  e.  V
) )
5550, 54sylibr 212 . . . . . . 7  |-  ( (
ph  /\  s  e.  D )  ->  s  e.  U. V )
5655ex 434 . . . . . 6  |-  ( ph  ->  ( s  e.  D  ->  s  e.  U. V
) )
5756ssrdv 3492 . . . . 5  |-  ( ph  ->  D  C_  U. V )
58 cmpcld 19768 . . . . . . . 8  |-  ( ( J  e.  Comp  /\  D  e.  ( Clsd `  J
) )  ->  ( Jt  D )  e.  Comp )
597, 30, 58syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( Jt  D )  e.  Comp )
607, 23syl 16 . . . . . . . 8  |-  ( ph  ->  J  e.  Top )
619cmpsub 19766 . . . . . . . 8  |-  ( ( J  e.  Top  /\  D  C_  T )  -> 
( ( Jt  D )  e.  Comp  <->  A. k  e.  ~P  J ( D  C_  U. k  ->  E. u  e.  ( ~P k  i^i 
Fin ) D  C_  U. u ) ) )
6260, 32, 61syl2anc 661 . . . . . . 7  |-  ( ph  ->  ( ( Jt  D )  e.  Comp  <->  A. k  e.  ~P  J ( D  C_  U. k  ->  E. u  e.  ( ~P k  i^i 
Fin ) D  C_  U. u ) ) )
6359, 62mpbid 210 . . . . . 6  |-  ( ph  ->  A. k  e.  ~P  J ( D  C_  U. k  ->  E. u  e.  ( ~P k  i^i 
Fin ) D  C_  U. u ) )
64 ssrab2 3567 . . . . . . . 8  |-  { 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 )
) }  C_  J
6544, 64eqsstri 3516 . . . . . . 7  |-  V  C_  J
6644, 7rabexd 4585 . . . . . . . 8  |-  ( ph  ->  V  e.  _V )
67 elpwg 4001 . . . . . . . 8  |-  ( V  e.  _V  ->  ( V  e.  ~P J  <->  V 
C_  J ) )
6866, 67syl 16 . . . . . . 7  |-  ( ph  ->  ( V  e.  ~P J 
<->  V  C_  J )
)
6965, 68mpbiri 233 . . . . . 6  |-  ( ph  ->  V  e.  ~P J
)
70 unieq 4238 . . . . . . . . 9  |-  ( k  =  V  ->  U. k  =  U. V )
7170sseq2d 3514 . . . . . . . 8  |-  ( k  =  V  ->  ( D  C_  U. k  <->  D  C_  U. V
) )
72 pweq 3996 . . . . . . . . . 10  |-  ( k  =  V  ->  ~P k  =  ~P V
)
7372ineq1d 3681 . . . . . . . . 9  |-  ( k  =  V  ->  ( ~P k  i^i  Fin )  =  ( ~P V  i^i  Fin ) )
7473rexeqdv 3045 . . . . . . . 8  |-  ( k  =  V  ->  ( E. u  e.  ( ~P k  i^i  Fin ) D  C_  U. u  <->  E. u  e.  ( ~P V  i^i  Fin ) D  C_  U. u
) )
7571, 74imbi12d 320 . . . . . . 7  |-  ( k  =  V  ->  (
( D  C_  U. k  ->  E. u  e.  ( ~P k  i^i  Fin ) D  C_  U. u
)  <->  ( D  C_  U. V  ->  E. u  e.  ( ~P V  i^i  Fin ) D  C_  U. u
) ) )
7675rspccva 3193 . . . . . 6  |-  ( ( A. k  e.  ~P  J ( D  C_  U. k  ->  E. u  e.  ( ~P k  i^i 
Fin ) D  C_  U. u )  /\  V  e.  ~P J )  -> 
( D  C_  U. V  ->  E. u  e.  ( ~P V  i^i  Fin ) D  C_  U. u
) )
7763, 69, 76syl2anc 661 . . . . 5  |-  ( ph  ->  ( D  C_  U. V  ->  E. u  e.  ( ~P V  i^i  Fin ) D  C_  U. u
) )
7857, 77mpd 15 . . . 4  |-  ( ph  ->  E. u  e.  ( ~P V  i^i  Fin ) D  C_  U. u
)
79 elinel1 31372 . . . . . . . . 9  |-  ( u  e.  ( ~P V  i^i  Fin )  ->  u  e.  ~P V )
80 elpwi 4002 . . . . . . . . . . 11  |-  ( u  e.  ~P V  ->  u  C_  V )
8180ssdifssd 3624 . . . . . . . . . 10  |-  ( u  e.  ~P V  -> 
( u  \  { (/)
} )  C_  V
)
82 vex 3096 . . . . . . . . . . . 12  |-  u  e. 
_V
83 difexg 4581 . . . . . . . . . . . 12  |-  ( u  e.  _V  ->  (
u  \  { (/) } )  e.  _V )
8482, 83ax-mp 5 . . . . . . . . . . 11  |-  ( u 
\  { (/) } )  e.  _V
8584elpw 3999 . . . . . . . . . 10  |-  ( ( u  \  { (/) } )  e.  ~P V  <->  ( u  \  { (/) } )  C_  V )
8681, 85sylibr 212 . . . . . . . . 9  |-  ( u  e.  ~P V  -> 
( u  \  { (/)
} )  e.  ~P V )
8779, 86syl 16 . . . . . . . 8  |-  ( u  e.  ( ~P V  i^i  Fin )  ->  (
u  \  { (/) } )  e.  ~P V )
88 elinel2 31371 . . . . . . . . 9  |-  ( u  e.  ( ~P V  i^i  Fin )  ->  u  e.  Fin )
89 diffi 7749 . . . . . . . . 9  |-  ( u  e.  Fin  ->  (
u  \  { (/) } )  e.  Fin )
9088, 89syl 16 . . . . . . . 8  |-  ( u  e.  ( ~P V  i^i  Fin )  ->  (
u  \  { (/) } )  e.  Fin )
9187, 90elind 3670 . . . . . . 7  |-  ( u  e.  ( ~P V  i^i  Fin )  ->  (
u  \  { (/) } )  e.  ( ~P V  i^i  Fin ) )
92913ad2ant2 1017 . . . . . 6  |-  ( (
ph  /\  u  e.  ( ~P V  i^i  Fin )  /\  D  C_  U. u
)  ->  ( u  \  { (/) } )  e.  ( ~P V  i^i  Fin ) )
93 unidif0 4606 . . . . . . . . 9  |-  U. (
u  \  { (/) } )  =  U. u
9493sseq2i 3511 . . . . . . . 8  |-  ( D 
C_  U. ( u  \  { (/) } )  <->  D  C_  U. u
)
9594biimpri 206 . . . . . . 7  |-  ( D 
C_  U. u  ->  D  C_ 
U. ( u  \  { (/) } ) )
96953ad2ant3 1018 . . . . . 6  |-  ( (
ph  /\  u  e.  ( ~P V  i^i  Fin )  /\  D  C_  U. u
)  ->  D  C_  U. (
u  \  { (/) } ) )
97 eldifsni 4137 . . . . . . . 8  |-  ( w  e.  ( u  \  { (/) } )  ->  w  =/=  (/) )
9897rgen 2801 . . . . . . 7  |-  A. w  e.  ( u  \  { (/)
} ) w  =/=  (/)
9998a1i 11 . . . . . 6  |-  ( (
ph  /\  u  e.  ( ~P V  i^i  Fin )  /\  D  C_  U. u
)  ->  A. w  e.  ( u  \  { (/)
} ) w  =/=  (/) )
100 unieq 4238 . . . . . . . . 9  |-  ( r  =  ( u  \  { (/) } )  ->  U. r  =  U. ( u  \  { (/) } ) )
101100sseq2d 3514 . . . . . . . 8  |-  ( r  =  ( u  \  { (/) } )  -> 
( D  C_  U. r  <->  D 
C_  U. ( u  \  { (/) } ) ) )
102 raleq 3038 . . . . . . . 8  |-  ( r  =  ( u  \  { (/) } )  -> 
( A. w  e.  r  w  =/=  (/)  <->  A. w  e.  ( u  \  { (/)
} ) w  =/=  (/) ) )
103101, 102anbi12d 710 . . . . . . 7  |-  ( r  =  ( u  \  { (/) } )  -> 
( ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) )  <->  ( D  C_  U. ( u  \  { (/)
} )  /\  A. w  e.  ( u  \  { (/) } ) w  =/=  (/) ) ) )
104103rspcev 3194 . . . . . 6  |-  ( ( ( u  \  { (/)
} )  e.  ( ~P V  i^i  Fin )  /\  ( D  C_  U. ( u  \  { (/)
} )  /\  A. w  e.  ( u  \  { (/) } ) w  =/=  (/) ) )  ->  E. r  e.  ( ~P V  i^i  Fin )
( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )
10592, 96, 99, 104syl12anc 1225 . . . . 5  |-  ( (
ph  /\  u  e.  ( ~P V  i^i  Fin )  /\  D  C_  U. u
)  ->  E. r  e.  ( ~P V  i^i  Fin ) ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )
106105rexlimdv3a 2935 . . . 4  |-  ( ph  ->  ( E. u  e.  ( ~P V  i^i  Fin ) D  C_  U. u  ->  E. r  e.  ( ~P V  i^i  Fin ) ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) ) )
10778, 106mpd 15 . . 3  |-  ( ph  ->  E. r  e.  ( ~P V  i^i  Fin ) ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )
108 nfv 1692 . . . . . 6  |-  F/ h ph
109 nfcv 2603 . . . . . . . . . . . 12  |-  F/_ h RR+
110 nfre1 2902 . . . . . . . . . . . 12  |-  F/ h 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 ) )
111109, 110nfral 2827 . . . . . . . . . . 11  |-  F/ h 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 )
)
112 nfcv 2603 . . . . . . . . . . 11  |-  F/_ h J
113111, 112nfrab 3023 . . . . . . . . . 10  |-  F/_ h { 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 ) ) }
11444, 113nfcxfr 2601 . . . . . . . . 9  |-  F/_ h V
115114nfpw 4005 . . . . . . . 8  |-  F/_ h ~P V
116 nfcv 2603 . . . . . . . 8  |-  F/_ h Fin
117115, 116nfin 3687 . . . . . . 7  |-  F/_ h
( ~P V  i^i  Fin )
118117nfcri 2596 . . . . . 6  |-  F/ h  r  e.  ( ~P V  i^i  Fin )
119 nfv 1692 . . . . . 6  |-  F/ h
( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) )
120108, 118, 119nf3an 1914 . . . . 5  |-  F/ h
( ph  /\  r  e.  ( ~P V  i^i  Fin )  /\  ( D 
C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )
121 nfcv 2603 . . . . . . . . . . . 12  |-  F/_ t RR+
122 nfcv 2603 . . . . . . . . . . . . 13  |-  F/_ t A
123 nfra1 2822 . . . . . . . . . . . . . 14  |-  F/ t A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 )
124 nfra1 2822 . . . . . . . . . . . . . 14  |-  F/ t A. t  e.  w  ( h `  t
)  <  e
125 nfra1 2822 . . . . . . . . . . . . . 14  |-  F/ t A. t  e.  ( T  \  U ) ( 1  -  e
)  <  ( h `  t )
126123, 124, 125nf3an 1914 . . . . . . . . . . . . 13  |-  F/ t ( 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 ) )
127122, 126nfrex 2904 . . . . . . . . . . . 12  |-  F/ t 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 ) )
128121, 127nfral 2827 . . . . . . . . . . 11  |-  F/ t 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 ) )
129 nfcv 2603 . . . . . . . . . . 11  |-  F/_ t J
130128, 129nfrab 3023 . . . . . . . . . 10  |-  F/_ 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 ) ) }
13144, 130nfcxfr 2601 . . . . . . . . 9  |-  F/_ t V
132131nfpw 4005 . . . . . . . 8  |-  F/_ t ~P V
133 nfcv 2603 . . . . . . . 8  |-  F/_ t Fin
134132, 133nfin 3687 . . . . . . 7  |-  F/_ t
( ~P V  i^i  Fin )
135134nfcri 2596 . . . . . 6  |-  F/ t  r  e.  ( ~P V  i^i  Fin )
136 nfcv 2603 . . . . . . . 8  |-  F/_ t U. r
1373, 136nfss 3479 . . . . . . 7  |-  F/ t  D  C_  U. r
138 nfv 1692 . . . . . . 7  |-  F/ t A. w  e.  r  w  =/=  (/)
139137, 138nfan 1912 . . . . . 6  |-  F/ t ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) )
1402, 135, 139nf3an 1914 . . . . 5  |-  F/ t ( ph  /\  r  e.  ( ~P V  i^i  Fin )  /\  ( D 
C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )
141 nfv 1692 . . . . . 6  |-  F/ w ph
14253nfpw 4005 . . . . . . . 8  |-  F/_ w ~P V
143 nfcv 2603 . . . . . . . 8  |-  F/_ w Fin
144142, 143nfin 3687 . . . . . . 7  |-  F/_ w
( ~P V  i^i  Fin )
145144nfcri 2596 . . . . . 6  |-  F/ w  r  e.  ( ~P V  i^i  Fin )
146 nfv 1692 . . . . . . 7  |-  F/ w  D  C_  U. r
147 nfra1 2822 . . . . . . 7  |-  F/ w A. w  e.  r  w  =/=  (/)
148146, 147nfan 1912 . . . . . 6  |-  F/ w
( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) )
149141, 145, 148nf3an 1914 . . . . 5  |-  F/ w
( ph  /\  r  e.  ( ~P V  i^i  Fin )  /\  ( D 
C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )
150 stoweidlem57.4 . . . . 5  |-  Y  =  { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }
151 simp2 996 . . . . 5  |-  ( (
ph  /\  r  e.  ( ~P V  i^i  Fin )  /\  ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )  ->  r  e.  ( ~P V  i^i  Fin ) )
152 simp3l 1023 . . . . 5  |-  ( (
ph  /\  r  e.  ( ~P V  i^i  Fin )  /\  ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )  ->  D  C_ 
U. r )
153 stoweidlem57.19 . . . . . 6  |-  ( ph  ->  D  =/=  (/) )
1541533ad2ant1 1016 . . . . 5  |-  ( (
ph  /\  r  e.  ( ~P V  i^i  Fin )  /\  ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )  ->  D  =/=  (/) )
155 stoweidlem57.20 . . . . . 6  |-  ( ph  ->  E  e.  RR+ )
1561553ad2ant1 1016 . . . . 5  |-  ( (
ph  /\  r  e.  ( ~P V  i^i  Fin )  /\  ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )  ->  E  e.  RR+ )
15726simpld 459 . . . . . 6  |-  ( ph  ->  B  C_  T )
1581573ad2ant1 1016 . . . . 5  |-  ( (
ph  /\  r  e.  ( ~P V  i^i  Fin )  /\  ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )  ->  B  C_  T )
159663ad2ant1 1016 . . . . 5  |-  ( (
ph  /\  r  e.  ( ~P V  i^i  Fin )  /\  ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )  ->  V  e.  _V )
160 retop 21134 . . . . . . . . 9  |-  ( topGen ` 
ran  (,) )  e.  Top
1616, 160eqeltri 2525 . . . . . . . 8  |-  K  e. 
Top
162 cnfex 31350 . . . . . . . 8  |-  ( ( J  e.  Top  /\  K  e.  Top )  ->  ( J  Cn  K
)  e.  _V )
16360, 161, 162sylancl 662 . . . . . . 7  |-  ( ph  ->  ( J  Cn  K
)  e.  _V )
16411, 10syl6sseq 3532 . . . . . . 7  |-  ( ph  ->  A  C_  ( J  Cn  K ) )
165163, 164ssexd 4580 . . . . . 6  |-  ( ph  ->  A  e.  _V )
1661653ad2ant1 1016 . . . . 5  |-  ( (
ph  /\  r  e.  ( ~P V  i^i  Fin )  /\  ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )  ->  A  e.  _V )
167120, 140, 149, 21, 150, 44, 151, 152, 154, 156, 158, 159, 166stoweidlem39 31706 . . . 4  |-  ( (
ph  /\  r  e.  ( ~P V  i^i  Fin )  /\  ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) ) )  ->  E. m  e.  NN  E. v ( v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )
168167rexlimdv3a 2935 . . 3  |-  ( ph  ->  ( E. r  e.  ( ~P V  i^i  Fin ) ( D  C_  U. r  /\  A. w  e.  r  w  =/=  (/) )  ->  E. m  e.  NN  E. v ( v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) ) )
169107, 168mpd 15 . 2  |-  ( ph  ->  E. m  e.  NN  E. v ( v : ( 1 ... m
) --> V  /\  D  C_ 
U. ran  v  /\  E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )
170 nfv 1692 . . . . . . 7  |-  F/ i ( ph  /\  m  e.  NN )
171 nfv 1692 . . . . . . . 8  |-  F/ i  v : ( 1 ... m ) --> V
172 nfv 1692 . . . . . . . 8  |-  F/ i  D  C_  U. ran  v
173 nfv 1692 . . . . . . . . . 10  |-  F/ i  y : ( 1 ... m ) --> Y
174 nfra1 2822 . . . . . . . . . 10  |-  F/ i A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) )
175173, 174nfan 1912 . . . . . . . . 9  |-  F/ i ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) )
176175nfex 1932 . . . . . . . 8  |-  F/ i E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) )
177171, 172, 176nf3an 1914 . . . . . . 7  |-  F/ i ( v : ( 1 ... m ) --> V  /\  D  C_  U.
ran  v  /\  E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) )
178170, 177nfan 1912 . . . . . 6  |-  F/ i ( ( ph  /\  m  e.  NN )  /\  ( v : ( 1 ... m ) --> V  /\  D  C_  U.
ran  v  /\  E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )
179 nfv 1692 . . . . . . . 8  |-  F/ t  m  e.  NN
1802, 179nfan 1912 . . . . . . 7  |-  F/ t ( ph  /\  m  e.  NN )
181 nfcv 2603 . . . . . . . . 9  |-  F/_ t
v
182 nfcv 2603 . . . . . . . . 9  |-  F/_ t
( 1 ... m
)
183181, 182, 131nff 5713 . . . . . . . 8  |-  F/ t  v : ( 1 ... m ) --> V
184 nfcv 2603 . . . . . . . . 9  |-  F/_ t U. ran  v
1853, 184nfss 3479 . . . . . . . 8  |-  F/ t  D  C_  U. ran  v
186 nfcv 2603 . . . . . . . . . . 11  |-  F/_ t
y
187123, 122nfrab 3023 . . . . . . . . . . . 12  |-  F/_ t { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }
188150, 187nfcxfr 2601 . . . . . . . . . . 11  |-  F/_ t Y
189186, 182, 188nff 5713 . . . . . . . . . 10  |-  F/ t  y : ( 1 ... m ) --> Y
190 nfra1 2822 . . . . . . . . . . . 12  |-  F/ t A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )
191 nfra1 2822 . . . . . . . . . . . 12  |-  F/ t A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t )
192190, 191nfan 1912 . . . . . . . . . . 11  |-  F/ t ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) )
193182, 192nfral 2827 . . . . . . . . . 10  |-  F/ t A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) )
194189, 193nfan 1912 . . . . . . . . 9  |-  F/ t ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) )
195194nfex 1932 . . . . . . . 8  |-  F/ t E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) )
196183, 185, 195nf3an 1914 . . . . . . 7  |-  F/ t ( v : ( 1 ... m ) --> V  /\  D  C_  U.
ran  v  /\  E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) )
197180, 196nfan 1912 . . . . . 6  |-  F/ t ( ( ph  /\  m  e.  NN )  /\  ( v : ( 1 ... m ) --> V  /\  D  C_  U.
ran  v  /\  E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )
198 nfv 1692 . . . . . . 7  |-  F/ y ( ph  /\  m  e.  NN )
199 nfv 1692 . . . . . . . 8  |-  F/ y  v : ( 1 ... m ) --> V
200 nfv 1692 . . . . . . . 8  |-  F/ y  D  C_  U. ran  v
201 nfe1 1824 . . . . . . . 8  |-  F/ y E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) )
202199, 200, 201nf3an 1914 . . . . . . 7  |-  F/ y ( v : ( 1 ... m ) --> V  /\  D  C_  U.
ran  v  /\  E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) )
203198, 202nfan 1912 . . . . . 6  |-  F/ y ( ( ph  /\  m  e.  NN )  /\  ( v : ( 1 ... m ) --> V  /\  D  C_  U.
ran  v  /\  E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )
204 nfv 1692 . . . . . . 7  |-  F/ w
( ph  /\  m  e.  NN )
205 nfcv 2603 . . . . . . . . 9  |-  F/_ w
v
206 nfcv 2603 . . . . . . . . 9  |-  F/_ w
( 1 ... m
)
207205, 206, 53nff 5713 . . . . . . . 8  |-  F/ w  v : ( 1 ... m ) --> V
208 nfv 1692 . . . . . . . 8  |-  F/ w  D  C_  U. ran  v
209 nfv 1692 . . . . . . . 8  |-  F/ w E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) )
210207, 208, 209nf3an 1914 . . . . . . 7  |-  F/ w
( v : ( 1 ... m ) --> V  /\  D  C_  U.
ran  v  /\  E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) )
211204, 210nfan 1912 . . . . . 6  |-  F/ w
( ( ph  /\  m  e.  NN )  /\  ( v : ( 1 ... m ) --> V  /\  D  C_  U.
ran  v  /\  E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )
212 eqid 2441 . . . . . 6  |-  { h  e.  A  |  A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) }  =  { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }
213 eqid 2441 . . . . . 6  |-  ( f  e.  { h  e.  A  |  A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) } , 
g  e.  { h  e.  A  |  A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) }  |->  ( t  e.  T  |->  ( ( f `  t
)  x.  ( g `
 t ) ) ) )  =  ( f  e.  { h  e.  A  |  A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) } , 
g  e.  { h  e.  A  |  A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) }  |->  ( t  e.  T  |->  ( ( f `  t
)  x.  ( g `
 t ) ) ) )
214 eqid 2441 . . . . . 6  |-  ( t  e.  T  |->  ( i  e.  ( 1 ... m )  |->  ( ( y `  i ) `
 t ) ) )  =  ( t  e.  T  |->  ( i  e.  ( 1 ... m )  |->  ( ( y `  i ) `
 t ) ) )
215 eqid 2441 . . . . . 6  |-  ( t  e.  T  |->  (  seq 1 (  x.  , 
( ( t  e.  T  |->  ( i  e.  ( 1 ... m
)  |->  ( ( y `
 i ) `  t ) ) ) `
 t ) ) `
 m ) )  =  ( t  e.  T  |->  (  seq 1
(  x.  ,  ( ( t  e.  T  |->  ( i  e.  ( 1 ... m ) 
|->  ( ( y `  i ) `  t
) ) ) `  t ) ) `  m ) )
216 simp1ll 1058 . . . . . . 7  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  ( v : ( 1 ... m ) --> V  /\  D  C_  U.
ran  v  /\  E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )  /\  f  e.  A  /\  g  e.  A )  ->  ph )
217216, 15syld3an1 1273 . . . . . 6  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  ( v : ( 1 ... m ) --> V  /\  D  C_  U.
ran  v  /\  E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )  /\  f  e.  A  /\  g  e.  A )  ->  (
t  e.  T  |->  ( ( f `  t
)  x.  ( g `
 t ) ) )  e.  A )
21811sselda 3486 . . . . . . . 8  |-  ( (
ph  /\  f  e.  A )  ->  f  e.  C )
2196, 9, 10, 218fcnre 31347 . . . . . . 7  |-  ( (
ph  /\  f  e.  A )  ->  f : T --> RR )
220219adant423 31375 . . . . . 6  |-  ( ( ( ( ph  /\  m  e.  NN )  /\  ( v : ( 1 ... m ) --> V  /\  D  C_  U.
ran  v  /\  E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )  /\  f  e.  A )  ->  f : T --> RR )
221 simplr 754 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )  ->  m  e.  NN )
222 simpr1 1001 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )  ->  v : ( 1 ... m ) --> V )
2239cldss 19396 . . . . . . . 8  |-  ( B  e.  ( Clsd `  J
)  ->  B  C_  T
)
22422, 223syl 16 . . . . . . 7  |-  ( ph  ->  B  C_  T )
225224ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )  ->  B  C_  T )
226 simpr2 1002 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )  ->  D  C_ 
U. ran  v )
22732ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )  ->  D  C_  T )
228 feq3 5701 . . . . . . . . . . . 12  |-  ( Y  =  { h  e.  A  |  A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) }  ->  ( y : ( 1 ... m ) --> Y  <-> 
y : ( 1 ... m ) --> { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) } ) )
229150, 228ax-mp 5 . . . . . . . . . . 11  |-  ( y : ( 1 ... m ) --> Y  <->  y :
( 1 ... m
) --> { h  e.  A  |  A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) } )
230229biimpi 194 . . . . . . . . . 10  |-  ( y : ( 1 ... m ) --> Y  -> 
y : ( 1 ... m ) --> { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) } )
231230anim1i 568 . . . . . . . . 9  |-  ( ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) )  ->  ( y : ( 1 ... m
) --> { h  e.  A  |  A. t  e.  T  ( 0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) }  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) )
232231eximi 1641 . . . . . . . 8  |-  ( E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) )  ->  E. y ( y : ( 1 ... m ) --> { h  e.  A  |  A. t  e.  T  (
0  <_  ( h `  t )  /\  (
h `  t )  <_  1 ) }  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) )
2332323ad2ant3 1018 . . . . . . 7  |-  ( ( v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) )  ->  E. y
( y : ( 1 ... m ) --> { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) )
234233adantl 466 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )  ->  E. y
( y : ( 1 ... m ) --> { h  e.  A  |  A. t  e.  T  ( 0  <_  (
h `  t )  /\  ( h `  t
)  <_  1 ) }  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) )
235 uniexg 6578 . . . . . . . . 9  |-  ( J  e.  Comp  ->  U. J  e.  _V )
2367, 235syl 16 . . . . . . . 8  |-  ( ph  ->  U. J  e.  _V )
2379, 236syl5eqel 2533 . . . . . . 7  |-  ( ph  ->  T  e.  _V )
238237ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )  ->  T  e.  _V )
239155ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )  ->  E  e.  RR+ )
240 stoweidlem57.21 . . . . . . 7  |-  ( ph  ->  E  <  ( 1  /  3 ) )
241240ad2antrr 725 . . . . . 6  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )  ->  E  <  ( 1  /  3
) )
242178, 197, 203, 211, 9, 212, 213, 214, 215, 44, 217, 220, 221, 222, 225, 226, 227, 234, 238, 239, 241stoweidlem54 31721 . . . . 5  |-  ( ( ( ph  /\  m  e.  NN )  /\  (
v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) ) )  ->  E. x  e.  A  ( A. t  e.  T  (
0  <_  ( x `  t )  /\  (
x `  t )  <_  1 )  /\  A. t  e.  D  (
x `  t )  <  E  /\  A. t  e.  B  ( 1  -  E )  < 
( x `  t
) ) )
243242ex 434 . . . 4  |-  ( (
ph  /\  m  e.  NN )  ->  ( ( v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) )  ->  E. x  e.  A  ( A. t  e.  T  (
0  <_  ( x `  t )  /\  (
x `  t )  <_  1 )  /\  A. t  e.  D  (
x `  t )  <  E  /\  A. t  e.  B  ( 1  -  E )  < 
( x `  t
) ) ) )
244243exlimdv 1709 . . 3  |-  ( (
ph  /\  m  e.  NN )  ->  ( E. v ( v : ( 1 ... m
) --> V  /\  D  C_ 
U. ran  v  /\  E. y ( y : ( 1 ... m
) --> Y  /\  A. i  e.  ( 1 ... m ) ( A. t  e.  ( v `  i ) ( ( y `  i ) `  t
)  <  ( E  /  m )  /\  A. t  e.  B  (
1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) )  ->  E. x  e.  A  ( A. t  e.  T  (
0  <_  ( x `  t )  /\  (
x `  t )  <_  1 )  /\  A. t  e.  D  (
x `  t )  <  E  /\  A. t  e.  B  ( 1  -  E )  < 
( x `  t
) ) ) )
245244rexlimdva 2933 . 2  |-  ( ph  ->  ( E. m  e.  NN  E. v ( v : ( 1 ... m ) --> V  /\  D  C_  U. ran  v  /\  E. y ( y : ( 1 ... m ) --> Y  /\  A. i  e.  ( 1 ... m
) ( A. t  e.  ( v `  i
) ( ( y `
 i ) `  t )  <  ( E  /  m )  /\  A. t  e.  B  ( 1  -  ( E  /  m ) )  <  ( ( y `
 i ) `  t ) ) ) )  ->  E. x  e.  A  ( A. t  e.  T  (
0  <_  ( x `  t )  /\  (
x `  t )  <_  1 )  /\  A. t  e.  D  (
x `  t )  <  E  /\  A. t  e.  B  ( 1  -  E )  < 
( x `  t
) ) ) )
246169, 245mpd 15 1  |-  ( ph  ->  E. x  e.  A  ( A. t  e.  T  ( 0  <_  (
x `  t )  /\  ( x `  t
)  <_  1 )  /\  A. t  e.  D  ( x `  t )  <  E  /\  A. t  e.  B  ( 1  -  E
)  <  ( x `  t ) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 972    = wceq 1381   E.wex 1597   F/wnf 1601    e. wcel 1802   F/_wnfc 2589    =/= wne 2636   A.wral 2791   E.wrex 2792   {crab 2795   _Vcvv 3093    \ cdif 3455    i^i cin 3457    C_ wss 3458   (/)c0 3767   ~Pcpw 3993   {csn 4010   U.cuni 4230   class class class wbr 4433    |-> cmpt 4491   ran crn 4986   -->wf 5570   ` cfv 5574  (class class class)co 6277    |-> cmpt2 6279   Fincfn 7514   RRcr 9489   0cc0 9490   1c1 9491    + caddc 9493    x. cmul 9495    < clt 9626    <_ cle 9627    - cmin 9805    / cdiv 10207   NNcn 10537   3c3 10587   RR+crp 11224   (,)cioo 11533   ...cfz 11676    seqcseq 12081   ↾t crest 14690   topGenctg 14707   Topctop 19261   Clsdccld 19383    Cn ccn 19591   Compccmp 19752
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-8 1804  ax-9 1806  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419  ax-rep 4544  ax-sep 4554  ax-nul 4562  ax-pow 4611  ax-pr 4672  ax-un 6573  ax-inf2 8056  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567  ax-pre-sup 9568  ax-mulf 9570
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 973  df-3an 974  df-tru 1384  df-fal 1387  df-ex 1598  df-nf 1602  df-sb 1725  df-eu 2270  df-mo 2271  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-ne 2638  df-nel 2639  df-ral 2796  df-rex 2797  df-reu 2798  df-rmo 2799  df-rab 2800  df-v 3095  df-sbc 3312  df-csb 3418  df-dif 3461  df-un 3463  df-in 3465  df-ss 3472  df-pss 3474  df-nul 3768  df-if 3923  df-pw 3995  df-sn 4011  df-pr 4013  df-tp 4015  df-op 4017  df-uni 4231  df-int 4268  df-iun 4313  df-iin 4314  df-br 4434  df-opab 4492  df-mpt 4493  df-tr 4527  df-eprel 4777  df-id 4781  df-po 4786  df-so 4787  df-fr 4824  df-se 4825  df-we 4826  df-ord 4867  df-on 4868  df-lim 4869  df-suc 4870  df-xp 4991  df-rel 4992  df-cnv 4993  df-co 4994  df-dm 4995  df-rn 4996  df-res 4997  df-ima 4998  df-iota 5537  df-fun 5576  df-fn 5577  df-f 5578  df-f1 5579  df-fo 5580  df-f1o 5581  df-fv 5582  df-isom 5583  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-of 6521  df-om 6682  df-1st 6781  df-2nd 6782  df-supp 6900  df-recs 7040  df-rdg 7074  df-1o 7128  df-2o 7129  df-oadd 7132  df-er 7309  df-map 7420  df-pm 7421  df-ixp 7468  df-en 7515  df-dom 7516  df-sdom 7517  df-fin 7518  df-fsupp 7828  df-fi 7869  df-sup 7899  df-oi 7933  df-card 8318  df-cda 8546  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9807  df-neg 9808  df-div 10208  df-nn 10538  df-2 10595  df-3 10596  df-4 10597  df-5 10598  df-6 10599  df-7 10600  df-8 10601  df-9 10602  df-10 10603  df-n0 10797  df-z 10866  df-dec 10980  df-uz 11086  df-q 11187  df-rp 11225  df-xneg 11322  df-xadd 11323  df-xmul 11324  df-ioo 11537  df-ico 11539  df-icc 11540  df-fz 11677  df-fzo 11799  df-fl 11903  df-seq 12082  df-exp 12141  df-hash 12380  df-cj 12906  df-re 12907  df-im 12908  df-sqrt 13042  df-abs 13043  df-clim 13285  df-rlim 13286  df-sum 13483  df-struct 14506  df-ndx 14507  df-slot 14508  df-base 14509  df-sets 14510  df-ress 14511  df-plusg 14582  df-mulr 14583  df-starv 14584  df-sca 14585  df-vsca 14586  df-ip 14587  df-tset 14588  df-ple 14589  df-ds 14591  df-unif 14592  df-hom 14593  df-cco 14594  df-rest 14692  df-topn 14693  df-0g 14711  df-gsum 14712  df-topgen 14713  df-pt 14714  df-prds 14717  df-xrs 14771  df-qtop 14776  df-imas 14777  df-xps 14779  df-mre 14855  df-mrc 14856  df-acs 14858  df-mgm 15741  df-sgrp 15780  df-mnd 15790  df-submnd 15836  df-mulg 15929  df-cntz 16224  df-cmn 16669  df-psmet 18279  df-xmet 18280  df-met 18281  df-bl 18282  df-mopn 18283  df-cnfld 18289  df-top 19266  df-bases 19268  df-topon 19269  df-topsp 19270  df-cld 19386  df-cn 19594  df-cnp 19595  df-cmp 19753  df-tx 19929  df-hmeo 20122  df-xms 20689  df-ms 20690  df-tms 20691
This theorem is referenced by:  stoweidlem58  31725
  Copyright terms: Public domain W3C validator