Metamath Proof Explorer

Theorem stoweidlem57

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)

Ref Expression
Hypotheses 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 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 ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem57.1 
 |-  F/_ t D
2 stoweidlem57.2 
 |-  F/_ t U
3 stoweidlem57.3 
 |-  F/ t ph
4 stoweidlem57.4 
 |-  Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
5 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 ) ) }
6 stoweidlem57.6 
 |-  K = ( topGen ` ran (,) )
7 stoweidlem57.7 
 |-  T = U. J
8 stoweidlem57.8 
 |-  C = ( J Cn K )
9 stoweidlem57.9 
 |-  U = ( T \ B )
10 stoweidlem57.10 
 |-  ( ph -> J e. Comp )
11 stoweidlem57.11 
 |-  ( ph -> A C_ C )
12 stoweidlem57.12 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
13 stoweidlem57.13 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
14 stoweidlem57.14 
 |-  ( ( ph /\ a e. RR ) -> ( t e. T |-> a ) e. A )
15 stoweidlem57.15 
 |-  ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
16 stoweidlem57.16 
 |-  ( ph -> B e. ( Clsd ` J ) )
17 stoweidlem57.17 
 |-  ( ph -> D e. ( Clsd ` J ) )
18 stoweidlem57.18 
 |-  ( ph -> ( B i^i D ) = (/) )
19 stoweidlem57.19 
 |-  ( ph -> D =/= (/) )
20 stoweidlem57.20 
 |-  ( ph -> E e. RR+ )
21 stoweidlem57.21 
 |-  ( ph -> E < ( 1 / 3 ) )
22 1 nfcri 
 |-  F/ t s e. D
23 3 22 nfan 
 |-  F/ t ( ph /\ s e. D )
24 10 adantr 
 |-  ( ( ph /\ s e. D ) -> J e. Comp )
25 11 adantr 
 |-  ( ( ph /\ s e. D ) -> A C_ C )
26 12 3adant1r 
 |-  ( ( ( ph /\ s e. D ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
27 13 3adant1r 
 |-  ( ( ( ph /\ s e. D ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
28 14 adantlr 
 |-  ( ( ( ph /\ s e. D ) /\ a e. RR ) -> ( t e. T |-> a ) e. A )
29 15 adantlr 
 |-  ( ( ( ph /\ s e. D ) /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
30 cmptop 
 |-  ( J e. Comp -> J e. Top )
31 7 iscld 
 |-  ( J e. Top -> ( B e. ( Clsd ` J ) <-> ( B C_ T /\ ( T \ B ) e. J ) ) )
32 10 30 31 3syl 
 |-  ( ph -> ( B e. ( Clsd ` J ) <-> ( B C_ T /\ ( T \ B ) e. J ) ) )
33 16 32 mpbid 
 |-  ( ph -> ( B C_ T /\ ( T \ B ) e. J ) )
34 33 simprd 
 |-  ( ph -> ( T \ B ) e. J )
35 9 34 eqeltrid 
 |-  ( ph -> U e. J )
36 35 adantr 
 |-  ( ( ph /\ s e. D ) -> U e. J )
37 7 cldss 
 |-  ( D e. ( Clsd ` J ) -> D C_ T )
38 17 37 syl 
 |-  ( ph -> D C_ T )
39 38 sselda 
 |-  ( ( ph /\ s e. D ) -> s e. T )
40 disjr 
 |-  ( ( B i^i D ) = (/) <-> A. s e. D -. s e. B )
41 18 40 sylib 
 |-  ( ph -> A. s e. D -. s e. B )
42 41 r19.21bi 
 |-  ( ( ph /\ s e. D ) -> -. s e. B )
43 39 42 eldifd 
 |-  ( ( ph /\ s e. D ) -> s e. ( T \ B ) )
44 43 9 eleqtrrdi 
 |-  ( ( ph /\ s e. D ) -> s e. U )
45 2 23 6 24 7 8 25 26 27 28 29 36 44 stoweidlem56 
 |-  ( ( 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 ) ) ) )
46 simpl 
 |-  ( ( 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 )
47 simprll 
 |-  ( ( 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 )
48 simprr 
 |-  ( ( 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 ) ) )
49 5 reqabi 
 |-  ( 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 ) ) ) )
50 46 48 49 sylanbrc 
 |-  ( ( 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 )
51 46 47 50 jca32 
 |-  ( ( 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 ) ) )
52 51 reximi2 
 |-  ( 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 ) )
53 rexex 
 |-  ( E. w e. J ( s e. w /\ w e. V ) -> E. w ( s e. w /\ w e. V ) )
54 45 52 53 3syl 
 |-  ( ( ph /\ s e. D ) -> E. w ( s e. w /\ w e. V ) )
55 nfcv 
 |-  F/_ w s
56 nfrab1 
 |-  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 ) ) }
57 5 56 nfcxfr 
 |-  F/_ w V
58 55 57 elunif 
 |-  ( s e. U. V <-> E. w ( s e. w /\ w e. V ) )
59 54 58 sylibr 
 |-  ( ( ph /\ s e. D ) -> s e. U. V )
60 59 ex 
 |-  ( ph -> ( s e. D -> s e. U. V ) )
61 60 ssrdv 
 |-  ( ph -> D C_ U. V )
62 cmpcld 
 |-  ( ( J e. Comp /\ D e. ( Clsd ` J ) ) -> ( J |`t D ) e. Comp )
63 10 17 62 syl2anc 
 |-  ( ph -> ( J |`t D ) e. Comp )
64 10 30 syl 
 |-  ( ph -> J e. Top )
65 7 cmpsub 
 |-  ( ( J e. Top /\ D C_ T ) -> ( ( J |`t D ) e. Comp <-> A. k e. ~P J ( D C_ U. k -> E. u e. ( ~P k i^i Fin ) D C_ U. u ) ) )
66 64 38 65 syl2anc 
 |-  ( ph -> ( ( J |`t D ) e. Comp <-> A. k e. ~P J ( D C_ U. k -> E. u e. ( ~P k i^i Fin ) D C_ U. u ) ) )
67 63 66 mpbid 
 |-  ( ph -> A. k e. ~P J ( D C_ U. k -> E. u e. ( ~P k i^i Fin ) D C_ U. u ) )
68 ssrab2 
 |-  { 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
69 5 68 eqsstri 
 |-  V C_ J
70 5 10 rabexd 
 |-  ( ph -> V e. _V )
71 elpwg 
 |-  ( V e. _V -> ( V e. ~P J <-> V C_ J ) )
72 70 71 syl 
 |-  ( ph -> ( V e. ~P J <-> V C_ J ) )
73 69 72 mpbiri 
 |-  ( ph -> V e. ~P J )
74 unieq 
 |-  ( k = V -> U. k = U. V )
75 74 sseq2d 
 |-  ( k = V -> ( D C_ U. k <-> D C_ U. V ) )
76 pweq 
 |-  ( k = V -> ~P k = ~P V )
77 76 ineq1d 
 |-  ( k = V -> ( ~P k i^i Fin ) = ( ~P V i^i Fin ) )
78 77 rexeqdv 
 |-  ( 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 ) )
79 75 78 imbi12d 
 |-  ( 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 ) ) )
80 79 rspccva 
 |-  ( ( 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 ) )
81 67 73 80 syl2anc 
 |-  ( ph -> ( D C_ U. V -> E. u e. ( ~P V i^i Fin ) D C_ U. u ) )
82 61 81 mpd 
 |-  ( ph -> E. u e. ( ~P V i^i Fin ) D C_ U. u )
83 elinel1 
 |-  ( u e. ( ~P V i^i Fin ) -> u e. ~P V )
84 elpwi 
 |-  ( u e. ~P V -> u C_ V )
85 84 ssdifssd 
 |-  ( u e. ~P V -> ( u \ { (/) } ) C_ V )
86 vex 
 |-  u e. _V
87 difexg 
 |-  ( u e. _V -> ( u \ { (/) } ) e. _V )
88 86 87 ax-mp 
 |-  ( u \ { (/) } ) e. _V
89 88 elpw 
 |-  ( ( u \ { (/) } ) e. ~P V <-> ( u \ { (/) } ) C_ V )
90 85 89 sylibr 
 |-  ( u e. ~P V -> ( u \ { (/) } ) e. ~P V )
91 83 90 syl 
 |-  ( u e. ( ~P V i^i Fin ) -> ( u \ { (/) } ) e. ~P V )
92 elinel2 
 |-  ( u e. ( ~P V i^i Fin ) -> u e. Fin )
93 diffi 
 |-  ( u e. Fin -> ( u \ { (/) } ) e. Fin )
94 92 93 syl 
 |-  ( u e. ( ~P V i^i Fin ) -> ( u \ { (/) } ) e. Fin )
95 91 94 elind 
 |-  ( u e. ( ~P V i^i Fin ) -> ( u \ { (/) } ) e. ( ~P V i^i Fin ) )
96 95 3ad2ant2 
 |-  ( ( ph /\ u e. ( ~P V i^i Fin ) /\ D C_ U. u ) -> ( u \ { (/) } ) e. ( ~P V i^i Fin ) )
97 unidif0 
 |-  U. ( u \ { (/) } ) = U. u
98 97 sseq2i 
 |-  ( D C_ U. ( u \ { (/) } ) <-> D C_ U. u )
99 98 biimpri 
 |-  ( D C_ U. u -> D C_ U. ( u \ { (/) } ) )
100 99 3ad2ant3 
 |-  ( ( ph /\ u e. ( ~P V i^i Fin ) /\ D C_ U. u ) -> D C_ U. ( u \ { (/) } ) )
101 eldifsni 
 |-  ( w e. ( u \ { (/) } ) -> w =/= (/) )
102 101 rgen 
 |-  A. w e. ( u \ { (/) } ) w =/= (/)
103 102 a1i 
 |-  ( ( ph /\ u e. ( ~P V i^i Fin ) /\ D C_ U. u ) -> A. w e. ( u \ { (/) } ) w =/= (/) )
104 unieq 
 |-  ( r = ( u \ { (/) } ) -> U. r = U. ( u \ { (/) } ) )
105 104 sseq2d 
 |-  ( r = ( u \ { (/) } ) -> ( D C_ U. r <-> D C_ U. ( u \ { (/) } ) ) )
106 raleq 
 |-  ( r = ( u \ { (/) } ) -> ( A. w e. r w =/= (/) <-> A. w e. ( u \ { (/) } ) w =/= (/) ) )
107 105 106 anbi12d 
 |-  ( r = ( u \ { (/) } ) -> ( ( D C_ U. r /\ A. w e. r w =/= (/) ) <-> ( D C_ U. ( u \ { (/) } ) /\ A. w e. ( u \ { (/) } ) w =/= (/) ) ) )
108 107 rspcev 
 |-  ( ( ( 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 =/= (/) ) )
109 96 100 103 108 syl12anc 
 |-  ( ( 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 =/= (/) ) )
110 109 rexlimdv3a 
 |-  ( 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 =/= (/) ) ) )
111 82 110 mpd 
 |-  ( ph -> E. r e. ( ~P V i^i Fin ) ( D C_ U. r /\ A. w e. r w =/= (/) ) )
112 nfv 
 |-  F/ h ph
113 nfcv 
 |-  F/_ h RR+
114 nfre1 
 |-  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 ) )
115 113 114 nfralw 
 |-  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 ) )
116 nfcv 
 |-  F/_ h J
117 115 116 nfrabw 
 |-  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 ) ) }
118 5 117 nfcxfr 
 |-  F/_ h V
119 118 nfpw 
 |-  F/_ h ~P V
120 nfcv 
 |-  F/_ h Fin
121 119 120 nfin 
 |-  F/_ h ( ~P V i^i Fin )
122 121 nfcri 
 |-  F/ h r e. ( ~P V i^i Fin )
123 nfv 
 |-  F/ h ( D C_ U. r /\ A. w e. r w =/= (/) )
124 112 122 123 nf3an 
 |-  F/ h ( ph /\ r e. ( ~P V i^i Fin ) /\ ( D C_ U. r /\ A. w e. r w =/= (/) ) )
125 nfcv 
 |-  F/_ t RR+
126 nfcv 
 |-  F/_ t A
127 nfra1 
 |-  F/ t A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 )
128 nfra1 
 |-  F/ t A. t e. w ( h ` t ) < e
129 nfra1 
 |-  F/ t A. t e. ( T \ U ) ( 1 - e ) < ( h ` t )
130 127 128 129 nf3an 
 |-  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 ) )
131 126 130 nfrexw 
 |-  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 ) )
132 125 131 nfralw 
 |-  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 ) )
133 nfcv 
 |-  F/_ t J
134 132 133 nfrabw 
 |-  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 ) ) }
135 5 134 nfcxfr 
 |-  F/_ t V
136 135 nfpw 
 |-  F/_ t ~P V
137 nfcv 
 |-  F/_ t Fin
138 136 137 nfin 
 |-  F/_ t ( ~P V i^i Fin )
139 138 nfcri 
 |-  F/ t r e. ( ~P V i^i Fin )
140 nfcv 
 |-  F/_ t U. r
141 1 140 nfss 
 |-  F/ t D C_ U. r
142 nfv 
 |-  F/ t A. w e. r w =/= (/)
143 141 142 nfan 
 |-  F/ t ( D C_ U. r /\ A. w e. r w =/= (/) )
144 3 139 143 nf3an 
 |-  F/ t ( ph /\ r e. ( ~P V i^i Fin ) /\ ( D C_ U. r /\ A. w e. r w =/= (/) ) )
145 nfv 
 |-  F/ w ph
146 57 nfpw 
 |-  F/_ w ~P V
147 nfcv 
 |-  F/_ w Fin
148 146 147 nfin 
 |-  F/_ w ( ~P V i^i Fin )
149 148 nfcri 
 |-  F/ w r e. ( ~P V i^i Fin )
150 nfv 
 |-  F/ w D C_ U. r
151 nfra1 
 |-  F/ w A. w e. r w =/= (/)
152 150 151 nfan 
 |-  F/ w ( D C_ U. r /\ A. w e. r w =/= (/) )
153 145 149 152 nf3an 
 |-  F/ w ( ph /\ r e. ( ~P V i^i Fin ) /\ ( D C_ U. r /\ A. w e. r w =/= (/) ) )
154 simp2 
 |-  ( ( ph /\ r e. ( ~P V i^i Fin ) /\ ( D C_ U. r /\ A. w e. r w =/= (/) ) ) -> r e. ( ~P V i^i Fin ) )
155 simp3l 
 |-  ( ( ph /\ r e. ( ~P V i^i Fin ) /\ ( D C_ U. r /\ A. w e. r w =/= (/) ) ) -> D C_ U. r )
156 19 3ad2ant1 
 |-  ( ( ph /\ r e. ( ~P V i^i Fin ) /\ ( D C_ U. r /\ A. w e. r w =/= (/) ) ) -> D =/= (/) )
157 20 3ad2ant1 
 |-  ( ( ph /\ r e. ( ~P V i^i Fin ) /\ ( D C_ U. r /\ A. w e. r w =/= (/) ) ) -> E e. RR+ )
158 33 simpld 
 |-  ( ph -> B C_ T )
159 158 3ad2ant1 
 |-  ( ( ph /\ r e. ( ~P V i^i Fin ) /\ ( D C_ U. r /\ A. w e. r w =/= (/) ) ) -> B C_ T )
160 70 3ad2ant1 
 |-  ( ( ph /\ r e. ( ~P V i^i Fin ) /\ ( D C_ U. r /\ A. w e. r w =/= (/) ) ) -> V e. _V )
161 retop 
 |-  ( topGen ` ran (,) ) e. Top
162 6 161 eqeltri 
 |-  K e. Top
163 cnfex 
 |-  ( ( J e. Top /\ K e. Top ) -> ( J Cn K ) e. _V )
164 64 162 163 sylancl 
 |-  ( ph -> ( J Cn K ) e. _V )
165 11 8 sseqtrdi 
 |-  ( ph -> A C_ ( J Cn K ) )
166 164 165 ssexd 
 |-  ( ph -> A e. _V )
167 166 3ad2ant1 
 |-  ( ( ph /\ r e. ( ~P V i^i Fin ) /\ ( D C_ U. r /\ A. w e. r w =/= (/) ) ) -> A e. _V )
168 124 144 153 9 4 5 154 155 156 157 159 160 167 stoweidlem39 
 |-  ( ( 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 ) ) ) ) )
169 168 rexlimdv3a 
 |-  ( 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 ) ) ) ) ) )
170 111 169 mpd 
 |-  ( 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 ) ) ) ) )
171 nfv 
 |-  F/ i ( ph /\ m e. NN )
172 nfv 
 |-  F/ i v : ( 1 ... m ) --> V
173 nfv 
 |-  F/ i D C_ U. ran v
174 nfv 
 |-  F/ i y : ( 1 ... m ) --> Y
175 nfra1 
 |-  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 ) )
176 174 175 nfan 
 |-  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 ) ) )
177 176 nfex 
 |-  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 ) ) )
178 172 173 177 nf3an 
 |-  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 ) ) ) )
179 171 178 nfan 
 |-  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 ) ) ) ) )
180 nfv 
 |-  F/ t m e. NN
181 3 180 nfan 
 |-  F/ t ( ph /\ m e. NN )
182 nfcv 
 |-  F/_ t v
183 nfcv 
 |-  F/_ t ( 1 ... m )
184 182 183 135 nff 
 |-  F/ t v : ( 1 ... m ) --> V
185 nfcv 
 |-  F/_ t U. ran v
186 1 185 nfss 
 |-  F/ t D C_ U. ran v
187 nfcv 
 |-  F/_ t y
188 127 126 nfrabw 
 |-  F/_ t { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }
189 4 188 nfcxfr 
 |-  F/_ t Y
190 187 183 189 nff 
 |-  F/ t y : ( 1 ... m ) --> Y
191 nfra1 
 |-  F/ t A. t e. ( v ` i ) ( ( y ` i ) ` t ) < ( E / m )
192 nfra1 
 |-  F/ t A. t e. B ( 1 - ( E / m ) ) < ( ( y ` i ) ` t )
193 191 192 nfan 
 |-  F/ t ( A. t e. ( v ` i ) ( ( y ` i ) ` t ) < ( E / m ) /\ A. t e. B ( 1 - ( E / m ) ) < ( ( y ` i ) ` t ) )
194 183 193 nfralw 
 |-  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 ) )
195 190 194 nfan 
 |-  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 ) ) )
196 195 nfex 
 |-  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 ) ) )
197 184 186 196 nf3an 
 |-  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 ) ) ) )
198 181 197 nfan 
 |-  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 ) ) ) ) )
199 nfv 
 |-  F/ y ( ph /\ m e. NN )
200 nfv 
 |-  F/ y v : ( 1 ... m ) --> V
201 nfv 
 |-  F/ y D C_ U. ran v
202 nfe1 
 |-  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 ) ) )
203 200 201 202 nf3an 
 |-  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 ) ) ) )
204 199 203 nfan 
 |-  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 ) ) ) ) )
205 nfv 
 |-  F/ w ( ph /\ m e. NN )
206 nfcv 
 |-  F/_ w v
207 nfcv 
 |-  F/_ w ( 1 ... m )
208 206 207 57 nff 
 |-  F/ w v : ( 1 ... m ) --> V
209 nfv 
 |-  F/ w D C_ U. ran v
210 nfv 
 |-  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 ) ) )
211 208 209 210 nf3an 
 |-  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 ) ) ) )
212 205 211 nfan 
 |-  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 ) ) ) ) )
213 eqid 
 |-  { 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 ) }
214 eqid 
 |-  ( 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 ) ) ) )
215 eqid 
 |-  ( t e. T |-> ( i e. ( 1 ... m ) |-> ( ( y ` i ) ` t ) ) ) = ( t e. T |-> ( i e. ( 1 ... m ) |-> ( ( y ` i ) ` t ) ) )
216 eqid 
 |-  ( 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 ) )
217 simp1ll 
 |-  ( ( ( ( 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 )
218 217 13 syld3an1 
 |-  ( ( ( ( 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 )
219 11 sselda 
 |-  ( ( ph /\ f e. A ) -> f e. C )
220 6 7 8 219 fcnre 
 |-  ( ( ph /\ f e. A ) -> f : T --> RR )
221 220 ad4ant14 
 |-  ( ( ( ( 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 )
222 simplr 
 |-  ( ( ( 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 )
223 simpr1 
 |-  ( ( ( 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 )
224 7 cldss 
 |-  ( B e. ( Clsd ` J ) -> B C_ T )
225 16 224 syl 
 |-  ( ph -> B C_ T )
226 225 ad2antrr 
 |-  ( ( ( 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 )
227 simpr2 
 |-  ( ( ( 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 )
228 38 ad2antrr 
 |-  ( ( ( 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 )
229 feq3 
 |-  ( 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 ) } ) )
230 4 229 ax-mp 
 |-  ( y : ( 1 ... m ) --> Y <-> y : ( 1 ... m ) --> { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) } )
231 230 biimpi 
 |-  ( y : ( 1 ... m ) --> Y -> y : ( 1 ... m ) --> { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) } )
232 231 anim1i 
 |-  ( ( 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 ) ) ) )
233 232 eximi 
 |-  ( 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 ) ) ) )
234 233 3ad2ant3 
 |-  ( ( 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 234 adantl 
 |-  ( ( ( 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 ) ) ) )
236 10 uniexd 
 |-  ( ph -> U. J e. _V )
237 7 236 eqeltrid 
 |-  ( ph -> T e. _V )
238 237 ad2antrr 
 |-  ( ( ( 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 )
239 20 ad2antrr 
 |-  ( ( ( 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 21 ad2antrr 
 |-  ( ( ( 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 ) )
241 179 198 204 212 7 213 214 215 216 5 218 221 222 223 226 227 228 235 238 239 240 stoweidlem54 
 |-  ( ( ( 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 ) ) )
242 241 ex 
 |-  ( ( 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 ) ) ) )
243 242 exlimdv 
 |-  ( ( 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 ) ) ) )
244 243 rexlimdva 
 |-  ( 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 ) ) ) )
245 170 244 mpd 
 |-  ( 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 ) ) )