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 ) )
39	38	adantr	\|- ( ( 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	ffvelcdmda	\|- ( ( 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 )
59	58	adantlr	\|- ( ( ( 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	ffvelcdmd	\|- ( ( ( 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	ffvelcdmda	\|- ( ( ( 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 )
75	74	adantl	\|- ( ( ( 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 ) )
89	8	adantr	\|- ( ( 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 ) )
92	18	adantr	\|- ( ( ( 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 )
107	17	adantr	\|- ( ( 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 )
115	114	adantrl	\|- ( ( 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 ) ) )
121	120	adantrr	\|- ( ( 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 ) ) )
125	124	adantr	\|- ( ( 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 )

Metamath Proof Explorer

Theorem stoweidlem48

Proof