Theorem stoweidlem35 40252

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

Hypotheses

Ref	Expression
stoweidlem35.1	|- F/ t ph
stoweidlem35.2	|- F/ w ph
stoweidlem35.3	|- F/ h ph
stoweidlem35.4	|- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
stoweidlem35.5	|- W = { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } }
stoweidlem35.6	|- G = ( w e. X |-> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
stoweidlem35.7	|- ( ph -> A e. _V )
stoweidlem35.8	|- ( ph -> X e. Fin )
stoweidlem35.9	|- ( ph -> X C_ W )
stoweidlem35.10	|- ( ph -> ( T \ U ) C_ U. X )
stoweidlem35.11	|- ( ph -> ( T \ U ) =/= (/) )

Assertion

Ref	Expression
stoweidlem35	|- ( ph -> E. m E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )

Distinct variable groups:   h, i, t, w   i, m, q, t   i, G   w, Q   T, h, w   U, q   ph, i, m   A, h, t   h, X, i, t, w   w, m   m, G   Q, q   T, q   t, Z   w, U

Allowed substitution hints:   ph( w, t, h, q)   A( w, i, m, q)   Q( t, h, i, m)   T( t, i, m)   U( t, h, i, m)   G( w, t, h, q)   J( w, t, h, i, m, q)   W( w, t, h, i, m, q)   X( m, q)   Z( w, h, i, m, q)

Proof of Theorem stoweidlem35

Dummy variables k f g l are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		stoweidlem35.8	. . . . . . . . . 10 |- ( ph -> X e. Fin )
2		stoweidlem35.6	. . . . . . . . . . 11 |- G = ( w e. X |-> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
3	2	rnmptfi 39351	. . . . . . . . . 10 |- ( X e. Fin -> ran G e. Fin )
4	1, 3	syl 17	. . . . . . . . 9 |- ( ph -> ran G e. Fin )
5		fnchoice 39188	. . . . . . . . . . 11 |- ( ran G e. Fin -> E. g ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) )
6	5	adantl 482	. . . . . . . . . 10 |- ( ( ph /\ ran G e. Fin ) -> E. g ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) )
7		simprl 794	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) -> g Fn ran G )
8		stoweidlem35.2	. . . . . . . . . . . . . . . . . . . . 21 |- F/ w ph
9		nfmpt1 4747	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/_ w ( w e. X |-> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
10	2, 9	nfcxfr 2762	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/_ w G
11	10	nfrn 5368	. . . . . . . . . . . . . . . . . . . . . 22 |- F/_ w ran G
12	11	nfcri 2758	. . . . . . . . . . . . . . . . . . . . 21 |- F/ w k e. ran G
13	8, 12	nfan 1828	. . . . . . . . . . . . . . . . . . . 20 |- F/ w ( ph /\ k e. ran G )
14		stoweidlem35.9	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> X C_ W )
15	14	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ w e. X ) -> w e. W )
16		stoweidlem35.5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- W = { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } }
17	15, 16	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ w e. X ) -> w e. { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } } )
18		rabid 3116	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( w e. { w e. J | E. h e. Q w = { t e. T | 0 < ( h ` t ) } } <-> ( w e. J /\ E. h e. Q w = { t e. T | 0 < ( h ` t ) } ) )
19	17, 18	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ w e. X ) -> ( w e. J /\ E. h e. Q w = { t e. T | 0 < ( h ` t ) } ) )
20	19	simprd 479	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ w e. X ) -> E. h e. Q w = { t e. T | 0 < ( h ` t ) } )
21		df-rex 2918	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( E. h e. Q w = { t e. T | 0 < ( h ` t ) } <-> E. h ( h e. Q /\ w = { t e. T | 0 < ( h ` t ) } ) )
22	20, 21	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ w e. X ) -> E. h ( h e. Q /\ w = { t e. T | 0 < ( h ` t ) } ) )
23		rabid 3116	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } <-> ( h e. Q /\ w = { t e. T | 0 < ( h ` t ) } ) )
24	23	exbii 1774	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( E. h h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } <-> E. h ( h e. Q /\ w = { t e. T | 0 < ( h ` t ) } ) )
25	22, 24	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ w e. X ) -> E. h h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
26	25	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ w e. X ) /\ k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) -> E. h h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
27		stoweidlem35.3	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/ h ph
28		nfv 1843	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/ h w e. X
29	27, 28	nfan 1828	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/ h ( ph /\ w e. X )
30		nfrab1 3122	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ h { h e. Q | w = { t e. T | 0 < ( h ` t ) } }
31	30	nfeq2 2780	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/ h k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } }
32	29, 31	nfan 1828	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/ h ( ( ph /\ w e. X ) /\ k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
33		eleq2 2690	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } -> ( h e. k <-> h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) )
34	33	biimprd 238	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } -> ( h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } -> h e. k ) )
35	34	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ w e. X ) /\ k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) -> ( h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } -> h e. k ) )
36	32, 35	eximd 2085	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ w e. X ) /\ k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) -> ( E. h h e. { h e. Q | w = { t e. T | 0 < ( h ` t ) } } -> E. h h e. k ) )
37	26, 36	mpd 15	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ w e. X ) /\ k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) -> E. h h e. k )
38	37	adantllr 755	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ k e. ran G ) /\ w e. X ) /\ k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) -> E. h h e. k )
39	2	elrnmpt 5372	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. ran G -> ( k e. ran G <-> E. w e. X k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } ) )
40	39	ibi 256	. . . . . . . . . . . . . . . . . . . . 21 |- ( k e. ran G -> E. w e. X k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
41	40	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. ran G ) -> E. w e. X k = { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
42	13, 38, 41	r19.29af 3076	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. ran G ) -> E. h h e. k )
43		n0 3931	. . . . . . . . . . . . . . . . . . 19 |- ( k =/= (/) <-> E. h h e. k )
44	42, 43	sylibr 224	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. ran G ) -> k =/= (/) )
45	44	adantlr 751	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) /\ k e. ran G ) -> k =/= (/) )
46		simplrr 801	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) /\ k e. ran G ) -> A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) )
47		neeq1 2856	. . . . . . . . . . . . . . . . . . . 20 |- ( l = k -> ( l =/= (/) <-> k =/= (/) ) )
48		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22 |- ( l = k -> ( g ` l ) = ( g ` k ) )
49	48	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . 21 |- ( l = k -> ( ( g ` l ) e. l <-> ( g ` k ) e. l ) )
50		eleq2 2690	. . . . . . . . . . . . . . . . . . . . 21 |- ( l = k -> ( ( g ` k ) e. l <-> ( g ` k ) e. k ) )
51	49, 50	bitrd 268	. . . . . . . . . . . . . . . . . . . 20 |- ( l = k -> ( ( g ` l ) e. l <-> ( g ` k ) e. k ) )
52	47, 51	imbi12d 334	. . . . . . . . . . . . . . . . . . 19 |- ( l = k -> ( ( l =/= (/) -> ( g ` l ) e. l ) <-> ( k =/= (/) -> ( g ` k ) e. k ) ) )
53	52	rspccva 3308	. . . . . . . . . . . . . . . . . 18 |- ( ( A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) /\ k e. ran G ) -> ( k =/= (/) -> ( g ` k ) e. k ) )
54	46, 53	sylancom 701	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) /\ k e. ran G ) -> ( k =/= (/) -> ( g ` k ) e. k ) )
55	45, 54	mpd 15	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) /\ k e. ran G ) -> ( g ` k ) e. k )
56	55	ralrimiva 2966	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) -> A. k e. ran G ( g ` k ) e. k )
57		fveq2 6191	. . . . . . . . . . . . . . . . . 18 |- ( k = l -> ( g ` k ) = ( g ` l ) )
58	57	eleq1d 2686	. . . . . . . . . . . . . . . . 17 |- ( k = l -> ( ( g ` k ) e. k <-> ( g ` l ) e. k ) )
59		eleq2 2690	. . . . . . . . . . . . . . . . 17 |- ( k = l -> ( ( g ` l ) e. k <-> ( g ` l ) e. l ) )
60	58, 59	bitrd 268	. . . . . . . . . . . . . . . 16 |- ( k = l -> ( ( g ` k ) e. k <-> ( g ` l ) e. l ) )
61	60	cbvralv 3171	. . . . . . . . . . . . . . 15 |- ( A. k e. ran G ( g ` k ) e. k <-> A. l e. ran G ( g ` l ) e. l )
62	56, 61	sylib 208	. . . . . . . . . . . . . 14 |- ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) -> A. l e. ran G ( g ` l ) e. l )
63	7, 62	jca 554	. . . . . . . . . . . . 13 |- ( ( ph /\ ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) ) -> ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) )
64	63	ex 450	. . . . . . . . . . . 12 |- ( ph -> ( ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) -> ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) ) )
65	64	adantr 481	. . . . . . . . . . 11 |- ( ( ph /\ ran G e. Fin ) -> ( ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) -> ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) ) )
66	65	eximdv 1846	. . . . . . . . . 10 |- ( ( ph /\ ran G e. Fin ) -> ( E. g ( g Fn ran G /\ A. l e. ran G ( l =/= (/) -> ( g ` l ) e. l ) ) -> E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) ) )
67	6, 66	mpd 15	. . . . . . . . 9 |- ( ( ph /\ ran G e. Fin ) -> E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) )
68	4, 67	mpdan 702	. . . . . . . 8 |- ( ph -> E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) )
69	68	ralrimivw 2967	. . . . . . 7 |- ( ph -> A. m e. NN E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) )
70		stoweidlem35.10	. . . . . . . . . . . . 13 |- ( ph -> ( T \ U ) C_ U. X )
71		stoweidlem35.11	. . . . . . . . . . . . 13 |- ( ph -> ( T \ U ) =/= (/) )
72		ssn0 3976	. . . . . . . . . . . . 13 |- ( ( ( T \ U ) C_ U. X /\ ( T \ U ) =/= (/) ) -> U. X =/= (/) )
73	70, 71, 72	syl2anc 693	. . . . . . . . . . . 12 |- ( ph -> U. X =/= (/) )
74	73	neneqd 2799	. . . . . . . . . . 11 |- ( ph -> -. U. X = (/) )
75		unieq 4444	. . . . . . . . . . . 12 |- ( X = (/) -> U. X = U. (/) )
76		uni0 4465	. . . . . . . . . . . 12 |- U. (/) = (/)
77	75, 76	syl6eq 2672	. . . . . . . . . . 11 |- ( X = (/) -> U. X = (/) )
78	74, 77	nsyl 135	. . . . . . . . . 10 |- ( ph -> -. X = (/) )
79		dm0rn0 5342	. . . . . . . . . . 11 |- ( dom G = (/) <-> ran G = (/) )
80		stoweidlem35.4	. . . . . . . . . . . . . . . . . 18 |- Q = { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
81		stoweidlem35.7	. . . . . . . . . . . . . . . . . 18 |- ( ph -> A e. _V )
82	80, 81	rabexd 4814	. . . . . . . . . . . . . . . . 17 |- ( ph -> Q e. _V )
83		nfrab1 3122	. . . . . . . . . . . . . . . . . . 19 |- F/_ h { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
84	80, 83	nfcxfr 2762	. . . . . . . . . . . . . . . . . 18 |- F/_ h Q
85	84	rabexgf 39183	. . . . . . . . . . . . . . . . 17 |- ( Q e. _V -> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } e. _V )
86	82, 85	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } e. _V )
87	86	adantr 481	. . . . . . . . . . . . . . 15 |- ( ( ph /\ w e. X ) -> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } e. _V )
88	8, 87, 2	fmptdf 6387	. . . . . . . . . . . . . 14 |- ( ph -> G : X --> _V )
89		dffn2 6047	. . . . . . . . . . . . . 14 |- ( G Fn X <-> G : X --> _V )
90	88, 89	sylibr 224	. . . . . . . . . . . . 13 |- ( ph -> G Fn X )
91		fndm 5990	. . . . . . . . . . . . 13 |- ( G Fn X -> dom G = X )
92	90, 91	syl 17	. . . . . . . . . . . 12 |- ( ph -> dom G = X )
93	92	eqeq1d 2624	. . . . . . . . . . 11 |- ( ph -> ( dom G = (/) <-> X = (/) ) )
94	79, 93	syl5bbr 274	. . . . . . . . . 10 |- ( ph -> ( ran G = (/) <-> X = (/) ) )
95	78, 94	mtbird 315	. . . . . . . . 9 |- ( ph -> -. ran G = (/) )
96		fz1f1o 14441	. . . . . . . . . . 11 |- ( ran G e. Fin -> ( ran G = (/) \/ ( ( # ` ran G ) e. NN /\ E. f f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) ) )
97	4, 96	syl 17	. . . . . . . . . 10 |- ( ph -> ( ran G = (/) \/ ( ( # ` ran G ) e. NN /\ E. f f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) ) )
98	97	ord 392	. . . . . . . . 9 |- ( ph -> ( -. ran G = (/) -> ( ( # ` ran G ) e. NN /\ E. f f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) ) )
99	95, 98	mpd 15	. . . . . . . 8 |- ( ph -> ( ( # ` ran G ) e. NN /\ E. f f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) )
100		oveq2 6658	. . . . . . . . . . 11 |- ( m = ( # ` ran G ) -> ( 1 ... m ) = ( 1 ... ( # ` ran G ) ) )
101		f1oeq2 6128	. . . . . . . . . . 11 |- ( ( 1 ... m ) = ( 1 ... ( # ` ran G ) ) -> ( f : ( 1 ... m ) -1-1-onto-> ran G <-> f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) )
102	100, 101	syl 17	. . . . . . . . . 10 |- ( m = ( # ` ran G ) -> ( f : ( 1 ... m ) -1-1-onto-> ran G <-> f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) )
103	102	exbidv 1850	. . . . . . . . 9 |- ( m = ( # ` ran G ) -> ( E. f f : ( 1 ... m ) -1-1-onto-> ran G <-> E. f f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) )
104	103	rspcev 3309	. . . . . . . 8 |- ( ( ( # ` ran G ) e. NN /\ E. f f : ( 1 ... ( # ` ran G ) ) -1-1-onto-> ran G ) -> E. m e. NN E. f f : ( 1 ... m ) -1-1-onto-> ran G )
105	99, 104	syl 17	. . . . . . 7 |- ( ph -> E. m e. NN E. f f : ( 1 ... m ) -1-1-onto-> ran G )
106		r19.29 3072	. . . . . . 7 |- ( ( A. m e. NN E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. m e. NN E. f f : ( 1 ... m ) -1-1-onto-> ran G ) -> E. m e. NN ( E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. f f : ( 1 ... m ) -1-1-onto-> ran G ) )
107	69, 105, 106	syl2anc 693	. . . . . 6 |- ( ph -> E. m e. NN ( E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. f f : ( 1 ... m ) -1-1-onto-> ran G ) )
108		eeanv 2182	. . . . . . . . 9 |- ( E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) <-> ( E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. f f : ( 1 ... m ) -1-1-onto-> ran G ) )
109	108	biimpri 218	. . . . . . . 8 |- ( ( E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. f f : ( 1 ... m ) -1-1-onto-> ran G ) -> E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) )
110	109	a1i 11	. . . . . . 7 |- ( ph -> ( ( E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. f f : ( 1 ... m ) -1-1-onto-> ran G ) -> E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
111	110	reximdv 3016	. . . . . 6 |- ( ph -> ( E. m e. NN ( E. g ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ E. f f : ( 1 ... m ) -1-1-onto-> ran G ) -> E. m e. NN E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
112	107, 111	mpd 15	. . . . 5 |- ( ph -> E. m e. NN E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) )
113		df-rex 2918	. . . . 5 |- ( E. m e. NN E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) <-> E. m ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
114	112, 113	sylib 208	. . . 4 |- ( ph -> E. m ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
115		ax-5 1839	. . . . . . . . 9 |- ( m e. NN -> A. g m e. NN )
116		19.29 1801	. . . . . . . . 9 |- ( ( A. g m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g ( m e. NN /\ E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
117	115, 116	sylan 488	. . . . . . . 8 |- ( ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g ( m e. NN /\ E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
118		ax-5 1839	. . . . . . . . . 10 |- ( m e. NN -> A. f m e. NN )
119		19.29 1801	. . . . . . . . . 10 |- ( ( A. f m e. NN /\ E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. f ( m e. NN /\ ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
120	118, 119	sylan 488	. . . . . . . . 9 |- ( ( m e. NN /\ E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. f ( m e. NN /\ ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
121	120	eximi 1762	. . . . . . . 8 |- ( E. g ( m e. NN /\ E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g E. f ( m e. NN /\ ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
122	117, 121	syl 17	. . . . . . 7 |- ( ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g E. f ( m e. NN /\ ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
123		df-3an 1039	. . . . . . . . 9 |- ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) <-> ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) )
124	123	anbi2i 730	. . . . . . . 8 |- ( ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) <-> ( m e. NN /\ ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
125	124	2exbii 1775	. . . . . . 7 |- ( E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) <-> E. g E. f ( m e. NN /\ ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
126	122, 125	sylibr 224	. . . . . 6 |- ( ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
127	126	a1i 11	. . . . 5 |- ( ph -> ( ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) )
128	127	eximdv 1846	. . . 4 |- ( ph -> ( E. m ( m e. NN /\ E. g E. f ( ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l ) /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. m E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) )
129	114, 128	mpd 15	. . 3 |- ( ph -> E. m E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
130	82	adantr 481	. . . . . . 7 |- ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> Q e. _V )
131		simprl 794	. . . . . . 7 |- ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> m e. NN )
132		simprr1 1109	. . . . . . 7 |- ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> g Fn ran G )
133		elex 3212	. . . . . . . . 9 |- ( ran G e. Fin -> ran G e. _V )
134	4, 133	syl 17	. . . . . . . 8 |- ( ph -> ran G e. _V )
135	134	adantr 481	. . . . . . 7 |- ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> ran G e. _V )
136		simprr2 1110	. . . . . . . 8 |- ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> A. l e. ran G ( g ` l ) e. l )
137	51	rspccva 3308	. . . . . . . 8 |- ( ( A. l e. ran G ( g ` l ) e. l /\ k e. ran G ) -> ( g ` k ) e. k )
138	136, 137	sylan 488	. . . . . . 7 |- ( ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) /\ k e. ran G ) -> ( g ` k ) e. k )
139		simprr3 1111	. . . . . . 7 |- ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> f : ( 1 ... m ) -1-1-onto-> ran G )
140	70	adantr 481	. . . . . . 7 |- ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> ( T \ U ) C_ U. X )
141		stoweidlem35.1	. . . . . . . 8 |- F/ t ph
142		nfv 1843	. . . . . . . . 9 |- F/ t m e. NN
143		nfcv 2764	. . . . . . . . . . 11 |- F/_ t g
144		nfcv 2764	. . . . . . . . . . . . . 14 |- F/_ t X
145		nfrab1 3122	. . . . . . . . . . . . . . . 16 |- F/_ t { t e. T | 0 < ( h ` t ) }
146	145	nfeq2 2780	. . . . . . . . . . . . . . 15 |- F/ t w = { t e. T | 0 < ( h ` t ) }
147		nfv 1843	. . . . . . . . . . . . . . . . . 18 |- F/ t ( h ` Z ) = 0
148		nfra1 2941	. . . . . . . . . . . . . . . . . 18 |- F/ t A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 )
149	147, 148	nfan 1828	. . . . . . . . . . . . . . . . 17 |- F/ t ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) )
150		nfcv 2764	. . . . . . . . . . . . . . . . 17 |- F/_ t A
151	149, 150	nfrab 3123	. . . . . . . . . . . . . . . 16 |- F/_ t { h e. A | ( ( h ` Z ) = 0 /\ A. t e. T ( 0 <_ ( h ` t ) /\ ( h ` t ) <_ 1 ) ) }
152	80, 151	nfcxfr 2762	. . . . . . . . . . . . . . 15 |- F/_ t Q
153	146, 152	nfrab 3123	. . . . . . . . . . . . . 14 |- F/_ t { h e. Q | w = { t e. T | 0 < ( h ` t ) } }
154	144, 153	nfmpt 4746	. . . . . . . . . . . . 13 |- F/_ t ( w e. X |-> { h e. Q | w = { t e. T | 0 < ( h ` t ) } } )
155	2, 154	nfcxfr 2762	. . . . . . . . . . . 12 |- F/_ t G
156	155	nfrn 5368	. . . . . . . . . . 11 |- F/_ t ran G
157	143, 156	nffn 5987	. . . . . . . . . 10 |- F/ t g Fn ran G
158		nfv 1843	. . . . . . . . . . 11 |- F/ t ( g ` l ) e. l
159	156, 158	nfral 2945	. . . . . . . . . 10 |- F/ t A. l e. ran G ( g ` l ) e. l
160		nfcv 2764	. . . . . . . . . . 11 |- F/_ t f
161		nfcv 2764	. . . . . . . . . . 11 |- F/_ t ( 1 ... m )
162	160, 161, 156	nff1o 6135	. . . . . . . . . 10 |- F/ t f : ( 1 ... m ) -1-1-onto-> ran G
163	157, 159, 162	nf3an 1831	. . . . . . . . 9 |- F/ t ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G )
164	142, 163	nfan 1828	. . . . . . . 8 |- F/ t ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) )
165	141, 164	nfan 1828	. . . . . . 7 |- F/ t ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
166		nfv 1843	. . . . . . . . 9 |- F/ w m e. NN
167		nfcv 2764	. . . . . . . . . . 11 |- F/_ w g
168	167, 11	nffn 5987	. . . . . . . . . 10 |- F/ w g Fn ran G
169		nfv 1843	. . . . . . . . . . 11 |- F/ w ( g ` l ) e. l
170	11, 169	nfral 2945	. . . . . . . . . 10 |- F/ w A. l e. ran G ( g ` l ) e. l
171		nfcv 2764	. . . . . . . . . . 11 |- F/_ w f
172		nfcv 2764	. . . . . . . . . . 11 |- F/_ w ( 1 ... m )
173	171, 172, 11	nff1o 6135	. . . . . . . . . 10 |- F/ w f : ( 1 ... m ) -1-1-onto-> ran G
174	168, 170, 173	nf3an 1831	. . . . . . . . 9 |- F/ w ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G )
175	166, 174	nfan 1828	. . . . . . . 8 |- F/ w ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) )
176	8, 175	nfan 1828	. . . . . . 7 |- F/ w ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) )
177	2, 130, 131, 132, 135, 138, 139, 140, 165, 176, 84	stoweidlem27 40244	. . . . . 6 |- ( ( ph /\ ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) ) -> E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )
178	177	ex 450	. . . . 5 |- ( ph -> ( ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) )
179	178	2eximdv 1848	. . . 4 |- ( ph -> ( E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. g E. f E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) )
180	179	eximdv 1846	. . 3 |- ( ph -> ( E. m E. g E. f ( m e. NN /\ ( g Fn ran G /\ A. l e. ran G ( g ` l ) e. l /\ f : ( 1 ... m ) -1-1-onto-> ran G ) ) -> E. m E. g E. f E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) ) )
181	129, 180	mpd 15	. 2 |- ( ph -> E. m E. g E. f E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )
182		id 22	. . . 4 |- ( E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` 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 ) ) ) )
183	182	exlimivv 1860	. . 3 |- ( E. g E. f E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` 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 ) ) ) )
184	183	eximi 1762	. 2 |- ( E. m E. g E. f E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) -> E. m E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )
185	181, 184	syl 17	1 |- ( ph -> E. m E. q ( m e. NN /\ ( q : ( 1 ... m ) --> Q /\ A. t e. ( T \ U ) E. i e. ( 1 ... m ) 0 < ( ( q ` i ) ` t ) ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   /\ w3a 1037   A.wal 1481   = wceq 1483   E.wex 1704   F/wnf 1708   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   C_ wss 3574   (/)c0 3915   U.cuni 4436   class class class wbr 4653   |-> cmpt 4729   dom cdm 5114   ran crn 5115   Fn wfn 5883   -->wf 5884   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   Fincfn 7955   0cc0 9936   1c1 9937   < clt 10074   <_ cle 10075   NNcn 11020   ...cfz 12326   #chash 13117

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-1st 7168  df-2nd 7169  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-nn 11021  df-n0 11293  df-z 11378  df-uz 11688  df-fz 12327  df-hash 13118

This theorem is referenced by:  stoweidlem53  40270