Metamath Proof Explorer

Theorem stoweidlem59

Description: This lemma proves that there exists a function x as in the proof in BrosowskiDeutsh p. 91, after Lemma 2: x_j is in the subalgebra, 0 <= x_j <= 1, x_j < ε / n on A_j (meaning A in the paper), x_j > 1 - \epsilon / n on B_j. Here D is used to represent A in the paper (because A is used for the subalgebra of functions), E is used to represent ε. (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem59.1 
|- F/_ t F
stoweidlem59.2 
|- F/ t ph
stoweidlem59.3 
|- K = ( topGen ` ran (,) )
stoweidlem59.4 
|- T = U. J
stoweidlem59.5 
|- C = ( J Cn K )
stoweidlem59.6 
|- D = ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
stoweidlem59.7 
|- B = ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
stoweidlem59.8 
|- Y = { y e. A | A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) }
stoweidlem59.9 
|- H = ( j e. ( 0 ... N ) |-> { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } )
stoweidlem59.10 
|- ( ph -> J e. Comp )
stoweidlem59.11 
|- ( ph -> A C_ C )
stoweidlem59.12 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
stoweidlem59.13 
|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
stoweidlem59.14 
|- ( ( ph /\ y e. RR ) -> ( t e. T |-> y ) e. A )
stoweidlem59.15 
|- ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
stoweidlem59.16 
|- ( ph -> F e. C )
stoweidlem59.17 
|- ( ph -> E e. RR+ )
stoweidlem59.18 
|- ( ph -> E < ( 1 / 3 ) )
stoweidlem59.19 
|- ( ph -> N e. NN )
Assertion stoweidlem59 
|- ( ph -> E. x ( x : ( 0 ... N ) --> A /\ A. j e. ( 0 ... N ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( x ` j ) ` t ) ) ) )

Proof

Step Hyp Ref Expression
1 stoweidlem59.1 
 |-  F/_ t F
2 stoweidlem59.2 
 |-  F/ t ph
3 stoweidlem59.3 
 |-  K = ( topGen ` ran (,) )
4 stoweidlem59.4 
 |-  T = U. J
5 stoweidlem59.5 
 |-  C = ( J Cn K )
6 stoweidlem59.6 
 |-  D = ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
7 stoweidlem59.7 
 |-  B = ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
8 stoweidlem59.8 
 |-  Y = { y e. A | A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) }
9 stoweidlem59.9 
 |-  H = ( j e. ( 0 ... N ) |-> { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } )
10 stoweidlem59.10 
 |-  ( ph -> J e. Comp )
11 stoweidlem59.11 
 |-  ( ph -> A C_ C )
12 stoweidlem59.12 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
13 stoweidlem59.13 
 |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
14 stoweidlem59.14 
 |-  ( ( ph /\ y e. RR ) -> ( t e. T |-> y ) e. A )
15 stoweidlem59.15 
 |-  ( ( ph /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
16 stoweidlem59.16 
 |-  ( ph -> F e. C )
17 stoweidlem59.17 
 |-  ( ph -> E e. RR+ )
18 stoweidlem59.18 
 |-  ( ph -> E < ( 1 / 3 ) )
19 stoweidlem59.19 
 |-  ( ph -> N e. NN )
20 nfrab1 
 |-  F/_ y { y e. A | A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) }
21 8 20 nfcxfr 
 |-  F/_ y Y
22 nfcv 
 |-  F/_ z Y
23 nfv 
 |-  F/ z ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) )
24 nfv 
 |-  F/ y ( A. t e. ( D ` j ) ( z ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( z ` t ) )
25 fveq1 
 |-  ( y = z -> ( y ` t ) = ( z ` t ) )
26 25 breq1d 
 |-  ( y = z -> ( ( y ` t ) < ( E / N ) <-> ( z ` t ) < ( E / N ) ) )
27 26 ralbidv 
 |-  ( y = z -> ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) <-> A. t e. ( D ` j ) ( z ` t ) < ( E / N ) ) )
28 25 breq2d 
 |-  ( y = z -> ( ( 1 - ( E / N ) ) < ( y ` t ) <-> ( 1 - ( E / N ) ) < ( z ` t ) ) )
29 28 ralbidv 
 |-  ( y = z -> ( A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) <-> A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( z ` t ) ) )
30 27 29 anbi12d 
 |-  ( y = z -> ( ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) <-> ( A. t e. ( D ` j ) ( z ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( z ` t ) ) ) )
31 21 22 23 24 30 cbvrabw 
 |-  { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } = { z e. Y | ( A. t e. ( D ` j ) ( z ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( z ` t ) ) }
32 ovexd 
 |-  ( ph -> ( J Cn K ) e. _V )
33 11 5 sseqtrdi 
 |-  ( ph -> A C_ ( J Cn K ) )
34 32 33 ssexd 
 |-  ( ph -> A e. _V )
35 8 34 rabexd 
 |-  ( ph -> Y e. _V )
36 31 35 rabexd 
 |-  ( ph -> { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } e. _V )
37 36 ralrimivw 
 |-  ( ph -> A. j e. ( 0 ... N ) { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } e. _V )
38 9 fnmpt 
 |-  ( A. j e. ( 0 ... N ) { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } e. _V -> H Fn ( 0 ... N ) )
39 37 38 syl 
 |-  ( ph -> H Fn ( 0 ... N ) )
40 fzfi 
 |-  ( 0 ... N ) e. Fin
41 fnfi 
 |-  ( ( H Fn ( 0 ... N ) /\ ( 0 ... N ) e. Fin ) -> H e. Fin )
42 39 40 41 sylancl 
 |-  ( ph -> H e. Fin )
43 rnfi 
 |-  ( H e. Fin -> ran H e. Fin )
44 42 43 syl 
 |-  ( ph -> ran H e. Fin )
45 fnchoice 
 |-  ( ran H e. Fin -> E. h ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) )
46 44 45 syl 
 |-  ( ph -> E. h ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) )
47 simprl 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> h Fn ran H )
48 ovex 
 |-  ( 0 ... N ) e. _V
49 48 mptex 
 |-  ( j e. ( 0 ... N ) |-> { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } ) e. _V
50 9 49 eqeltri 
 |-  H e. _V
51 50 rnex 
 |-  ran H e. _V
52 fnex 
 |-  ( ( h Fn ran H /\ ran H e. _V ) -> h e. _V )
53 47 51 52 sylancl 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> h e. _V )
54 coexg 
 |-  ( ( h e. _V /\ H e. _V ) -> ( h o. H ) e. _V )
55 53 50 54 sylancl 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> ( h o. H ) e. _V )
56 dffn3 
 |-  ( h Fn ran H <-> h : ran H --> ran h )
57 47 56 sylib 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> h : ran H --> ran h )
58 nfv 
 |-  F/ w ph
59 nfv 
 |-  F/ w h Fn ran H
60 nfra1 
 |-  F/ w A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w )
61 59 60 nfan 
 |-  F/ w ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) )
62 58 61 nfan 
 |-  F/ w ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) )
63 simplrr 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ w e. ran H ) -> A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) )
64 simpr 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ w e. ran H ) -> w e. ran H )
65 fvelrnb 
 |-  ( H Fn ( 0 ... N ) -> ( w e. ran H <-> E. a e. ( 0 ... N ) ( H ` a ) = w ) )
66 nfv 
 |-  F/ a ( H ` j ) = w
67 nfmpt1 
 |-  F/_ j ( j e. ( 0 ... N ) |-> { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } )
68 9 67 nfcxfr 
 |-  F/_ j H
69 nfcv 
 |-  F/_ j a
70 68 69 nffv 
 |-  F/_ j ( H ` a )
71 nfcv 
 |-  F/_ j w
72 70 71 nfeq 
 |-  F/ j ( H ` a ) = w
73 fveq2 
 |-  ( j = a -> ( H ` j ) = ( H ` a ) )
74 73 eqeq1d 
 |-  ( j = a -> ( ( H ` j ) = w <-> ( H ` a ) = w ) )
75 66 72 74 cbvrexw 
 |-  ( E. j e. ( 0 ... N ) ( H ` j ) = w <-> E. a e. ( 0 ... N ) ( H ` a ) = w )
76 65 75 bitr4di 
 |-  ( H Fn ( 0 ... N ) -> ( w e. ran H <-> E. j e. ( 0 ... N ) ( H ` j ) = w ) )
77 39 76 syl 
 |-  ( ph -> ( w e. ran H <-> E. j e. ( 0 ... N ) ( H ` j ) = w ) )
78 77 biimpa 
 |-  ( ( ph /\ w e. ran H ) -> E. j e. ( 0 ... N ) ( H ` j ) = w )
79 simp3 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ ( H ` j ) = w ) -> ( H ` j ) = w )
80 simpr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> j e. ( 0 ... N ) )
81 36 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } e. _V )
82 9 fvmpt2 
 |-  ( ( j e. ( 0 ... N ) /\ { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } e. _V ) -> ( H ` j ) = { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } )
83 80 81 82 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( H ` j ) = { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } )
84 nfcv 
 |-  F/_ t ( 0 ... N )
85 nfrab1 
 |-  F/_ t { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) }
86 84 85 nfmpt 
 |-  F/_ t ( j e. ( 0 ... N ) |-> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
87 6 86 nfcxfr 
 |-  F/_ t D
88 nfcv 
 |-  F/_ t j
89 87 88 nffv 
 |-  F/_ t ( D ` j )
90 nfcv 
 |-  F/_ t T
91 nfrab1 
 |-  F/_ t { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) }
92 84 91 nfmpt 
 |-  F/_ t ( j e. ( 0 ... N ) |-> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
93 7 92 nfcxfr 
 |-  F/_ t B
94 93 88 nffv 
 |-  F/_ t ( B ` j )
95 90 94 nfdif 
 |-  F/_ t ( T \ ( B ` j ) )
96 nfv 
 |-  F/ t j e. ( 0 ... N )
97 2 96 nfan 
 |-  F/ t ( ph /\ j e. ( 0 ... N ) )
98 10 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> J e. Comp )
99 11 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> A C_ C )
100 12 3adant1r 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) + ( g ` t ) ) ) e. A )
101 13 3adant1r 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )
102 14 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ y e. RR ) -> ( t e. T |-> y ) e. A )
103 15 adantlr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( r e. T /\ t e. T /\ r =/= t ) ) -> E. q e. A ( q ` r ) =/= ( q ` t ) )
104 10 uniexd 
 |-  ( ph -> U. J e. _V )
105 4 104 eqeltrid 
 |-  ( ph -> T e. _V )
106 105 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> T e. _V )
107 rabexg 
 |-  ( T e. _V -> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
108 106 107 syl 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V )
109 7 fvmpt2 
 |-  ( ( j e. ( 0 ... N ) /\ { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. _V ) -> ( B ` j ) = { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
110 80 108 109 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( B ` j ) = { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
111 eqid 
 |-  { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } = { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) }
112 elfzelz 
 |-  ( j e. ( 0 ... N ) -> j e. ZZ )
113 112 zred 
 |-  ( j e. ( 0 ... N ) -> j e. RR )
114 3re 
 |-  3 e. RR
115 3ne0 
 |-  3 =/= 0
116 114 115 rereccli 
 |-  ( 1 / 3 ) e. RR
117 readdcl 
 |-  ( ( j e. RR /\ ( 1 / 3 ) e. RR ) -> ( j + ( 1 / 3 ) ) e. RR )
118 113 116 117 sylancl 
 |-  ( j e. ( 0 ... N ) -> ( j + ( 1 / 3 ) ) e. RR )
119 118 adantl 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( j + ( 1 / 3 ) ) e. RR )
120 17 rpred 
 |-  ( ph -> E e. RR )
121 120 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> E e. RR )
122 119 121 remulcld 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( j + ( 1 / 3 ) ) x. E ) e. RR )
123 16 5 eleqtrdi 
 |-  ( ph -> F e. ( J Cn K ) )
124 123 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> F e. ( J Cn K ) )
125 1 3 4 111 122 124 rfcnpre3 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } e. ( Clsd ` J ) )
126 110 125 eqeltrd 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( B ` j ) e. ( Clsd ` J ) )
127 rabexg 
 |-  ( T e. _V -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } e. _V )
128 106 127 syl 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } e. _V )
129 6 fvmpt2 
 |-  ( ( j e. ( 0 ... N ) /\ { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } e. _V ) -> ( D ` j ) = { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
130 80 128 129 syl2anc 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) = { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
131 eqid 
 |-  { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } = { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) }
132 resubcl 
 |-  ( ( j e. RR /\ ( 1 / 3 ) e. RR ) -> ( j - ( 1 / 3 ) ) e. RR )
133 113 116 132 sylancl 
 |-  ( j e. ( 0 ... N ) -> ( j - ( 1 / 3 ) ) e. RR )
134 133 adantl 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( j - ( 1 / 3 ) ) e. RR )
135 134 121 remulcld 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( j - ( 1 / 3 ) ) x. E ) e. RR )
136 1 3 4 131 135 124 rfcnpre4 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } e. ( Clsd ` J ) )
137 130 136 eqeltrd 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( D ` j ) e. ( Clsd ` J ) )
138 135 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> ( ( j - ( 1 / 3 ) ) x. E ) e. RR )
139 122 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> ( ( j + ( 1 / 3 ) ) x. E ) e. RR )
140 3 4 5 16 fcnre 
 |-  ( ph -> F : T --> RR )
141 140 ad2antrr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> F : T --> RR )
142 ssrab2 
 |-  { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } C_ T
143 110 142 eqsstrdi 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( B ` j ) C_ T )
144 143 sselda 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> t e. T )
145 141 144 ffvelrnd 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> ( F ` t ) e. RR )
146 116 132 mpan2 
 |-  ( j e. RR -> ( j - ( 1 / 3 ) ) e. RR )
147 id 
 |-  ( j e. RR -> j e. RR )
148 116 117 mpan2 
 |-  ( j e. RR -> ( j + ( 1 / 3 ) ) e. RR )
149 3pos 
 |-  0 < 3
150 114 149 recgt0ii 
 |-  0 < ( 1 / 3 )
151 116 150 elrpii 
 |-  ( 1 / 3 ) e. RR+
152 ltsubrp 
 |-  ( ( j e. RR /\ ( 1 / 3 ) e. RR+ ) -> ( j - ( 1 / 3 ) ) < j )
153 151 152 mpan2 
 |-  ( j e. RR -> ( j - ( 1 / 3 ) ) < j )
154 ltaddrp 
 |-  ( ( j e. RR /\ ( 1 / 3 ) e. RR+ ) -> j < ( j + ( 1 / 3 ) ) )
155 151 154 mpan2 
 |-  ( j e. RR -> j < ( j + ( 1 / 3 ) ) )
156 146 147 148 153 155 lttrd 
 |-  ( j e. RR -> ( j - ( 1 / 3 ) ) < ( j + ( 1 / 3 ) ) )
157 113 156 syl 
 |-  ( j e. ( 0 ... N ) -> ( j - ( 1 / 3 ) ) < ( j + ( 1 / 3 ) ) )
158 157 adantl 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( j - ( 1 / 3 ) ) < ( j + ( 1 / 3 ) ) )
159 17 rpregt0d 
 |-  ( ph -> ( E e. RR /\ 0 < E ) )
160 159 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( E e. RR /\ 0 < E ) )
161 ltmul1 
 |-  ( ( ( j - ( 1 / 3 ) ) e. RR /\ ( j + ( 1 / 3 ) ) e. RR /\ ( E e. RR /\ 0 < E ) ) -> ( ( j - ( 1 / 3 ) ) < ( j + ( 1 / 3 ) ) <-> ( ( j - ( 1 / 3 ) ) x. E ) < ( ( j + ( 1 / 3 ) ) x. E ) ) )
162 134 119 160 161 syl3anc 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( j - ( 1 / 3 ) ) < ( j + ( 1 / 3 ) ) <-> ( ( j - ( 1 / 3 ) ) x. E ) < ( ( j + ( 1 / 3 ) ) x. E ) ) )
163 158 162 mpbid 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( j - ( 1 / 3 ) ) x. E ) < ( ( j + ( 1 / 3 ) ) x. E ) )
164 163 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> ( ( j - ( 1 / 3 ) ) x. E ) < ( ( j + ( 1 / 3 ) ) x. E ) )
165 110 eleq2d 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( t e. ( B ` j ) <-> t e. { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } ) )
166 165 biimpa 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> t e. { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } )
167 rabid 
 |-  ( t e. { t e. T | ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) } <-> ( t e. T /\ ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) ) )
168 166 167 sylib 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> ( t e. T /\ ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) ) )
169 168 simprd 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> ( ( j + ( 1 / 3 ) ) x. E ) <_ ( F ` t ) )
170 138 139 145 164 169 ltletrd 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> ( ( j - ( 1 / 3 ) ) x. E ) < ( F ` t ) )
171 138 145 ltnled 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> ( ( ( j - ( 1 / 3 ) ) x. E ) < ( F ` t ) <-> -. ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) )
172 170 171 mpbid 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> -. ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) )
173 172 intnand 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> -. ( t e. T /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) )
174 rabid 
 |-  ( t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } <-> ( t e. T /\ ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) ) )
175 173 174 sylnibr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> -. t e. { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
176 130 adantr 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> ( D ` j ) = { t e. T | ( F ` t ) <_ ( ( j - ( 1 / 3 ) ) x. E ) } )
177 175 176 neleqtrrd 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ t e. ( B ` j ) ) -> -. t e. ( D ` j ) )
178 177 ex 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( t e. ( B ` j ) -> -. t e. ( D ` j ) ) )
179 97 178 ralrimi 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> A. t e. ( B ` j ) -. t e. ( D ` j ) )
180 disj 
 |-  ( ( ( B ` j ) i^i ( D ` j ) ) = (/) <-> A. a e. ( B ` j ) -. a e. ( D ` j ) )
181 nfcv 
 |-  F/_ a ( B ` j )
182 89 nfcri 
 |-  F/ t a e. ( D ` j )
183 182 nfn 
 |-  F/ t -. a e. ( D ` j )
184 nfv 
 |-  F/ a -. t e. ( D ` j )
185 eleq1 
 |-  ( a = t -> ( a e. ( D ` j ) <-> t e. ( D ` j ) ) )
186 185 notbid 
 |-  ( a = t -> ( -. a e. ( D ` j ) <-> -. t e. ( D ` j ) ) )
187 181 94 183 184 186 cbvralfw 
 |-  ( A. a e. ( B ` j ) -. a e. ( D ` j ) <-> A. t e. ( B ` j ) -. t e. ( D ` j ) )
188 180 187 bitri 
 |-  ( ( ( B ` j ) i^i ( D ` j ) ) = (/) <-> A. t e. ( B ` j ) -. t e. ( D ` j ) )
189 179 188 sylibr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( B ` j ) i^i ( D ` j ) ) = (/) )
190 eqid 
 |-  ( T \ ( B ` j ) ) = ( T \ ( B ` j ) )
191 19 nnrpd 
 |-  ( ph -> N e. RR+ )
192 17 191 rpdivcld 
 |-  ( ph -> ( E / N ) e. RR+ )
193 192 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( E / N ) e. RR+ )
194 120 19 nndivred 
 |-  ( ph -> ( E / N ) e. RR )
195 116 a1i 
 |-  ( ph -> ( 1 / 3 ) e. RR )
196 19 nnge1d 
 |-  ( ph -> 1 <_ N )
197 1re 
 |-  1 e. RR
198 0lt1 
 |-  0 < 1
199 197 198 pm3.2i 
 |-  ( 1 e. RR /\ 0 < 1 )
200 199 a1i 
 |-  ( ph -> ( 1 e. RR /\ 0 < 1 ) )
201 19 nnred 
 |-  ( ph -> N e. RR )
202 19 nngt0d 
 |-  ( ph -> 0 < N )
203 lediv2 
 |-  ( ( ( 1 e. RR /\ 0 < 1 ) /\ ( N e. RR /\ 0 < N ) /\ ( E e. RR /\ 0 < E ) ) -> ( 1 <_ N <-> ( E / N ) <_ ( E / 1 ) ) )
204 200 201 202 159 203 syl121anc 
 |-  ( ph -> ( 1 <_ N <-> ( E / N ) <_ ( E / 1 ) ) )
205 196 204 mpbid 
 |-  ( ph -> ( E / N ) <_ ( E / 1 ) )
206 17 rpcnd 
 |-  ( ph -> E e. CC )
207 206 div1d 
 |-  ( ph -> ( E / 1 ) = E )
208 205 207 breqtrd 
 |-  ( ph -> ( E / N ) <_ E )
209 194 120 195 208 18 lelttrd 
 |-  ( ph -> ( E / N ) < ( 1 / 3 ) )
210 209 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( E / N ) < ( 1 / 3 ) )
211 89 95 97 3 4 5 98 99 100 101 102 103 126 137 189 190 193 210 stoweidlem58 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) )
212 df-rex 
 |-  ( E. x e. A ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) <-> E. x ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) ) )
213 211 212 sylib 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> E. x ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) ) )
214 simprl 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) ) ) -> x e. A )
215 simprr1 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) ) ) -> A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) )
216 fveq1 
 |-  ( y = x -> ( y ` t ) = ( x ` t ) )
217 216 breq2d 
 |-  ( y = x -> ( 0 <_ ( y ` t ) <-> 0 <_ ( x ` t ) ) )
218 216 breq1d 
 |-  ( y = x -> ( ( y ` t ) <_ 1 <-> ( x ` t ) <_ 1 ) )
219 217 218 anbi12d 
 |-  ( y = x -> ( ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) <-> ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) ) )
220 219 ralbidv 
 |-  ( y = x -> ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) ) )
221 220 8 elrab2 
 |-  ( x e. Y <-> ( x e. A /\ A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) ) )
222 214 215 221 sylanbrc 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) ) ) -> x e. Y )
223 simprr2 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) ) ) -> A. t e. ( D ` j ) ( x ` t ) < ( E / N ) )
224 simprr3 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) ) ) -> A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) )
225 223 224 jca 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) ) ) -> ( A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) )
226 nfcv 
 |-  F/_ y x
227 nfv 
 |-  F/ y ( A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) )
228 216 breq1d 
 |-  ( y = x -> ( ( y ` t ) < ( E / N ) <-> ( x ` t ) < ( E / N ) ) )
229 228 ralbidv 
 |-  ( y = x -> ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) <-> A. t e. ( D ` j ) ( x ` t ) < ( E / N ) ) )
230 216 breq2d 
 |-  ( y = x -> ( ( 1 - ( E / N ) ) < ( y ` t ) <-> ( 1 - ( E / N ) ) < ( x ` t ) ) )
231 230 ralbidv 
 |-  ( y = x -> ( A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) <-> A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) )
232 229 231 anbi12d 
 |-  ( y = x -> ( ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) <-> ( A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) ) )
233 226 21 227 232 elrabf 
 |-  ( x e. { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } <-> ( x e. Y /\ ( A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) ) )
234 222 225 233 sylanbrc 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) ) ) -> x e. { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } )
235 234 ex 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) ) -> x e. { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } ) )
236 235 eximdv 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( E. x ( x e. A /\ ( A. t e. T ( 0 <_ ( x ` t ) /\ ( x ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( x ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( x ` t ) ) ) -> E. x x e. { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } ) )
237 213 236 mpd 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> E. x x e. { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } )
238 ne0i 
 |-  ( x e. { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } -> { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } =/= (/) )
239 238 exlimiv 
 |-  ( E. x x e. { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } -> { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } =/= (/) )
240 237 239 syl 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } =/= (/) )
241 83 240 eqnetrd 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( H ` j ) =/= (/) )
242 241 3adant3 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ ( H ` j ) = w ) -> ( H ` j ) =/= (/) )
243 79 242 eqnetrrd 
 |-  ( ( ph /\ j e. ( 0 ... N ) /\ ( H ` j ) = w ) -> w =/= (/) )
244 243 3exp 
 |-  ( ph -> ( j e. ( 0 ... N ) -> ( ( H ` j ) = w -> w =/= (/) ) ) )
245 244 rexlimdv 
 |-  ( ph -> ( E. j e. ( 0 ... N ) ( H ` j ) = w -> w =/= (/) ) )
246 245 adantr 
 |-  ( ( ph /\ w e. ran H ) -> ( E. j e. ( 0 ... N ) ( H ` j ) = w -> w =/= (/) ) )
247 78 246 mpd 
 |-  ( ( ph /\ w e. ran H ) -> w =/= (/) )
248 247 adantlr 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ w e. ran H ) -> w =/= (/) )
249 rsp 
 |-  ( A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) -> ( w e. ran H -> ( w =/= (/) -> ( h ` w ) e. w ) ) )
250 63 64 248 249 syl3c 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ w e. ran H ) -> ( h ` w ) e. w )
251 250 ex 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> ( w e. ran H -> ( h ` w ) e. w ) )
252 62 251 ralrimi 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> A. w e. ran H ( h ` w ) e. w )
253 chfnrn 
 |-  ( ( h Fn ran H /\ A. w e. ran H ( h ` w ) e. w ) -> ran h C_ U. ran H )
254 47 252 253 syl2anc 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> ran h C_ U. ran H )
255 nfv 
 |-  F/ y ph
256 nfcv 
 |-  F/_ y h
257 nfcv 
 |-  F/_ y ( 0 ... N )
258 nfrab1 
 |-  F/_ y { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) }
259 257 258 nfmpt 
 |-  F/_ y ( j e. ( 0 ... N ) |-> { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } )
260 9 259 nfcxfr 
 |-  F/_ y H
261 260 nfrn 
 |-  F/_ y ran H
262 256 261 nffn 
 |-  F/ y h Fn ran H
263 nfv 
 |-  F/ y ( w =/= (/) -> ( h ` w ) e. w )
264 261 263 nfralw 
 |-  F/ y A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w )
265 262 264 nfan 
 |-  F/ y ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) )
266 255 265 nfan 
 |-  F/ y ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) )
267 261 nfuni 
 |-  F/_ y U. ran H
268 fnunirn 
 |-  ( H Fn ( 0 ... N ) -> ( y e. U. ran H <-> E. z e. ( 0 ... N ) y e. ( H ` z ) ) )
269 nfcv 
 |-  F/_ j z
270 68 269 nffv 
 |-  F/_ j ( H ` z )
271 270 nfcri 
 |-  F/ j y e. ( H ` z )
272 nfv 
 |-  F/ z y e. ( H ` j )
273 fveq2 
 |-  ( z = j -> ( H ` z ) = ( H ` j ) )
274 273 eleq2d 
 |-  ( z = j -> ( y e. ( H ` z ) <-> y e. ( H ` j ) ) )
275 271 272 274 cbvrexw 
 |-  ( E. z e. ( 0 ... N ) y e. ( H ` z ) <-> E. j e. ( 0 ... N ) y e. ( H ` j ) )
276 268 275 bitrdi 
 |-  ( H Fn ( 0 ... N ) -> ( y e. U. ran H <-> E. j e. ( 0 ... N ) y e. ( H ` j ) ) )
277 39 276 syl 
 |-  ( ph -> ( y e. U. ran H <-> E. j e. ( 0 ... N ) y e. ( H ` j ) ) )
278 277 biimpa 
 |-  ( ( ph /\ y e. U. ran H ) -> E. j e. ( 0 ... N ) y e. ( H ` j ) )
279 nfv 
 |-  F/ j ph
280 68 nfrn 
 |-  F/_ j ran H
281 280 nfuni 
 |-  F/_ j U. ran H
282 281 nfcri 
 |-  F/ j y e. U. ran H
283 279 282 nfan 
 |-  F/ j ( ph /\ y e. U. ran H )
284 nfv 
 |-  F/ j y e. Y
285 simp1l 
 |-  ( ( ( ph /\ y e. U. ran H ) /\ j e. ( 0 ... N ) /\ y e. ( H ` j ) ) -> ph )
286 simp2 
 |-  ( ( ( ph /\ y e. U. ran H ) /\ j e. ( 0 ... N ) /\ y e. ( H ` j ) ) -> j e. ( 0 ... N ) )
287 simp3 
 |-  ( ( ( ph /\ y e. U. ran H ) /\ j e. ( 0 ... N ) /\ y e. ( H ` j ) ) -> y e. ( H ` j ) )
288 83 eleq2d 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> ( y e. ( H ` j ) <-> y e. { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } ) )
289 288 biimpa 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ y e. ( H ` j ) ) -> y e. { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } )
290 rabid 
 |-  ( y e. { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } <-> ( y e. Y /\ ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) ) )
291 289 290 sylib 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ y e. ( H ` j ) ) -> ( y e. Y /\ ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) ) )
292 291 simpld 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ y e. ( H ` j ) ) -> y e. Y )
293 285 286 287 292 syl21anc 
 |-  ( ( ( ph /\ y e. U. ran H ) /\ j e. ( 0 ... N ) /\ y e. ( H ` j ) ) -> y e. Y )
294 293 3exp 
 |-  ( ( ph /\ y e. U. ran H ) -> ( j e. ( 0 ... N ) -> ( y e. ( H ` j ) -> y e. Y ) ) )
295 283 284 294 rexlimd 
 |-  ( ( ph /\ y e. U. ran H ) -> ( E. j e. ( 0 ... N ) y e. ( H ` j ) -> y e. Y ) )
296 278 295 mpd 
 |-  ( ( ph /\ y e. U. ran H ) -> y e. Y )
297 296 adantlr 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ y e. U. ran H ) -> y e. Y )
298 297 ex 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> ( y e. U. ran H -> y e. Y ) )
299 266 267 21 298 ssrd 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> U. ran H C_ Y )
300 ssrab2 
 |-  { y e. A | A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) } C_ A
301 8 300 eqsstri 
 |-  Y C_ A
302 299 301 sstrdi 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> U. ran H C_ A )
303 254 302 sstrd 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> ran h C_ A )
304 57 303 fssd 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> h : ran H --> A )
305 dffn3 
 |-  ( H Fn ( 0 ... N ) <-> H : ( 0 ... N ) --> ran H )
306 39 305 sylib 
 |-  ( ph -> H : ( 0 ... N ) --> ran H )
307 306 adantr 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> H : ( 0 ... N ) --> ran H )
308 fco 
 |-  ( ( h : ran H --> A /\ H : ( 0 ... N ) --> ran H ) -> ( h o. H ) : ( 0 ... N ) --> A )
309 304 307 308 syl2anc 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> ( h o. H ) : ( 0 ... N ) --> A )
310 nfcv 
 |-  F/_ j h
311 310 280 nffn 
 |-  F/ j h Fn ran H
312 nfv 
 |-  F/ j ( w =/= (/) -> ( h ` w ) e. w )
313 280 312 nfralw 
 |-  F/ j A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w )
314 311 313 nfan 
 |-  F/ j ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) )
315 279 314 nfan 
 |-  F/ j ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) )
316 simpll 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> ph )
317 simpr 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> j e. ( 0 ... N ) )
318 39 ad2antrr 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> H Fn ( 0 ... N ) )
319 fvco2 
 |-  ( ( H Fn ( 0 ... N ) /\ j e. ( 0 ... N ) ) -> ( ( h o. H ) ` j ) = ( h ` ( H ` j ) ) )
320 318 319 sylancom 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> ( ( h o. H ) ` j ) = ( h ` ( H ` j ) ) )
321 simplrr 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) )
322 fnfun 
 |-  ( H Fn ( 0 ... N ) -> Fun H )
323 39 322 syl 
 |-  ( ph -> Fun H )
324 323 ad2antrr 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> Fun H )
325 39 fndmd 
 |-  ( ph -> dom H = ( 0 ... N ) )
326 325 adantr 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> dom H = ( 0 ... N ) )
327 80 326 eleqtrrd 
 |-  ( ( ph /\ j e. ( 0 ... N ) ) -> j e. dom H )
328 327 adantlr 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> j e. dom H )
329 fvelrn 
 |-  ( ( Fun H /\ j e. dom H ) -> ( H ` j ) e. ran H )
330 324 328 329 syl2anc 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> ( H ` j ) e. ran H )
331 321 330 jca 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> ( A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) /\ ( H ` j ) e. ran H ) )
332 241 adantlr 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> ( H ` j ) =/= (/) )
333 neeq1 
 |-  ( w = ( H ` j ) -> ( w =/= (/) <-> ( H ` j ) =/= (/) ) )
334 fveq2 
 |-  ( w = ( H ` j ) -> ( h ` w ) = ( h ` ( H ` j ) ) )
335 id 
 |-  ( w = ( H ` j ) -> w = ( H ` j ) )
336 334 335 eleq12d 
 |-  ( w = ( H ` j ) -> ( ( h ` w ) e. w <-> ( h ` ( H ` j ) ) e. ( H ` j ) ) )
337 333 336 imbi12d 
 |-  ( w = ( H ` j ) -> ( ( w =/= (/) -> ( h ` w ) e. w ) <-> ( ( H ` j ) =/= (/) -> ( h ` ( H ` j ) ) e. ( H ` j ) ) ) )
338 337 rspccva 
 |-  ( ( A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) /\ ( H ` j ) e. ran H ) -> ( ( H ` j ) =/= (/) -> ( h ` ( H ` j ) ) e. ( H ` j ) ) )
339 331 332 338 sylc 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> ( h ` ( H ` j ) ) e. ( H ` j ) )
340 320 339 eqeltrd 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> ( ( h o. H ) ` j ) e. ( H ` j ) )
341 256 260 nfco 
 |-  F/_ y ( h o. H )
342 nfcv 
 |-  F/_ y j
343 341 342 nffv 
 |-  F/_ y ( ( h o. H ) ` j )
344 nfv 
 |-  F/ y ( ph /\ j e. ( 0 ... N ) )
345 260 342 nffv 
 |-  F/_ y ( H ` j )
346 343 345 nfel 
 |-  F/ y ( ( h o. H ) ` j ) e. ( H ` j )
347 344 346 nfan 
 |-  F/ y ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) )
348 343 21 nfel 
 |-  F/ y ( ( h o. H ) ` j ) e. Y
349 347 348 nfim 
 |-  F/ y ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) ) -> ( ( h o. H ) ` j ) e. Y )
350 eleq1 
 |-  ( y = ( ( h o. H ) ` j ) -> ( y e. ( H ` j ) <-> ( ( h o. H ) ` j ) e. ( H ` j ) ) )
351 350 anbi2d 
 |-  ( y = ( ( h o. H ) ` j ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) /\ y e. ( H ` j ) ) <-> ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) ) ) )
352 eleq1 
 |-  ( y = ( ( h o. H ) ` j ) -> ( y e. Y <-> ( ( h o. H ) ` j ) e. Y ) )
353 351 352 imbi12d 
 |-  ( y = ( ( h o. H ) ` j ) -> ( ( ( ( ph /\ j e. ( 0 ... N ) ) /\ y e. ( H ` j ) ) -> y e. Y ) <-> ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) ) -> ( ( h o. H ) ` j ) e. Y ) ) )
354 343 349 353 292 vtoclgf 
 |-  ( ( ( h o. H ) ` j ) e. ( H ` j ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) ) -> ( ( h o. H ) ` j ) e. Y ) )
355 354 anabsi7 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) ) -> ( ( h o. H ) ` j ) e. Y )
356 316 317 340 355 syl21anc 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> ( ( h o. H ) ` j ) e. Y )
357 8 eleq2i 
 |-  ( ( ( h o. H ) ` j ) e. Y <-> ( ( h o. H ) ` j ) e. { y e. A | A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) } )
358 nfcv 
 |-  F/_ y A
359 nfcv 
 |-  F/_ y T
360 nfcv 
 |-  F/_ y 0
361 nfcv 
 |-  F/_ y <_
362 nfcv 
 |-  F/_ y t
363 343 362 nffv 
 |-  F/_ y ( ( ( h o. H ) ` j ) ` t )
364 360 361 363 nfbr 
 |-  F/ y 0 <_ ( ( ( h o. H ) ` j ) ` t )
365 nfcv 
 |-  F/_ y 1
366 363 361 365 nfbr 
 |-  F/ y ( ( ( h o. H ) ` j ) ` t ) <_ 1
367 364 366 nfan 
 |-  F/ y ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 )
368 359 367 nfralw 
 |-  F/ y A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 )
369 nfcv 
 |-  F/_ t y
370 nfcv 
 |-  F/_ t h
371 nfra1 
 |-  F/ t A. t e. ( D ` j ) ( y ` t ) < ( E / N )
372 nfra1 
 |-  F/ t A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t )
373 371 372 nfan 
 |-  F/ t ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) )
374 nfra1 
 |-  F/ t A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 )
375 nfcv 
 |-  F/_ t A
376 374 375 nfrabw 
 |-  F/_ t { y e. A | A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) }
377 8 376 nfcxfr 
 |-  F/_ t Y
378 373 377 nfrabw 
 |-  F/_ t { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) }
379 84 378 nfmpt 
 |-  F/_ t ( j e. ( 0 ... N ) |-> { y e. Y | ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) } )
380 9 379 nfcxfr 
 |-  F/_ t H
381 370 380 nfco 
 |-  F/_ t ( h o. H )
382 381 88 nffv 
 |-  F/_ t ( ( h o. H ) ` j )
383 369 382 nfeq 
 |-  F/ t y = ( ( h o. H ) ` j )
384 fveq1 
 |-  ( y = ( ( h o. H ) ` j ) -> ( y ` t ) = ( ( ( h o. H ) ` j ) ` t ) )
385 384 breq2d 
 |-  ( y = ( ( h o. H ) ` j ) -> ( 0 <_ ( y ` t ) <-> 0 <_ ( ( ( h o. H ) ` j ) ` t ) ) )
386 384 breq1d 
 |-  ( y = ( ( h o. H ) ` j ) -> ( ( y ` t ) <_ 1 <-> ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) )
387 385 386 anbi12d 
 |-  ( y = ( ( h o. H ) ` j ) -> ( ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) <-> ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) ) )
388 383 387 ralbid 
 |-  ( y = ( ( h o. H ) ` j ) -> ( A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) ) )
389 343 358 368 388 elrabf 
 |-  ( ( ( h o. H ) ` j ) e. { y e. A | A. t e. T ( 0 <_ ( y ` t ) /\ ( y ` t ) <_ 1 ) } <-> ( ( ( h o. H ) ` j ) e. A /\ A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) ) )
390 357 389 bitri 
 |-  ( ( ( h o. H ) ` j ) e. Y <-> ( ( ( h o. H ) ` j ) e. A /\ A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) ) )
391 356 390 sylib 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> ( ( ( h o. H ) ` j ) e. A /\ A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) ) )
392 391 simprd 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) )
393 nfcv 
 |-  F/_ y ( D ` j )
394 nfcv 
 |-  F/_ y <
395 nfcv 
 |-  F/_ y ( E / N )
396 363 394 395 nfbr 
 |-  F/ y ( ( ( h o. H ) ` j ) ` t ) < ( E / N )
397 393 396 nfralw 
 |-  F/ y A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N )
398 347 397 nfim 
 |-  F/ y ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) ) -> A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) )
399 384 breq1d 
 |-  ( y = ( ( h o. H ) ` j ) -> ( ( y ` t ) < ( E / N ) <-> ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) ) )
400 383 399 ralbid 
 |-  ( y = ( ( h o. H ) ` j ) -> ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) <-> A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) ) )
401 351 400 imbi12d 
 |-  ( y = ( ( h o. H ) ` j ) -> ( ( ( ( ph /\ j e. ( 0 ... N ) ) /\ y e. ( H ` j ) ) -> A. t e. ( D ` j ) ( y ` t ) < ( E / N ) ) <-> ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) ) -> A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) ) ) )
402 291 simprd 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ y e. ( H ` j ) ) -> ( A. t e. ( D ` j ) ( y ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) )
403 402 simpld 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ y e. ( H ` j ) ) -> A. t e. ( D ` j ) ( y ` t ) < ( E / N ) )
404 343 398 401 403 vtoclgf 
 |-  ( ( ( h o. H ) ` j ) e. ( H ` j ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) ) -> A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) ) )
405 404 anabsi7 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) ) -> A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) )
406 316 317 340 405 syl21anc 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) )
407 nfcv 
 |-  F/_ y ( B ` j )
408 nfcv 
 |-  F/_ y ( 1 - ( E / N ) )
409 408 394 363 nfbr 
 |-  F/ y ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t )
410 407 409 nfralw 
 |-  F/ y A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t )
411 347 410 nfim 
 |-  F/ y ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) ) -> A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) )
412 384 breq2d 
 |-  ( y = ( ( h o. H ) ` j ) -> ( ( 1 - ( E / N ) ) < ( y ` t ) <-> ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) )
413 383 412 ralbid 
 |-  ( y = ( ( h o. H ) ` j ) -> ( A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) <-> A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) )
414 351 413 imbi12d 
 |-  ( y = ( ( h o. H ) ` j ) -> ( ( ( ( ph /\ j e. ( 0 ... N ) ) /\ y e. ( H ` j ) ) -> A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) ) <-> ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) ) -> A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) ) )
415 402 simprd 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ y e. ( H ` j ) ) -> A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( y ` t ) )
416 343 411 414 415 vtoclgf 
 |-  ( ( ( h o. H ) ` j ) e. ( H ` j ) -> ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) ) -> A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) )
417 416 anabsi7 
 |-  ( ( ( ph /\ j e. ( 0 ... N ) ) /\ ( ( h o. H ) ` j ) e. ( H ` j ) ) -> A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) )
418 316 317 340 417 syl21anc 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) )
419 392 406 418 3jca 
 |-  ( ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) /\ j e. ( 0 ... N ) ) -> ( A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) )
420 419 ex 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> ( j e. ( 0 ... N ) -> ( A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) ) )
421 315 420 ralrimi 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> A. j e. ( 0 ... N ) ( A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) )
422 309 421 jca 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> ( ( h o. H ) : ( 0 ... N ) --> A /\ A. j e. ( 0 ... N ) ( A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) ) )
423 feq1 
 |-  ( x = ( h o. H ) -> ( x : ( 0 ... N ) --> A <-> ( h o. H ) : ( 0 ... N ) --> A ) )
424 nfcv 
 |-  F/_ j x
425 310 68 nfco 
 |-  F/_ j ( h o. H )
426 424 425 nfeq 
 |-  F/ j x = ( h o. H )
427 nfcv 
 |-  F/_ t x
428 427 381 nfeq 
 |-  F/ t x = ( h o. H )
429 fveq1 
 |-  ( x = ( h o. H ) -> ( x ` j ) = ( ( h o. H ) ` j ) )
430 429 fveq1d 
 |-  ( x = ( h o. H ) -> ( ( x ` j ) ` t ) = ( ( ( h o. H ) ` j ) ` t ) )
431 430 breq2d 
 |-  ( x = ( h o. H ) -> ( 0 <_ ( ( x ` j ) ` t ) <-> 0 <_ ( ( ( h o. H ) ` j ) ` t ) ) )
432 430 breq1d 
 |-  ( x = ( h o. H ) -> ( ( ( x ` j ) ` t ) <_ 1 <-> ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) )
433 431 432 anbi12d 
 |-  ( x = ( h o. H ) -> ( ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) <-> ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) ) )
434 428 433 ralbid 
 |-  ( x = ( h o. H ) -> ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) ) )
435 430 breq1d 
 |-  ( x = ( h o. H ) -> ( ( ( x ` j ) ` t ) < ( E / N ) <-> ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) ) )
436 428 435 ralbid 
 |-  ( x = ( h o. H ) -> ( A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / N ) <-> A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) ) )
437 430 breq2d 
 |-  ( x = ( h o. H ) -> ( ( 1 - ( E / N ) ) < ( ( x ` j ) ` t ) <-> ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) )
438 428 437 ralbid 
 |-  ( x = ( h o. H ) -> ( A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( x ` j ) ` t ) <-> A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) )
439 434 436 438 3anbi123d 
 |-  ( x = ( h o. H ) -> ( ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( x ` j ) ` t ) ) <-> ( A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) ) )
440 426 439 ralbid 
 |-  ( x = ( h o. H ) -> ( A. j e. ( 0 ... N ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( x ` j ) ` t ) ) <-> A. j e. ( 0 ... N ) ( A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) ) )
441 423 440 anbi12d 
 |-  ( x = ( h o. H ) -> ( ( x : ( 0 ... N ) --> A /\ A. j e. ( 0 ... N ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( x ` j ) ` t ) ) ) <-> ( ( h o. H ) : ( 0 ... N ) --> A /\ A. j e. ( 0 ... N ) ( A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) ) ) )
442 441 spcegv 
 |-  ( ( h o. H ) e. _V -> ( ( ( h o. H ) : ( 0 ... N ) --> A /\ A. j e. ( 0 ... N ) ( A. t e. T ( 0 <_ ( ( ( h o. H ) ` j ) ` t ) /\ ( ( ( h o. H ) ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( ( h o. H ) ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( ( h o. H ) ` j ) ` t ) ) ) -> E. x ( x : ( 0 ... N ) --> A /\ A. j e. ( 0 ... N ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( x ` j ) ` t ) ) ) ) )
443 55 422 442 sylc 
 |-  ( ( ph /\ ( h Fn ran H /\ A. w e. ran H ( w =/= (/) -> ( h ` w ) e. w ) ) ) -> E. x ( x : ( 0 ... N ) --> A /\ A. j e. ( 0 ... N ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( x ` j ) ` t ) ) ) )
444 46 443 exlimddv 
 |-  ( ph -> E. x ( x : ( 0 ... N ) --> A /\ A. j e. ( 0 ... N ) ( A. t e. T ( 0 <_ ( ( x ` j ) ` t ) /\ ( ( x ` j ) ` t ) <_ 1 ) /\ A. t e. ( D ` j ) ( ( x ` j ) ` t ) < ( E / N ) /\ A. t e. ( B ` j ) ( 1 - ( E / N ) ) < ( ( x ` j ) ` t ) ) ) )