stoweidlem27

Description: This lemma is used to prove the existence of a function p as in Lemma 1 BrosowskiDeutsh p. 90: p is in the subalgebra, such that 0 <= p <= 1, p__(t_0) = 0, and p > 0 on T - U. Here ( qi ) is used to represent p__(t_i) in the paper. (Contributed by Glauco Siliprandi, 20-Apr-2017)

	Ref	Expression
Hypotheses	stoweidlem27.1	\|- G = ( w e. X \|-> { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } )
	stoweidlem27.2	\|- ( ph -> Q e. _V )
	stoweidlem27.3	\|- ( ph -> M e. NN )
	stoweidlem27.4	\|- ( ph -> Y Fn ran G )
	stoweidlem27.5	\|- ( ph -> ran G e. _V )
	stoweidlem27.6	\|- ( ( ph /\ l e. ran G ) -> ( Y ` l ) e. l )
	stoweidlem27.7	\|- ( ph -> F : ( 1 ... M ) -1-1-onto-> ran G )
	stoweidlem27.8	\|- ( ph -> ( T \ U ) C_ U. X )
	stoweidlem27.9	\|- F/ t ph
	stoweidlem27.10	\|- F/ w ph
	stoweidlem27.11	\|- F/_ h Q
Assertion	stoweidlem27	\|- ( ph -> E. q ( M e. NN /\ ( q : ( 1 ... M ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... M ) 0 < ( ( q ` i ) ` t ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		stoweidlem27.1	\|- G = ( w e. X \|-> { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } )
2		stoweidlem27.2	\|- ( ph -> Q e. _V )
3		stoweidlem27.3	\|- ( ph -> M e. NN )
4		stoweidlem27.4	\|- ( ph -> Y Fn ran G )
5		stoweidlem27.5	\|- ( ph -> ran G e. _V )
6		stoweidlem27.6	\|- ( ( ph /\ l e. ran G ) -> ( Y ` l ) e. l )
7		stoweidlem27.7	\|- ( ph -> F : ( 1 ... M ) -1-1-onto-> ran G )
8		stoweidlem27.8	\|- ( ph -> ( T \ U ) C_ U. X )
9		stoweidlem27.9	\|- F/ t ph
10		stoweidlem27.10	\|- F/ w ph
11		stoweidlem27.11	\|- F/_ h Q
12		fnex	\|- ( ( Y Fn ran G /\ ran G e. _V ) -> Y e. _V )
13	4 5 12	syl2anc	\|- ( ph -> Y e. _V )
14		f1ofn	\|- ( F : ( 1 ... M ) -1-1-onto-> ran G -> F Fn ( 1 ... M ) )
15	7 14	syl	\|- ( ph -> F Fn ( 1 ... M ) )
16		ovex	\|- ( 1 ... M ) e. _V
17		fnex	\|- ( ( F Fn ( 1 ... M ) /\ ( 1 ... M ) e. _V ) -> F e. _V )
18	15 16 17	sylancl	\|- ( ph -> F e. _V )
19		coexg	\|- ( ( Y e. _V /\ F e. _V ) -> ( Y o. F ) e. _V )
20	13 18 19	syl2anc	\|- ( ph -> ( Y o. F ) e. _V )
21		f1of	\|- ( F : ( 1 ... M ) -1-1-onto-> ran G -> F : ( 1 ... M ) --> ran G )
22	7 21	syl	\|- ( ph -> F : ( 1 ... M ) --> ran G )
23		fnfco	\|- ( ( Y Fn ran G /\ F : ( 1 ... M ) --> ran G ) -> ( Y o. F ) Fn ( 1 ... M ) )
24	4 22 23	syl2anc	\|- ( ph -> ( Y o. F ) Fn ( 1 ... M ) )
25		rncoss	\|- ran ( Y o. F ) C_ ran Y
26		fvelrnb	\|- ( Y Fn ran G -> ( k e. ran Y <-> E. l e. ran G ( Y ` l ) = k ) )
27	4 26	syl	\|- ( ph -> ( k e. ran Y <-> E. l e. ran G ( Y ` l ) = k ) )
28	27	biimpa	\|- ( ( ph /\ k e. ran Y ) -> E. l e. ran G ( Y ` l ) = k )
29		nfmpt1	\|- F/_ w ( w e. X \|-> { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } )
30	1 29	nfcxfr	\|- F/_ w G
31	30	nfrn	\|- F/_ w ran G
32	31	nfcri	\|- F/ w l e. ran G
33	10 32	nfan	\|- F/ w ( ph /\ l e. ran G )
34	6	ad2antrr	\|- ( ( ( ( ph /\ l e. ran G ) /\ w e. X ) /\ l = { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } ) -> ( Y ` l ) e. l )
35		simpr	\|- ( ( ( ( ph /\ l e. ran G ) /\ w e. X ) /\ l = { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } ) -> l = { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } )
36	34 35	eleqtrd	\|- ( ( ( ( ph /\ l e. ran G ) /\ w e. X ) /\ l = { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } ) -> ( Y ` l ) e. { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } )
37		nfcv	\|- F/_ h ( Y ` l )
38		nfv	\|- F/ h w = { t e. T \| 0 < ( ( Y ` l ) ` t ) }
39		fveq1	\|- ( h = ( Y ` l ) -> ( h ` t ) = ( ( Y ` l ) ` t ) )
40	39	breq2d	\|- ( h = ( Y ` l ) -> ( 0 < ( h ` t ) <-> 0 < ( ( Y ` l ) ` t ) ) )
41	40	rabbidv	\|- ( h = ( Y ` l ) -> { t e. T \| 0 < ( h ` t ) } = { t e. T \| 0 < ( ( Y ` l ) ` t ) } )
42	41	eqeq2d	\|- ( h = ( Y ` l ) -> ( w = { t e. T \| 0 < ( h ` t ) } <-> w = { t e. T \| 0 < ( ( Y ` l ) ` t ) } ) )
43	37 11 38 42	elrabf	\|- ( ( Y ` l ) e. { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } <-> ( ( Y ` l ) e. Q /\ w = { t e. T \| 0 < ( ( Y ` l ) ` t ) } ) )
44	36 43	sylib	\|- ( ( ( ( ph /\ l e. ran G ) /\ w e. X ) /\ l = { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } ) -> ( ( Y ` l ) e. Q /\ w = { t e. T \| 0 < ( ( Y ` l ) ` t ) } ) )
45	44	simpld	\|- ( ( ( ( ph /\ l e. ran G ) /\ w e. X ) /\ l = { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } ) -> ( Y ` l ) e. Q )
46		simpr	\|- ( ( ph /\ l e. ran G ) -> l e. ran G )
47	1	elrnmpt	\|- ( l e. ran G -> ( l e. ran G <-> E. w e. X l = { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } ) )
48	46 47	syl	\|- ( ( ph /\ l e. ran G ) -> ( l e. ran G <-> E. w e. X l = { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } ) )
49	46 48	mpbid	\|- ( ( ph /\ l e. ran G ) -> E. w e. X l = { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } )
50	33 45 49	r19.29af	\|- ( ( ph /\ l e. ran G ) -> ( Y ` l ) e. Q )
51	50	adantlr	\|- ( ( ( ph /\ k e. ran Y ) /\ l e. ran G ) -> ( Y ` l ) e. Q )
52		eleq1	\|- ( ( Y ` l ) = k -> ( ( Y ` l ) e. Q <-> k e. Q ) )
53	51 52	syl5ibcom	\|- ( ( ( ph /\ k e. ran Y ) /\ l e. ran G ) -> ( ( Y ` l ) = k -> k e. Q ) )
54	53	reximdva	\|- ( ( ph /\ k e. ran Y ) -> ( E. l e. ran G ( Y ` l ) = k -> E. l e. ran G k e. Q ) )
55	28 54	mpd	\|- ( ( ph /\ k e. ran Y ) -> E. l e. ran G k e. Q )
56		idd	\|- ( l e. ran G -> ( k e. Q -> k e. Q ) )
57	56	a1i	\|- ( ( ph /\ k e. ran Y ) -> ( l e. ran G -> ( k e. Q -> k e. Q ) ) )
58	57	rexlimdv	\|- ( ( ph /\ k e. ran Y ) -> ( E. l e. ran G k e. Q -> k e. Q ) )
59	55 58	mpd	\|- ( ( ph /\ k e. ran Y ) -> k e. Q )
60	59	ex	\|- ( ph -> ( k e. ran Y -> k e. Q ) )
61	60	ssrdv	\|- ( ph -> ran Y C_ Q )
62	25 61	sstrid	\|- ( ph -> ran ( Y o. F ) C_ Q )
63		df-f	\|- ( ( Y o. F ) : ( 1 ... M ) --> Q <-> ( ( Y o. F ) Fn ( 1 ... M ) /\ ran ( Y o. F ) C_ Q ) )
64	24 62 63	sylanbrc	\|- ( ph -> ( Y o. F ) : ( 1 ... M ) --> Q )
65		nfv	\|- F/ w t e. ( T \ U )
66	10 65	nfan	\|- F/ w ( ph /\ t e. ( T \ U ) )
67		nfv	\|- F/ w E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t )
68	8	sselda	\|- ( ( ph /\ t e. ( T \ U ) ) -> t e. U. X )
69		eluni	\|- ( t e. U. X <-> E. w ( t e. w /\ w e. X ) )
70	68 69	sylib	\|- ( ( ph /\ t e. ( T \ U ) ) -> E. w ( t e. w /\ w e. X ) )
71	1	funmpt2	\|- Fun G
72	1	dmeqi	\|- dom G = dom ( w e. X \|-> { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } )
73	11	rabexgf	\|- ( Q e. _V -> { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } e. _V )
74	2 73	syl	\|- ( ph -> { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } e. _V )
75	74	adantr	\|- ( ( ph /\ w e. X ) -> { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } e. _V )
76	75	ex	\|- ( ph -> ( w e. X -> { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } e. _V ) )
77	10 76	ralrimi	\|- ( ph -> A. w e. X { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } e. _V )
78		dmmptg	\|- ( A. w e. X { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } e. _V -> dom ( w e. X \|-> { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } ) = X )
79	77 78	syl	\|- ( ph -> dom ( w e. X \|-> { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } ) = X )
80	72 79	syl5eq	\|- ( ph -> dom G = X )
81	80	eleq2d	\|- ( ph -> ( w e. dom G <-> w e. X ) )
82	81	biimpar	\|- ( ( ph /\ w e. X ) -> w e. dom G )
83		fvelrn	\|- ( ( Fun G /\ w e. dom G ) -> ( G ` w ) e. ran G )
84	71 82 83	sylancr	\|- ( ( ph /\ w e. X ) -> ( G ` w ) e. ran G )
85	84	adantrl	\|- ( ( ph /\ ( t e. w /\ w e. X ) ) -> ( G ` w ) e. ran G )
86	22	ad2antrr	\|- ( ( ( ph /\ ( G ` w ) e. ran G ) /\ ( i e. ( 1 ... M ) /\ ( F ` i ) = ( G ` w ) ) ) -> F : ( 1 ... M ) --> ran G )
87		simprl	\|- ( ( ( ph /\ ( G ` w ) e. ran G ) /\ ( i e. ( 1 ... M ) /\ ( F ` i ) = ( G ` w ) ) ) -> i e. ( 1 ... M ) )
88		fvco3	\|- ( ( F : ( 1 ... M ) --> ran G /\ i e. ( 1 ... M ) ) -> ( ( Y o. F ) ` i ) = ( Y ` ( F ` i ) ) )
89	86 87 88	syl2anc	\|- ( ( ( ph /\ ( G ` w ) e. ran G ) /\ ( i e. ( 1 ... M ) /\ ( F ` i ) = ( G ` w ) ) ) -> ( ( Y o. F ) ` i ) = ( Y ` ( F ` i ) ) )
90		fveq2	\|- ( ( F ` i ) = ( G ` w ) -> ( Y ` ( F ` i ) ) = ( Y ` ( G ` w ) ) )
91	90	ad2antll	\|- ( ( ( ph /\ ( G ` w ) e. ran G ) /\ ( i e. ( 1 ... M ) /\ ( F ` i ) = ( G ` w ) ) ) -> ( Y ` ( F ` i ) ) = ( Y ` ( G ` w ) ) )
92	89 91	eqtrd	\|- ( ( ( ph /\ ( G ` w ) e. ran G ) /\ ( i e. ( 1 ... M ) /\ ( F ` i ) = ( G ` w ) ) ) -> ( ( Y o. F ) ` i ) = ( Y ` ( G ` w ) ) )
93		eleq1	\|- ( l = ( G ` w ) -> ( l e. ran G <-> ( G ` w ) e. ran G ) )
94	93	anbi2d	\|- ( l = ( G ` w ) -> ( ( ph /\ l e. ran G ) <-> ( ph /\ ( G ` w ) e. ran G ) ) )
95		eleq2	\|- ( l = ( G ` w ) -> ( ( Y ` l ) e. l <-> ( Y ` l ) e. ( G ` w ) ) )
96		fveq2	\|- ( l = ( G ` w ) -> ( Y ` l ) = ( Y ` ( G ` w ) ) )
97	96	eleq1d	\|- ( l = ( G ` w ) -> ( ( Y ` l ) e. ( G ` w ) <-> ( Y ` ( G ` w ) ) e. ( G ` w ) ) )
98	95 97	bitrd	\|- ( l = ( G ` w ) -> ( ( Y ` l ) e. l <-> ( Y ` ( G ` w ) ) e. ( G ` w ) ) )
99	94 98	imbi12d	\|- ( l = ( G ` w ) -> ( ( ( ph /\ l e. ran G ) -> ( Y ` l ) e. l ) <-> ( ( ph /\ ( G ` w ) e. ran G ) -> ( Y ` ( G ` w ) ) e. ( G ` w ) ) ) )
100	99 6	vtoclg	\|- ( ( G ` w ) e. ran G -> ( ( ph /\ ( G ` w ) e. ran G ) -> ( Y ` ( G ` w ) ) e. ( G ` w ) ) )
101	100	anabsi7	\|- ( ( ph /\ ( G ` w ) e. ran G ) -> ( Y ` ( G ` w ) ) e. ( G ` w ) )
102	101	adantr	\|- ( ( ( ph /\ ( G ` w ) e. ran G ) /\ ( i e. ( 1 ... M ) /\ ( F ` i ) = ( G ` w ) ) ) -> ( Y ` ( G ` w ) ) e. ( G ` w ) )
103	92 102	eqeltrd	\|- ( ( ( ph /\ ( G ` w ) e. ran G ) /\ ( i e. ( 1 ... M ) /\ ( F ` i ) = ( G ` w ) ) ) -> ( ( Y o. F ) ` i ) e. ( G ` w ) )
104		f1ofo	\|- ( F : ( 1 ... M ) -1-1-onto-> ran G -> F : ( 1 ... M ) -onto-> ran G )
105		forn	\|- ( F : ( 1 ... M ) -onto-> ran G -> ran F = ran G )
106	7 104 105	3syl	\|- ( ph -> ran F = ran G )
107	106	eleq2d	\|- ( ph -> ( ( G ` w ) e. ran F <-> ( G ` w ) e. ran G ) )
108	107	biimpar	\|- ( ( ph /\ ( G ` w ) e. ran G ) -> ( G ` w ) e. ran F )
109	15	adantr	\|- ( ( ph /\ ( G ` w ) e. ran G ) -> F Fn ( 1 ... M ) )
110		fvelrnb	\|- ( F Fn ( 1 ... M ) -> ( ( G ` w ) e. ran F <-> E. i e. ( 1 ... M ) ( F ` i ) = ( G ` w ) ) )
111	109 110	syl	\|- ( ( ph /\ ( G ` w ) e. ran G ) -> ( ( G ` w ) e. ran F <-> E. i e. ( 1 ... M ) ( F ` i ) = ( G ` w ) ) )
112	108 111	mpbid	\|- ( ( ph /\ ( G ` w ) e. ran G ) -> E. i e. ( 1 ... M ) ( F ` i ) = ( G ` w ) )
113	103 112	reximddv	\|- ( ( ph /\ ( G ` w ) e. ran G ) -> E. i e. ( 1 ... M ) ( ( Y o. F ) ` i ) e. ( G ` w ) )
114	85 113	syldan	\|- ( ( ph /\ ( t e. w /\ w e. X ) ) -> E. i e. ( 1 ... M ) ( ( Y o. F ) ` i ) e. ( G ` w ) )
115		simplrl	\|- ( ( ( ph /\ ( t e. w /\ w e. X ) ) /\ ( ( Y o. F ) ` i ) e. ( G ` w ) ) -> t e. w )
116		simpr	\|- ( ( ph /\ w e. X ) -> w e. X )
117	1	fvmpt2	\|- ( ( w e. X /\ { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } e. _V ) -> ( G ` w ) = { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } )
118	116 75 117	syl2anc	\|- ( ( ph /\ w e. X ) -> ( G ` w ) = { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } )
119	118	eleq2d	\|- ( ( ph /\ w e. X ) -> ( ( ( Y o. F ) ` i ) e. ( G ` w ) <-> ( ( Y o. F ) ` i ) e. { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } ) )
120	119	biimpa	\|- ( ( ( ph /\ w e. X ) /\ ( ( Y o. F ) ` i ) e. ( G ` w ) ) -> ( ( Y o. F ) ` i ) e. { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } )
121	120	adantlrl	\|- ( ( ( ph /\ ( t e. w /\ w e. X ) ) /\ ( ( Y o. F ) ` i ) e. ( G ` w ) ) -> ( ( Y o. F ) ` i ) e. { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } )
122		nfcv	\|- F/_ h ( ( Y o. F ) ` i )
123		nfv	\|- F/ h w = { t e. T \| 0 < ( ( ( Y o. F ) ` i ) ` t ) }
124		fveq1	\|- ( h = ( ( Y o. F ) ` i ) -> ( h ` t ) = ( ( ( Y o. F ) ` i ) ` t ) )
125	124	breq2d	\|- ( h = ( ( Y o. F ) ` i ) -> ( 0 < ( h ` t ) <-> 0 < ( ( ( Y o. F ) ` i ) ` t ) ) )
126	125	rabbidv	\|- ( h = ( ( Y o. F ) ` i ) -> { t e. T \| 0 < ( h ` t ) } = { t e. T \| 0 < ( ( ( Y o. F ) ` i ) ` t ) } )
127	126	eqeq2d	\|- ( h = ( ( Y o. F ) ` i ) -> ( w = { t e. T \| 0 < ( h ` t ) } <-> w = { t e. T \| 0 < ( ( ( Y o. F ) ` i ) ` t ) } ) )
128	122 11 123 127	elrabf	\|- ( ( ( Y o. F ) ` i ) e. { h e. Q \| w = { t e. T \| 0 < ( h ` t ) } } <-> ( ( ( Y o. F ) ` i ) e. Q /\ w = { t e. T \| 0 < ( ( ( Y o. F ) ` i ) ` t ) } ) )
129	121 128	sylib	\|- ( ( ( ph /\ ( t e. w /\ w e. X ) ) /\ ( ( Y o. F ) ` i ) e. ( G ` w ) ) -> ( ( ( Y o. F ) ` i ) e. Q /\ w = { t e. T \| 0 < ( ( ( Y o. F ) ` i ) ` t ) } ) )
130	129	simprd	\|- ( ( ( ph /\ ( t e. w /\ w e. X ) ) /\ ( ( Y o. F ) ` i ) e. ( G ` w ) ) -> w = { t e. T \| 0 < ( ( ( Y o. F ) ` i ) ` t ) } )
131	115 130	eleqtrd	\|- ( ( ( ph /\ ( t e. w /\ w e. X ) ) /\ ( ( Y o. F ) ` i ) e. ( G ` w ) ) -> t e. { t e. T \| 0 < ( ( ( Y o. F ) ` i ) ` t ) } )
132		rabid	\|- ( t e. { t e. T \| 0 < ( ( ( Y o. F ) ` i ) ` t ) } <-> ( t e. T /\ 0 < ( ( ( Y o. F ) ` i ) ` t ) ) )
133	131 132	sylib	\|- ( ( ( ph /\ ( t e. w /\ w e. X ) ) /\ ( ( Y o. F ) ` i ) e. ( G ` w ) ) -> ( t e. T /\ 0 < ( ( ( Y o. F ) ` i ) ` t ) ) )
134	133	simprd	\|- ( ( ( ph /\ ( t e. w /\ w e. X ) ) /\ ( ( Y o. F ) ` i ) e. ( G ` w ) ) -> 0 < ( ( ( Y o. F ) ` i ) ` t ) )
135	134	ex	\|- ( ( ph /\ ( t e. w /\ w e. X ) ) -> ( ( ( Y o. F ) ` i ) e. ( G ` w ) -> 0 < ( ( ( Y o. F ) ` i ) ` t ) ) )
136	135	reximdv	\|- ( ( ph /\ ( t e. w /\ w e. X ) ) -> ( E. i e. ( 1 ... M ) ( ( Y o. F ) ` i ) e. ( G ` w ) -> E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t ) ) )
137	114 136	mpd	\|- ( ( ph /\ ( t e. w /\ w e. X ) ) -> E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t ) )
138	137	ex	\|- ( ph -> ( ( t e. w /\ w e. X ) -> E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t ) ) )
139	138	adantr	\|- ( ( ph /\ t e. ( T \ U ) ) -> ( ( t e. w /\ w e. X ) -> E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t ) ) )
140	66 67 70 139	exlimimdd	\|- ( ( ph /\ t e. ( T \ U ) ) -> E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t ) )
141	140	ex	\|- ( ph -> ( t e. ( T \ U ) -> E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t ) ) )
142	9 141	ralrimi	\|- ( ph -> A. t e. ( T \ U ) E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t ) )
143	3 64 142	jca32	\|- ( ph -> ( M e. NN /\ ( ( Y o. F ) : ( 1 ... M ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t ) ) ) )
144		feq1	\|- ( q = ( Y o. F ) -> ( q : ( 1 ... M ) --> Q <-> ( Y o. F ) : ( 1 ... M ) --> Q ) )
145		fveq1	\|- ( q = ( Y o. F ) -> ( q ` i ) = ( ( Y o. F ) ` i ) )
146	145	fveq1d	\|- ( q = ( Y o. F ) -> ( ( q ` i ) ` t ) = ( ( ( Y o. F ) ` i ) ` t ) )
147	146	breq2d	\|- ( q = ( Y o. F ) -> ( 0 < ( ( q ` i ) ` t ) <-> 0 < ( ( ( Y o. F ) ` i ) ` t ) ) )
148	147	rexbidv	\|- ( q = ( Y o. F ) -> ( E. i e. ( 1 ... M ) 0 < ( ( q ` i ) ` t ) <-> E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t ) ) )
149	148	ralbidv	\|- ( q = ( Y o. F ) -> ( A. t e. ( T \ U ) E. i e. ( 1 ... M ) 0 < ( ( q ` i ) ` t ) <-> A. t e. ( T \ U ) E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t ) ) )
150	144 149	anbi12d	\|- ( q = ( Y o. F ) -> ( ( q : ( 1 ... M ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... M ) 0 < ( ( q ` i ) ` t ) ) <-> ( ( Y o. F ) : ( 1 ... M ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t ) ) ) )
151	150	anbi2d	\|- ( q = ( Y o. F ) -> ( ( M e. NN /\ ( q : ( 1 ... M ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... M ) 0 < ( ( q ` i ) ` t ) ) ) <-> ( M e. NN /\ ( ( Y o. F ) : ( 1 ... M ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t ) ) ) ) )
152	151	spcegv	\|- ( ( Y o. F ) e. _V -> ( ( M e. NN /\ ( ( Y o. F ) : ( 1 ... M ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... M ) 0 < ( ( ( Y o. F ) ` i ) ` t ) ) ) -> E. q ( M e. NN /\ ( q : ( 1 ... M ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... M ) 0 < ( ( q ` i ) ` t ) ) ) ) )
153	20 143 152	sylc	\|- ( ph -> E. q ( M e. NN /\ ( q : ( 1 ... M ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... M ) 0 < ( ( q ` i ) ` t ) ) ) )

Metamath Proof Explorer

Theorem stoweidlem27

Proof