# Metamath Proof Explorer

## Theorem stoweidlem48

Description: This lemma is used to prove that x built as in Lemma 2 of BrosowskiDeutsh p. 91, is such that x < ε on A . Here X is used to represent x in the paper, E is used to represent ε in the paper, and D is used to represent A in the paper (because A is always used to represent the subalgebra). (Contributed by Glauco Siliprandi, 20-Apr-2017)

Ref Expression
Hypotheses stoweidlem48.1
`|- F/ i ph`
stoweidlem48.2
`|- F/ t ph`
stoweidlem48.3
`|- Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }`
stoweidlem48.4
`|- P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )`
stoweidlem48.5
`|- X = ( seq 1 ( P , U ) ` M )`
stoweidlem48.6
`|- F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )`
stoweidlem48.7
`|- Z = ( t e. T |-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )`
stoweidlem48.8
`|- ( ph -> M e. NN )`
stoweidlem48.9
`|- ( ph -> W : ( 1 ... M ) --> V )`
stoweidlem48.10
`|- ( ph -> U : ( 1 ... M ) --> Y )`
stoweidlem48.11
`|- ( ph -> D C_ U. ran W )`
stoweidlem48.12
`|- ( ph -> D C_ T )`
stoweidlem48.13
`|- ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. ( W ` i ) ( ( U ` i ) ` t ) < E )`
stoweidlem48.14
`|- ( ph -> T e. _V )`
stoweidlem48.15
`|- ( ( ph /\ f e. A ) -> f : T --> RR )`
stoweidlem48.16
`|- ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )`
stoweidlem48.17
`|- ( ph -> E e. RR+ )`
Assertion stoweidlem48
`|- ( ph -> A. t e. D ( X ` t ) < E )`

### Proof

Step Hyp Ref Expression
1 stoweidlem48.1
` |-  F/ i ph`
2 stoweidlem48.2
` |-  F/ t ph`
3 stoweidlem48.3
` |-  Y = { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }`
4 stoweidlem48.4
` |-  P = ( f e. Y , g e. Y |-> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) )`
5 stoweidlem48.5
` |-  X = ( seq 1 ( P , U ) ` M )`
6 stoweidlem48.6
` |-  F = ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )`
7 stoweidlem48.7
` |-  Z = ( t e. T |-> ( seq 1 ( x. , ( F ` t ) ) ` M ) )`
8 stoweidlem48.8
` |-  ( ph -> M e. NN )`
9 stoweidlem48.9
` |-  ( ph -> W : ( 1 ... M ) --> V )`
10 stoweidlem48.10
` |-  ( ph -> U : ( 1 ... M ) --> Y )`
11 stoweidlem48.11
` |-  ( ph -> D C_ U. ran W )`
12 stoweidlem48.12
` |-  ( ph -> D C_ T )`
13 stoweidlem48.13
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. ( W ` i ) ( ( U ` i ) ` t ) < E )`
14 stoweidlem48.14
` |-  ( ph -> T e. _V )`
15 stoweidlem48.15
` |-  ( ( ph /\ f e. A ) -> f : T --> RR )`
16 stoweidlem48.16
` |-  ( ( ph /\ f e. A /\ g e. A ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. A )`
17 stoweidlem48.17
` |-  ( ph -> E e. RR+ )`
18 12 sselda
` |-  ( ( ph /\ t e. D ) -> t e. T )`
19 nfra1
` |-  F/ t A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 )`
20 nfcv
` |-  F/_ t A`
21 19 20 nfrabw
` |-  F/_ t { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) }`
22 3 21 nfcxfr
` |-  F/_ t Y`
23 3 eleq2i
` |-  ( f e. Y <-> f e. { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) } )`
24 fveq1
` |-  ( h = f -> ( h ` t ) = ( f ` t ) )`
25 24 breq2d
` |-  ( h = f -> ( 0 <_ ( h ` t ) <-> 0 <_ ( f ` t ) ) )`
26 24 breq1d
` |-  ( h = f -> ( ( h ` t ) <_ 1 <-> ( f ` t ) <_ 1 ) )`
27 25 26 anbi12d
` |-  ( h = f -> ( ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> ( 0 <_ ( f ` t ) /\ ( f ` t ) <_ 1 ) ) )`
28 27 ralbidv
` |-  ( h = f -> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( f ` t ) /\ ( f ` t ) <_ 1 ) ) )`
29 28 elrab
` |-  ( f e. { h e. A | A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) } <-> ( f e. A /\ A. t e. T ( 0 <_ ( f ` t ) /\ ( f ` t ) <_ 1 ) ) )`
30 23 29 sylbb
` |-  ( f e. Y -> ( f e. A /\ A. t e. T ( 0 <_ ( f ` t ) /\ ( f ` t ) <_ 1 ) ) )`
31 30 simpld
` |-  ( f e. Y -> f e. A )`
32 31 15 sylan2
` |-  ( ( ph /\ f e. Y ) -> f : T --> RR )`
33 eqid
` |-  ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) = ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) )`
34 2 3 33 15 16 stoweidlem16
` |-  ( ( ph /\ f e. Y /\ g e. Y ) -> ( t e. T |-> ( ( f ` t ) x. ( g ` t ) ) ) e. Y )`
35 1 22 4 5 6 7 14 8 10 32 34 fmuldfeq
` |-  ( ( ph /\ t e. T ) -> ( X ` t ) = ( Z ` t ) )`
36 18 35 syldan
` |-  ( ( ph /\ t e. D ) -> ( X ` t ) = ( Z ` t ) )`
37 elnnuz
` |-  ( M e. NN <-> M e. ( ZZ>= ` 1 ) )`
38 8 37 sylib
` |-  ( ph -> M e. ( ZZ>= ` 1 ) )`
` |-  ( ( ph /\ t e. D ) -> M e. ( ZZ>= ` 1 ) )`
40 nfv
` |-  F/ i t e. T`
41 1 40 nfan
` |-  F/ i ( ph /\ t e. T )`
42 10 ffvelrnda
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( U ` i ) e. Y )`
43 fveq1
` |-  ( h = ( U ` i ) -> ( h ` t ) = ( ( U ` i ) ` t ) )`
44 43 breq2d
` |-  ( h = ( U ` i ) -> ( 0 <_ ( h ` t ) <-> 0 <_ ( ( U ` i ) ` t ) ) )`
45 43 breq1d
` |-  ( h = ( U ` i ) -> ( ( h ` t ) <_ 1 <-> ( ( U ` i ) ` t ) <_ 1 ) )`
46 44 45 anbi12d
` |-  ( h = ( U ` i ) -> ( ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> ( 0 <_ ( ( U ` i ) ` t ) /\ ( ( U ` i ) ` t ) <_ 1 ) ) )`
47 46 ralbidv
` |-  ( h = ( U ` i ) -> ( A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) <-> A. t e. T ( 0 <_ ( ( U ` i ) ` t ) /\ ( ( U ` i ) ` t ) <_ 1 ) ) )`
48 47 3 elrab2
` |-  ( ( U ` i ) e. Y <-> ( ( U ` i ) e. A /\ A. t e. T ( 0 <_ ( ( U ` i ) ` t ) /\ ( ( U ` i ) ` t ) <_ 1 ) ) )`
49 42 48 sylib
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ( U ` i ) e. A /\ A. t e. T ( 0 <_ ( ( U ` i ) ` t ) /\ ( ( U ` i ) ` t ) <_ 1 ) ) )`
50 49 simpld
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( U ` i ) e. A )`
51 simpl
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ph )`
52 51 50 jca
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( ph /\ ( U ` i ) e. A ) )`
53 eleq1
` |-  ( f = ( U ` i ) -> ( f e. A <-> ( U ` i ) e. A ) )`
54 53 anbi2d
` |-  ( f = ( U ` i ) -> ( ( ph /\ f e. A ) <-> ( ph /\ ( U ` i ) e. A ) ) )`
55 feq1
` |-  ( f = ( U ` i ) -> ( f : T --> RR <-> ( U ` i ) : T --> RR ) )`
56 54 55 imbi12d
` |-  ( f = ( U ` i ) -> ( ( ( ph /\ f e. A ) -> f : T --> RR ) <-> ( ( ph /\ ( U ` i ) e. A ) -> ( U ` i ) : T --> RR ) ) )`
57 56 15 vtoclg
` |-  ( ( U ` i ) e. A -> ( ( ph /\ ( U ` i ) e. A ) -> ( U ` i ) : T --> RR ) )`
58 50 52 57 sylc
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> ( U ` i ) : T --> RR )`
` |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> ( U ` i ) : T --> RR )`
60 simplr
` |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> t e. T )`
61 59 60 ffvelrnd
` |-  ( ( ( ph /\ t e. T ) /\ i e. ( 1 ... M ) ) -> ( ( U ` i ) ` t ) e. RR )`
62 eqid
` |-  ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) = ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) )`
63 41 61 62 fmptdf
` |-  ( ( ph /\ t e. T ) -> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) : ( 1 ... M ) --> RR )`
64 simpr
` |-  ( ( ph /\ t e. T ) -> t e. T )`
65 ovex
` |-  ( 1 ... M ) e. _V`
66 mptexg
` |-  ( ( 1 ... M ) e. _V -> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) e. _V )`
67 65 66 mp1i
` |-  ( ( ph /\ t e. T ) -> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) e. _V )`
68 6 fvmpt2
` |-  ( ( t e. T /\ ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) e. _V ) -> ( F ` t ) = ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )`
69 64 67 68 syl2anc
` |-  ( ( ph /\ t e. T ) -> ( F ` t ) = ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )`
70 69 feq1d
` |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) : ( 1 ... M ) --> RR <-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) : ( 1 ... M ) --> RR ) )`
71 63 70 mpbird
` |-  ( ( ph /\ t e. T ) -> ( F ` t ) : ( 1 ... M ) --> RR )`
72 18 71 syldan
` |-  ( ( ph /\ t e. D ) -> ( F ` t ) : ( 1 ... M ) --> RR )`
73 72 ffvelrnda
` |-  ( ( ( ph /\ t e. D ) /\ k e. ( 1 ... M ) ) -> ( ( F ` t ) ` k ) e. RR )`
74 remulcl
` |-  ( ( k e. RR /\ j e. RR ) -> ( k x. j ) e. RR )`
` |-  ( ( ( ph /\ t e. D ) /\ ( k e. RR /\ j e. RR ) ) -> ( k x. j ) e. RR )`
76 39 73 75 seqcl
` |-  ( ( ph /\ t e. D ) -> ( seq 1 ( x. , ( F ` t ) ) ` M ) e. RR )`
77 7 fvmpt2
` |-  ( ( t e. T /\ ( seq 1 ( x. , ( F ` t ) ) ` M ) e. RR ) -> ( Z ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` M ) )`
78 18 76 77 syl2anc
` |-  ( ( ph /\ t e. D ) -> ( Z ` t ) = ( seq 1 ( x. , ( F ` t ) ) ` M ) )`
79 nfcv
` |-  F/_ i T`
80 nfmpt1
` |-  F/_ i ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) )`
81 79 80 nfmpt
` |-  F/_ i ( t e. T |-> ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) )`
82 6 81 nfcxfr
` |-  F/_ i F`
83 nfcv
` |-  F/_ i t`
84 82 83 nffv
` |-  F/_ i ( F ` t )`
85 nfv
` |-  F/ i t e. D`
86 1 85 nfan
` |-  F/ i ( ph /\ t e. D )`
87 nfcv
` |-  F/_ j seq 1 ( x. , ( F ` t ) )`
88 eqid
` |-  seq 1 ( x. , ( F ` t ) ) = seq 1 ( x. , ( F ` t ) )`
` |-  ( ( ph /\ t e. D ) -> M e. NN )`
90 simpll
` |-  ( ( ( ph /\ t e. D ) /\ i e. ( 1 ... M ) ) -> ph )`
91 simpr
` |-  ( ( ( ph /\ t e. D ) /\ i e. ( 1 ... M ) ) -> i e. ( 1 ... M ) )`
` |-  ( ( ( ph /\ t e. D ) /\ i e. ( 1 ... M ) ) -> t e. T )`
93 49 simprd
` |-  ( ( ph /\ i e. ( 1 ... M ) ) -> A. t e. T ( 0 <_ ( ( U ` i ) ` t ) /\ ( ( U ` i ) ` t ) <_ 1 ) )`
94 93 r19.21bi
` |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. T ) -> ( 0 <_ ( ( U ` i ) ` t ) /\ ( ( U ` i ) ` t ) <_ 1 ) )`
95 94 simpld
` |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. T ) -> 0 <_ ( ( U ` i ) ` t ) )`
96 90 91 92 95 syl21anc
` |-  ( ( ( ph /\ t e. D ) /\ i e. ( 1 ... M ) ) -> 0 <_ ( ( U ` i ) ` t ) )`
97 69 fveq1d
` |-  ( ( ph /\ t e. T ) -> ( ( F ` t ) ` i ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` i ) )`
98 90 92 97 syl2anc
` |-  ( ( ( ph /\ t e. D ) /\ i e. ( 1 ... M ) ) -> ( ( F ` t ) ` i ) = ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` i ) )`
99 90 92 91 61 syl21anc
` |-  ( ( ( ph /\ t e. D ) /\ i e. ( 1 ... M ) ) -> ( ( U ` i ) ` t ) e. RR )`
100 62 fvmpt2
` |-  ( ( i e. ( 1 ... M ) /\ ( ( U ` i ) ` t ) e. RR ) -> ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` i ) = ( ( U ` i ) ` t ) )`
101 91 99 100 syl2anc
` |-  ( ( ( ph /\ t e. D ) /\ i e. ( 1 ... M ) ) -> ( ( i e. ( 1 ... M ) |-> ( ( U ` i ) ` t ) ) ` i ) = ( ( U ` i ) ` t ) )`
102 98 101 eqtrd
` |-  ( ( ( ph /\ t e. D ) /\ i e. ( 1 ... M ) ) -> ( ( F ` t ) ` i ) = ( ( U ` i ) ` t ) )`
103 96 102 breqtrrd
` |-  ( ( ( ph /\ t e. D ) /\ i e. ( 1 ... M ) ) -> 0 <_ ( ( F ` t ) ` i ) )`
104 94 simprd
` |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. T ) -> ( ( U ` i ) ` t ) <_ 1 )`
105 90 91 92 104 syl21anc
` |-  ( ( ( ph /\ t e. D ) /\ i e. ( 1 ... M ) ) -> ( ( U ` i ) ` t ) <_ 1 )`
106 102 105 eqbrtrd
` |-  ( ( ( ph /\ t e. D ) /\ i e. ( 1 ... M ) ) -> ( ( F ` t ) ` i ) <_ 1 )`
` |-  ( ( ph /\ t e. D ) -> E e. RR+ )`
108 11 sselda
` |-  ( ( ph /\ t e. D ) -> t e. U. ran W )`
109 eluni
` |-  ( t e. U. ran W <-> E. w ( t e. w /\ w e. ran W ) )`
110 108 109 sylib
` |-  ( ( ph /\ t e. D ) -> E. w ( t e. w /\ w e. ran W ) )`
111 ffn
` |-  ( W : ( 1 ... M ) --> V -> W Fn ( 1 ... M ) )`
112 fvelrnb
` |-  ( W Fn ( 1 ... M ) -> ( w e. ran W <-> E. j e. ( 1 ... M ) ( W ` j ) = w ) )`
113 9 111 112 3syl
` |-  ( ph -> ( w e. ran W <-> E. j e. ( 1 ... M ) ( W ` j ) = w ) )`
114 113 biimpa
` |-  ( ( ph /\ w e. ran W ) -> E. j e. ( 1 ... M ) ( W ` j ) = w )`
` |-  ( ( ph /\ ( t e. w /\ w e. ran W ) ) -> E. j e. ( 1 ... M ) ( W ` j ) = w )`
116 simplr
` |-  ( ( ( ph /\ t e. w ) /\ ( W ` j ) = w ) -> t e. w )`
117 simpr
` |-  ( ( ( ph /\ t e. w ) /\ ( W ` j ) = w ) -> ( W ` j ) = w )`
118 116 117 eleqtrrd
` |-  ( ( ( ph /\ t e. w ) /\ ( W ` j ) = w ) -> t e. ( W ` j ) )`
119 118 ex
` |-  ( ( ph /\ t e. w ) -> ( ( W ` j ) = w -> t e. ( W ` j ) ) )`
120 119 reximdv
` |-  ( ( ph /\ t e. w ) -> ( E. j e. ( 1 ... M ) ( W ` j ) = w -> E. j e. ( 1 ... M ) t e. ( W ` j ) ) )`
` |-  ( ( ph /\ ( t e. w /\ w e. ran W ) ) -> ( E. j e. ( 1 ... M ) ( W ` j ) = w -> E. j e. ( 1 ... M ) t e. ( W ` j ) ) )`
122 115 121 mpd
` |-  ( ( ph /\ ( t e. w /\ w e. ran W ) ) -> E. j e. ( 1 ... M ) t e. ( W ` j ) )`
123 122 ex
` |-  ( ph -> ( ( t e. w /\ w e. ran W ) -> E. j e. ( 1 ... M ) t e. ( W ` j ) ) )`
124 123 exlimdv
` |-  ( ph -> ( E. w ( t e. w /\ w e. ran W ) -> E. j e. ( 1 ... M ) t e. ( W ` j ) ) )`
` |-  ( ( ph /\ t e. D ) -> ( E. w ( t e. w /\ w e. ran W ) -> E. j e. ( 1 ... M ) t e. ( W ` j ) ) )`
126 110 125 mpd
` |-  ( ( ph /\ t e. D ) -> E. j e. ( 1 ... M ) t e. ( W ` j ) )`
127 simplll
` |-  ( ( ( ( ph /\ t e. D ) /\ j e. ( 1 ... M ) ) /\ t e. ( W ` j ) ) -> ph )`
128 simplr
` |-  ( ( ( ( ph /\ t e. D ) /\ j e. ( 1 ... M ) ) /\ t e. ( W ` j ) ) -> j e. ( 1 ... M ) )`
129 simpr
` |-  ( ( ( ( ph /\ t e. D ) /\ j e. ( 1 ... M ) ) /\ t e. ( W ` j ) ) -> t e. ( W ` j ) )`
130 nfv
` |-  F/ i j e. ( 1 ... M )`
131 nfv
` |-  F/ i t e. ( W ` j )`
132 1 130 131 nf3an
` |-  F/ i ( ph /\ j e. ( 1 ... M ) /\ t e. ( W ` j ) )`
133 nfv
` |-  F/ i ( ( U ` j ) ` t ) < E`
134 132 133 nfim
` |-  F/ i ( ( ph /\ j e. ( 1 ... M ) /\ t e. ( W ` j ) ) -> ( ( U ` j ) ` t ) < E )`
135 eleq1
` |-  ( i = j -> ( i e. ( 1 ... M ) <-> j e. ( 1 ... M ) ) )`
136 fveq2
` |-  ( i = j -> ( W ` i ) = ( W ` j ) )`
137 136 eleq2d
` |-  ( i = j -> ( t e. ( W ` i ) <-> t e. ( W ` j ) ) )`
138 135 137 3anbi23d
` |-  ( i = j -> ( ( ph /\ i e. ( 1 ... M ) /\ t e. ( W ` i ) ) <-> ( ph /\ j e. ( 1 ... M ) /\ t e. ( W ` j ) ) ) )`
139 fveq2
` |-  ( i = j -> ( U ` i ) = ( U ` j ) )`
140 139 fveq1d
` |-  ( i = j -> ( ( U ` i ) ` t ) = ( ( U ` j ) ` t ) )`
141 140 breq1d
` |-  ( i = j -> ( ( ( U ` i ) ` t ) < E <-> ( ( U ` j ) ` t ) < E ) )`
142 138 141 imbi12d
` |-  ( i = j -> ( ( ( ph /\ i e. ( 1 ... M ) /\ t e. ( W ` i ) ) -> ( ( U ` i ) ` t ) < E ) <-> ( ( ph /\ j e. ( 1 ... M ) /\ t e. ( W ` j ) ) -> ( ( U ` j ) ` t ) < E ) ) )`
143 13 r19.21bi
` |-  ( ( ( ph /\ i e. ( 1 ... M ) ) /\ t e. ( W ` i ) ) -> ( ( U ` i ) ` t ) < E )`
144 143 3impa
` |-  ( ( ph /\ i e. ( 1 ... M ) /\ t e. ( W ` i ) ) -> ( ( U ` i ) ` t ) < E )`
145 134 142 144 chvarfv
` |-  ( ( ph /\ j e. ( 1 ... M ) /\ t e. ( W ` j ) ) -> ( ( U ` j ) ` t ) < E )`
146 127 128 129 145 syl3anc
` |-  ( ( ( ( ph /\ t e. D ) /\ j e. ( 1 ... M ) ) /\ t e. ( W ` j ) ) -> ( ( U ` j ) ` t ) < E )`
147 146 ex
` |-  ( ( ( ph /\ t e. D ) /\ j e. ( 1 ... M ) ) -> ( t e. ( W ` j ) -> ( ( U ` j ) ` t ) < E ) )`
148 147 reximdva
` |-  ( ( ph /\ t e. D ) -> ( E. j e. ( 1 ... M ) t e. ( W ` j ) -> E. j e. ( 1 ... M ) ( ( U ` j ) ` t ) < E ) )`
149 126 148 mpd
` |-  ( ( ph /\ t e. D ) -> E. j e. ( 1 ... M ) ( ( U ` j ) ` t ) < E )`
150 86 130 nfan
` |-  F/ i ( ( ph /\ t e. D ) /\ j e. ( 1 ... M ) )`
151 nfcv
` |-  F/_ i j`
152 84 151 nffv
` |-  F/_ i ( ( F ` t ) ` j )`
153 152 nfeq1
` |-  F/ i ( ( F ` t ) ` j ) = ( ( U ` j ) ` t )`
154 150 153 nfim
` |-  F/ i ( ( ( ph /\ t e. D ) /\ j e. ( 1 ... M ) ) -> ( ( F ` t ) ` j ) = ( ( U ` j ) ` t ) )`
155 135 anbi2d
` |-  ( i = j -> ( ( ( ph /\ t e. D ) /\ i e. ( 1 ... M ) ) <-> ( ( ph /\ t e. D ) /\ j e. ( 1 ... M ) ) ) )`
156 fveq2
` |-  ( i = j -> ( ( F ` t ) ` i ) = ( ( F ` t ) ` j ) )`
157 156 140 eqeq12d
` |-  ( i = j -> ( ( ( F ` t ) ` i ) = ( ( U ` i ) ` t ) <-> ( ( F ` t ) ` j ) = ( ( U ` j ) ` t ) ) )`
158 155 157 imbi12d
` |-  ( i = j -> ( ( ( ( ph /\ t e. D ) /\ i e. ( 1 ... M ) ) -> ( ( F ` t ) ` i ) = ( ( U ` i ) ` t ) ) <-> ( ( ( ph /\ t e. D ) /\ j e. ( 1 ... M ) ) -> ( ( F ` t ) ` j ) = ( ( U ` j ) ` t ) ) ) )`
159 154 158 102 chvarfv
` |-  ( ( ( ph /\ t e. D ) /\ j e. ( 1 ... M ) ) -> ( ( F ` t ) ` j ) = ( ( U ` j ) ` t ) )`
160 159 breq1d
` |-  ( ( ( ph /\ t e. D ) /\ j e. ( 1 ... M ) ) -> ( ( ( F ` t ) ` j ) < E <-> ( ( U ` j ) ` t ) < E ) )`
161 160 biimprd
` |-  ( ( ( ph /\ t e. D ) /\ j e. ( 1 ... M ) ) -> ( ( ( U ` j ) ` t ) < E -> ( ( F ` t ) ` j ) < E ) )`
162 161 reximdva
` |-  ( ( ph /\ t e. D ) -> ( E. j e. ( 1 ... M ) ( ( U ` j ) ` t ) < E -> E. j e. ( 1 ... M ) ( ( F ` t ) ` j ) < E ) )`
163 149 162 mpd
` |-  ( ( ph /\ t e. D ) -> E. j e. ( 1 ... M ) ( ( F ` t ) ` j ) < E )`
164 84 86 87 88 89 72 103 106 107 163 fmul01lt1
` |-  ( ( ph /\ t e. D ) -> ( seq 1 ( x. , ( F ` t ) ) ` M ) < E )`
165 78 164 eqbrtrd
` |-  ( ( ph /\ t e. D ) -> ( Z ` t ) < E )`
166 36 165 eqbrtrd
` |-  ( ( ph /\ t e. D ) -> ( X ` t ) < E )`
167 166 ex
` |-  ( ph -> ( t e. D -> ( X ` t ) < E ) )`
168 2 167 ralrimi
` |-  ( ph -> A. t e. D ( X ` t ) < E )`