Theorem sdclem2

Description: Lemma for sdc . (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypotheses	sdc.1	|- Z = ( ZZ>= ` M )
	sdc.2	|- ( g = ( f |` ( M ... n ) ) -> ( ps <-> ch ) )
	sdc.3	|- ( n = M -> ( ps <-> ta ) )
	sdc.4	|- ( n = k -> ( ps <-> th ) )
	sdc.5	|- ( ( g = h /\ n = ( k + 1 ) ) -> ( ps <-> si ) )
	sdc.6	|- ( ph -> A e. V )
	sdc.7	|- ( ph -> M e. ZZ )
	sdc.8	|- ( ph -> E. g ( g : { M } --> A /\ ta ) )
	sdc.9	|- ( ( ph /\ k e. Z ) -> ( ( g : ( M ... k ) --> A /\ th ) -> E. h ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) ) )
	sdc.10	|- J = { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) }
	sdc.11	|- F = ( w e. Z , x e. J |-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } )
	sdc.12	|- F/ k ph
	sdc.13	|- ( ph -> G : Z --> J )
	sdc.14	|- ( ph -> ( G ` M ) : ( M ... M ) --> A )
	sdc.15	|- ( ( ph /\ w e. Z ) -> ( G ` ( w + 1 ) ) e. ( w F ( G ` w ) ) )
Assertion	sdclem2	|- ( ph -> E. f ( f : Z --> A /\ A. n e. Z ch ) )

Proof

Step	Hyp	Ref	Expression
1		sdc.1	|- Z = ( ZZ>= ` M )
2		sdc.2	|- ( g = ( f |` ( M ... n ) ) -> ( ps <-> ch ) )
3		sdc.3	|- ( n = M -> ( ps <-> ta ) )
4		sdc.4	|- ( n = k -> ( ps <-> th ) )
5		sdc.5	|- ( ( g = h /\ n = ( k + 1 ) ) -> ( ps <-> si ) )
6		sdc.6	|- ( ph -> A e. V )
7		sdc.7	|- ( ph -> M e. ZZ )
8		sdc.8	|- ( ph -> E. g ( g : { M } --> A /\ ta ) )
9		sdc.9	|- ( ( ph /\ k e. Z ) -> ( ( g : ( M ... k ) --> A /\ th ) -> E. h ( h : ( M ... ( k + 1 ) ) --> A /\ g = ( h |` ( M ... k ) ) /\ si ) ) )
10		sdc.10	|- J = { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) }
11		sdc.11	|- F = ( w e. Z , x e. J |-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } )
12		sdc.12	|- F/ k ph
13		sdc.13	|- ( ph -> G : Z --> J )
14		sdc.14	|- ( ph -> ( G ` M ) : ( M ... M ) --> A )
15		sdc.15	|- ( ( ph /\ w e. Z ) -> ( G ` ( w + 1 ) ) e. ( w F ( G ` w ) ) )
16	13	ffvelcdmda	|- ( ( ph /\ k e. Z ) -> ( G ` k ) e. J )
17	10	eleq2i	|- ( ( G ` k ) e. J <-> ( G ` k ) e. { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } )
18		nfcv	|- F/_ g Z
19		nfv	|- F/ g ( G ` k ) : ( M ... n ) --> A
20		nfsbc1v	|- F/ g [. ( G ` k ) / g ]. ps
21	19 20	nfan	|- F/ g ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps )
22	18 21	nfrexw	|- F/ g E. n e. Z ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps )
23		fvex	|- ( G ` k ) e. _V
24		feq1	|- ( g = ( G ` k ) -> ( g : ( M ... n ) --> A <-> ( G ` k ) : ( M ... n ) --> A ) )
25		sbceq1a	|- ( g = ( G ` k ) -> ( ps <-> [. ( G ` k ) / g ]. ps ) )
26	24 25	anbi12d	|- ( g = ( G ` k ) -> ( ( g : ( M ... n ) --> A /\ ps ) <-> ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps ) ) )
27	26	rexbidv	|- ( g = ( G ` k ) -> ( E. n e. Z ( g : ( M ... n ) --> A /\ ps ) <-> E. n e. Z ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps ) ) )
28	22 23 27	elabf	|- ( ( G ` k ) e. { g | E. n e. Z ( g : ( M ... n ) --> A /\ ps ) } <-> E. n e. Z ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps ) )
29	17 28	bitri	|- ( ( G ` k ) e. J <-> E. n e. Z ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps ) )
30	16 29	sylib	|- ( ( ph /\ k e. Z ) -> E. n e. Z ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps ) )
31		fdm	|- ( ( G ` k ) : ( M ... n ) --> A -> dom ( G ` k ) = ( M ... n ) )
32	31	adantr	|- ( ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps ) -> dom ( G ` k ) = ( M ... n ) )
33		fveq2	|- ( x = M -> ( G ` x ) = ( G ` M ) )
34		oveq2	|- ( x = M -> ( M ... x ) = ( M ... M ) )
35	34	mpteq1d	|- ( x = M -> ( m e. ( M ... x ) |-> ( ( G ` m ) ` m ) ) = ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) )
36	33 35	eqeq12d	|- ( x = M -> ( ( G ` x ) = ( m e. ( M ... x ) |-> ( ( G ` m ) ` m ) ) <-> ( G ` M ) = ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) ) )
37	36	imbi2d	|- ( x = M -> ( ( ph -> ( G ` x ) = ( m e. ( M ... x ) |-> ( ( G ` m ) ` m ) ) ) <-> ( ph -> ( G ` M ) = ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) ) ) )
38		fveq2	|- ( x = w -> ( G ` x ) = ( G ` w ) )
39		oveq2	|- ( x = w -> ( M ... x ) = ( M ... w ) )
40	39	mpteq1d	|- ( x = w -> ( m e. ( M ... x ) |-> ( ( G ` m ) ` m ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) )
41	38 40	eqeq12d	|- ( x = w -> ( ( G ` x ) = ( m e. ( M ... x ) |-> ( ( G ` m ) ` m ) ) <-> ( G ` w ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) )
42	41	imbi2d	|- ( x = w -> ( ( ph -> ( G ` x ) = ( m e. ( M ... x ) |-> ( ( G ` m ) ` m ) ) ) <-> ( ph -> ( G ` w ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) )
43		fveq2	|- ( x = ( w + 1 ) -> ( G ` x ) = ( G ` ( w + 1 ) ) )
44		oveq2	|- ( x = ( w + 1 ) -> ( M ... x ) = ( M ... ( w + 1 ) ) )
45	44	mpteq1d	|- ( x = ( w + 1 ) -> ( m e. ( M ... x ) |-> ( ( G ` m ) ` m ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) )
46	43 45	eqeq12d	|- ( x = ( w + 1 ) -> ( ( G ` x ) = ( m e. ( M ... x ) |-> ( ( G ` m ) ` m ) ) <-> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ) )
47	46	imbi2d	|- ( x = ( w + 1 ) -> ( ( ph -> ( G ` x ) = ( m e. ( M ... x ) |-> ( ( G ` m ) ` m ) ) ) <-> ( ph -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ) ) )
48		fveq2	|- ( x = k -> ( G ` x ) = ( G ` k ) )
49		oveq2	|- ( x = k -> ( M ... x ) = ( M ... k ) )
50	49	mpteq1d	|- ( x = k -> ( m e. ( M ... x ) |-> ( ( G ` m ) ` m ) ) = ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) )
51	48 50	eqeq12d	|- ( x = k -> ( ( G ` x ) = ( m e. ( M ... x ) |-> ( ( G ` m ) ` m ) ) <-> ( G ` k ) = ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) ) )
52	51	imbi2d	|- ( x = k -> ( ( ph -> ( G ` x ) = ( m e. ( M ... x ) |-> ( ( G ` m ) ` m ) ) ) <-> ( ph -> ( G ` k ) = ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) ) ) )
53		fveq2	|- ( m = k -> ( G ` m ) = ( G ` k ) )
54		id	|- ( m = k -> m = k )
55	53 54	fveq12d	|- ( m = k -> ( ( G ` m ) ` m ) = ( ( G ` k ) ` k ) )
56		eqid	|- ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) = ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) )
57		fvex	|- ( ( G ` k ) ` k ) e. _V
58	55 56 57	fvmpt	|- ( k e. ( M ... M ) -> ( ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) ` k ) = ( ( G ` k ) ` k ) )
59	58	adantl	|- ( ( ph /\ k e. ( M ... M ) ) -> ( ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) ` k ) = ( ( G ` k ) ` k ) )
60		elfz1eq	|- ( k e. ( M ... M ) -> k = M )
61	60	adantl	|- ( ( ph /\ k e. ( M ... M ) ) -> k = M )
62	61	fveq2d	|- ( ( ph /\ k e. ( M ... M ) ) -> ( G ` k ) = ( G ` M ) )
63	62	fveq1d	|- ( ( ph /\ k e. ( M ... M ) ) -> ( ( G ` k ) ` k ) = ( ( G ` M ) ` k ) )
64	59 63	eqtr2d	|- ( ( ph /\ k e. ( M ... M ) ) -> ( ( G ` M ) ` k ) = ( ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) ` k ) )
65	64	ex	|- ( ph -> ( k e. ( M ... M ) -> ( ( G ` M ) ` k ) = ( ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) ` k ) ) )
66	12 65	ralrimi	|- ( ph -> A. k e. ( M ... M ) ( ( G ` M ) ` k ) = ( ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) ` k ) )
67	14	ffnd	|- ( ph -> ( G ` M ) Fn ( M ... M ) )
68		fvex	|- ( ( G ` m ) ` m ) e. _V
69	68 56	fnmpti	|- ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) Fn ( M ... M )
70		eqfnfv	|- ( ( ( G ` M ) Fn ( M ... M ) /\ ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) Fn ( M ... M ) ) -> ( ( G ` M ) = ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) <-> A. k e. ( M ... M ) ( ( G ` M ) ` k ) = ( ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) ` k ) ) )
71	67 69 70	sylancl	|- ( ph -> ( ( G ` M ) = ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) <-> A. k e. ( M ... M ) ( ( G ` M ) ` k ) = ( ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) ` k ) ) )
72	66 71	mpbird	|- ( ph -> ( G ` M ) = ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) )
73	72	a1i	|- ( M e. ZZ -> ( ph -> ( G ` M ) = ( m e. ( M ... M ) |-> ( ( G ` m ) ` m ) ) ) )
74	1	eleq2i	|- ( w e. Z <-> w e. ( ZZ>= ` M ) )
75	13	ffvelcdmda	|- ( ( ph /\ w e. Z ) -> ( G ` w ) e. J )
76		simpr	|- ( ( ph /\ w e. Z ) -> w e. Z )
77		3simpa	|- ( ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) -> ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) )
78	77	reximi	|- ( E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) -> E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) )
79	78	ss2abi	|- { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } C_ { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) }
80	1	fvexi	|- Z e. _V
81		nfv	|- F/ k w e. Z
82	12 81	nfan	|- F/ k ( ph /\ w e. Z )
83	6	adantr	|- ( ( ph /\ w e. Z ) -> A e. V )
84		simpl	|- ( ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) -> h : ( M ... ( k + 1 ) ) --> A )
85		ovex	|- ( M ... ( k + 1 ) ) e. _V
86		elmapg	|- ( ( A e. V /\ ( M ... ( k + 1 ) ) e. _V ) -> ( h e. ( A ^m ( M ... ( k + 1 ) ) ) <-> h : ( M ... ( k + 1 ) ) --> A ) )
87	85 86	mpan2	|- ( A e. V -> ( h e. ( A ^m ( M ... ( k + 1 ) ) ) <-> h : ( M ... ( k + 1 ) ) --> A ) )
88	84 87	imbitrrid	|- ( A e. V -> ( ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) -> h e. ( A ^m ( M ... ( k + 1 ) ) ) ) )
89	88	abssdv	|- ( A e. V -> { h | ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } C_ ( A ^m ( M ... ( k + 1 ) ) ) )
90	83 89	syl	|- ( ( ph /\ w e. Z ) -> { h | ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } C_ ( A ^m ( M ... ( k + 1 ) ) ) )
91		ovex	|- ( A ^m ( M ... ( k + 1 ) ) ) e. _V
92		ssexg	|- ( ( { h | ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } C_ ( A ^m ( M ... ( k + 1 ) ) ) /\ ( A ^m ( M ... ( k + 1 ) ) ) e. _V ) -> { h | ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } e. _V )
93	90 91 92	sylancl	|- ( ( ph /\ w e. Z ) -> { h | ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } e. _V )
94	93	a1d	|- ( ( ph /\ w e. Z ) -> ( k e. Z -> { h | ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } e. _V ) )
95	82 94	ralrimi	|- ( ( ph /\ w e. Z ) -> A. k e. Z { h | ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } e. _V )
96		abrexex2g	|- ( ( Z e. _V /\ A. k e. Z { h | ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } e. _V ) -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } e. _V )
97	80 95 96	sylancr	|- ( ( ph /\ w e. Z ) -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } e. _V )
98		ssexg	|- ( ( { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } C_ { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } /\ { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } e. _V ) -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } e. _V )
99	79 97 98	sylancr	|- ( ( ph /\ w e. Z ) -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } e. _V )
100		eqeq1	|- ( x = ( G ` w ) -> ( x = ( h |` ( M ... k ) ) <-> ( G ` w ) = ( h |` ( M ... k ) ) ) )
101	100	3anbi2d	|- ( x = ( G ` w ) -> ( ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) <-> ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) ) )
102	101	rexbidv	|- ( x = ( G ` w ) -> ( E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) <-> E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) ) )
103	102	abbidv	|- ( x = ( G ` w ) -> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } )
104	103	eleq1d	|- ( x = ( G ` w ) -> ( { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. _V <-> { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } e. _V ) )
105		oveq2	|- ( x = ( G ` w ) -> ( w F x ) = ( w F ( G ` w ) ) )
106	105 103	eqeq12d	|- ( x = ( G ` w ) -> ( ( w F x ) = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } <-> ( w F ( G ` w ) ) = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } ) )
107	104 106	imbi12d	|- ( x = ( G ` w ) -> ( ( { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. _V -> ( w F x ) = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } ) <-> ( { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } e. _V -> ( w F ( G ` w ) ) = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } ) ) )
108	107	imbi2d	|- ( x = ( G ` w ) -> ( ( w e. Z -> ( { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. _V -> ( w F x ) = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } ) ) <-> ( w e. Z -> ( { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } e. _V -> ( w F ( G ` w ) ) = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } ) ) ) )
109	11	ovmpt4g	|- ( ( w e. Z /\ x e. J /\ { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. _V ) -> ( w F x ) = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } )
110	109	3com12	|- ( ( x e. J /\ w e. Z /\ { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. _V ) -> ( w F x ) = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } )
111	110	3exp	|- ( x e. J -> ( w e. Z -> ( { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } e. _V -> ( w F x ) = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ x = ( h |` ( M ... k ) ) /\ si ) } ) ) )
112	108 111	vtoclga	|- ( ( G ` w ) e. J -> ( w e. Z -> ( { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } e. _V -> ( w F ( G ` w ) ) = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } ) ) )
113	75 76 99 112	syl3c	|- ( ( ph /\ w e. Z ) -> ( w F ( G ` w ) ) = { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) /\ si ) } )
114	113 79	eqsstrdi	|- ( ( ph /\ w e. Z ) -> ( w F ( G ` w ) ) C_ { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } )
115	114 15	sseldd	|- ( ( ph /\ w e. Z ) -> ( G ` ( w + 1 ) ) e. { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } )
116		fvex	|- ( G ` ( w + 1 ) ) e. _V
117		feq1	|- ( h = ( G ` ( w + 1 ) ) -> ( h : ( M ... ( k + 1 ) ) --> A <-> ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A ) )
118		reseq1	|- ( h = ( G ` ( w + 1 ) ) -> ( h |` ( M ... k ) ) = ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) )
119	118	eqeq2d	|- ( h = ( G ` ( w + 1 ) ) -> ( ( G ` w ) = ( h |` ( M ... k ) ) <-> ( G ` w ) = ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) ) )
120	117 119	anbi12d	|- ( h = ( G ` ( w + 1 ) ) -> ( ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) <-> ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) ) ) )
121	120	rexbidv	|- ( h = ( G ` ( w + 1 ) ) -> ( E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) <-> E. k e. Z ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) ) ) )
122	116 121	elab	|- ( ( G ` ( w + 1 ) ) e. { h | E. k e. Z ( h : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( h |` ( M ... k ) ) ) } <-> E. k e. Z ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) ) )
123	115 122	sylib	|- ( ( ph /\ w e. Z ) -> E. k e. Z ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) ) )
124		nfv	|- F/ k ( ( G ` w ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) )
125		simprl	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A )
126		fzssp1	|- ( M ... k ) C_ ( M ... ( k + 1 ) )
127		fssres	|- ( ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( M ... k ) C_ ( M ... ( k + 1 ) ) ) -> ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) : ( M ... k ) --> A )
128	125 126 127	sylancl	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) : ( M ... k ) --> A )
129	128	fdmd	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> dom ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( M ... k ) )
130		eqid	|- ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) )
131	68 130	fnmpti	|- ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) Fn ( M ... w )
132		simprr	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) )
133	132	fneq1d	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) Fn ( M ... w ) <-> ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) Fn ( M ... w ) ) )
134	131 133	mpbiri	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) Fn ( M ... w ) )
135	134	fndmd	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> dom ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( M ... w ) )
136	129 135	eqtr3d	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( M ... k ) = ( M ... w ) )
137		simplr	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> k e. Z )
138	137 1	eleqtrdi	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> k e. ( ZZ>= ` M ) )
139		fzopth	|- ( k e. ( ZZ>= ` M ) -> ( ( M ... k ) = ( M ... w ) <-> ( M = M /\ k = w ) ) )
140	138 139	syl	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( ( M ... k ) = ( M ... w ) <-> ( M = M /\ k = w ) ) )
141	136 140	mpbid	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( M = M /\ k = w ) )
142	141	simprd	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> k = w )
143	142	oveq1d	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( k + 1 ) = ( w + 1 ) )
144	143	oveq2d	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( M ... ( k + 1 ) ) = ( M ... ( w + 1 ) ) )
145		elfzp1	|- ( k e. ( ZZ>= ` M ) -> ( x e. ( M ... ( k + 1 ) ) <-> ( x e. ( M ... k ) \/ x = ( k + 1 ) ) ) )
146	138 145	syl	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( x e. ( M ... ( k + 1 ) ) <-> ( x e. ( M ... k ) \/ x = ( k + 1 ) ) ) )
147	136	reseq2d	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) |` ( M ... k ) ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) |` ( M ... w ) ) )
148		fzssp1	|- ( M ... w ) C_ ( M ... ( w + 1 ) )
149		resmpt	|- ( ( M ... w ) C_ ( M ... ( w + 1 ) ) -> ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) |` ( M ... w ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) )
150	148 149	ax-mp	|- ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) |` ( M ... w ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) )
151	147 150	eqtr2di	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) |` ( M ... k ) ) )
152	132 151	eqtrd	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) |` ( M ... k ) ) )
153	152	fveq1d	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) ` x ) = ( ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) |` ( M ... k ) ) ` x ) )
154		fvres	|- ( x e. ( M ... k ) -> ( ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) ` x ) = ( ( G ` ( w + 1 ) ) ` x ) )
155		fvres	|- ( x e. ( M ... k ) -> ( ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) |` ( M ... k ) ) ` x ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` x ) )
156	154 155	eqeq12d	|- ( x e. ( M ... k ) -> ( ( ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) ` x ) = ( ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) |` ( M ... k ) ) ` x ) <-> ( ( G ` ( w + 1 ) ) ` x ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` x ) ) )
157	153 156	syl5ibcom	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( x e. ( M ... k ) -> ( ( G ` ( w + 1 ) ) ` x ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` x ) ) )
158	143	eqeq2d	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( x = ( k + 1 ) <-> x = ( w + 1 ) ) )
159	142 138	eqeltrrd	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> w e. ( ZZ>= ` M ) )
160		peano2uz	|- ( w e. ( ZZ>= ` M ) -> ( w + 1 ) e. ( ZZ>= ` M ) )
161		eluzfz2	|- ( ( w + 1 ) e. ( ZZ>= ` M ) -> ( w + 1 ) e. ( M ... ( w + 1 ) ) )
162		fveq2	|- ( m = ( w + 1 ) -> ( G ` m ) = ( G ` ( w + 1 ) ) )
163		id	|- ( m = ( w + 1 ) -> m = ( w + 1 ) )
164	162 163	fveq12d	|- ( m = ( w + 1 ) -> ( ( G ` m ) ` m ) = ( ( G ` ( w + 1 ) ) ` ( w + 1 ) ) )
165		eqid	|- ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) )
166		fvex	|- ( ( G ` ( w + 1 ) ) ` ( w + 1 ) ) e. _V
167	164 165 166	fvmpt	|- ( ( w + 1 ) e. ( M ... ( w + 1 ) ) -> ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` ( w + 1 ) ) = ( ( G ` ( w + 1 ) ) ` ( w + 1 ) ) )
168	159 160 161 167	4syl	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` ( w + 1 ) ) = ( ( G ` ( w + 1 ) ) ` ( w + 1 ) ) )
169	168	eqcomd	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( ( G ` ( w + 1 ) ) ` ( w + 1 ) ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` ( w + 1 ) ) )
170		fveq2	|- ( x = ( w + 1 ) -> ( ( G ` ( w + 1 ) ) ` x ) = ( ( G ` ( w + 1 ) ) ` ( w + 1 ) ) )
171		fveq2	|- ( x = ( w + 1 ) -> ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` x ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` ( w + 1 ) ) )
172	170 171	eqeq12d	|- ( x = ( w + 1 ) -> ( ( ( G ` ( w + 1 ) ) ` x ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` x ) <-> ( ( G ` ( w + 1 ) ) ` ( w + 1 ) ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` ( w + 1 ) ) ) )
173	169 172	syl5ibrcom	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( x = ( w + 1 ) -> ( ( G ` ( w + 1 ) ) ` x ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` x ) ) )
174	158 173	sylbid	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( x = ( k + 1 ) -> ( ( G ` ( w + 1 ) ) ` x ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` x ) ) )
175	157 174	jaod	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( ( x e. ( M ... k ) \/ x = ( k + 1 ) ) -> ( ( G ` ( w + 1 ) ) ` x ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` x ) ) )
176	146 175	sylbid	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( x e. ( M ... ( k + 1 ) ) -> ( ( G ` ( w + 1 ) ) ` x ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` x ) ) )
177	176	ralrimiv	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> A. x e. ( M ... ( k + 1 ) ) ( ( G ` ( w + 1 ) ) ` x ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` x ) )
178		ffn	|- ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A -> ( G ` ( w + 1 ) ) Fn ( M ... ( k + 1 ) ) )
179	178	ad2antrl	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( G ` ( w + 1 ) ) Fn ( M ... ( k + 1 ) ) )
180	68 165	fnmpti	|- ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) Fn ( M ... ( w + 1 ) )
181		eqfnfv2	|- ( ( ( G ` ( w + 1 ) ) Fn ( M ... ( k + 1 ) ) /\ ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) Fn ( M ... ( w + 1 ) ) ) -> ( ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) <-> ( ( M ... ( k + 1 ) ) = ( M ... ( w + 1 ) ) /\ A. x e. ( M ... ( k + 1 ) ) ( ( G ` ( w + 1 ) ) ` x ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` x ) ) ) )
182	179 180 181	sylancl	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) <-> ( ( M ... ( k + 1 ) ) = ( M ... ( w + 1 ) ) /\ A. x e. ( M ... ( k + 1 ) ) ( ( G ` ( w + 1 ) ) ` x ) = ( ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ` x ) ) ) )
183	144 177 182	mpbir2and	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) ) -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) )
184	183	expr	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A ) -> ( ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ) )
185		eqeq1	|- ( ( G ` w ) = ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) -> ( ( G ` w ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) <-> ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) )
186	185	imbi1d	|- ( ( G ` w ) = ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) -> ( ( ( G ` w ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ) <-> ( ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ) ) )
187	184 186	syl5ibrcom	|- ( ( ( ( ph /\ w e. Z ) /\ k e. Z ) /\ ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A ) -> ( ( G ` w ) = ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) -> ( ( G ` w ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ) ) )
188	187	expimpd	|- ( ( ( ph /\ w e. Z ) /\ k e. Z ) -> ( ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) ) -> ( ( G ` w ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ) ) )
189	188	ex	|- ( ( ph /\ w e. Z ) -> ( k e. Z -> ( ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) ) -> ( ( G ` w ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ) ) ) )
190	82 124 189	rexlimd	|- ( ( ph /\ w e. Z ) -> ( E. k e. Z ( ( G ` ( w + 1 ) ) : ( M ... ( k + 1 ) ) --> A /\ ( G ` w ) = ( ( G ` ( w + 1 ) ) |` ( M ... k ) ) ) -> ( ( G ` w ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ) ) )
191	123 190	mpd	|- ( ( ph /\ w e. Z ) -> ( ( G ` w ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ) )
192	191	expcom	|- ( w e. Z -> ( ph -> ( ( G ` w ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ) ) )
193	74 192	sylbir	|- ( w e. ( ZZ>= ` M ) -> ( ph -> ( ( G ` w ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ) ) )
194	193	a2d	|- ( w e. ( ZZ>= ` M ) -> ( ( ph -> ( G ` w ) = ( m e. ( M ... w ) |-> ( ( G ` m ) ` m ) ) ) -> ( ph -> ( G ` ( w + 1 ) ) = ( m e. ( M ... ( w + 1 ) ) |-> ( ( G ` m ) ` m ) ) ) ) )
195	37 42 47 52 73 194	uzind4	|- ( k e. ( ZZ>= ` M ) -> ( ph -> ( G ` k ) = ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) ) )
196	195 1	eleq2s	|- ( k e. Z -> ( ph -> ( G ` k ) = ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) ) )
197	196	impcom	|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) )
198	197	dmeqd	|- ( ( ph /\ k e. Z ) -> dom ( G ` k ) = dom ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) )
199		dmmptg	|- ( A. m e. ( M ... k ) ( ( G ` m ) ` m ) e. _V -> dom ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) = ( M ... k ) )
200	68	a1i	|- ( m e. ( M ... k ) -> ( ( G ` m ) ` m ) e. _V )
201	199 200	mprg	|- dom ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) = ( M ... k )
202	198 201	eqtrdi	|- ( ( ph /\ k e. Z ) -> dom ( G ` k ) = ( M ... k ) )
203	202	eqeq1d	|- ( ( ph /\ k e. Z ) -> ( dom ( G ` k ) = ( M ... n ) <-> ( M ... k ) = ( M ... n ) ) )
204		simpr	|- ( ( ph /\ k e. Z ) -> k e. Z )
205	204 1	eleqtrdi	|- ( ( ph /\ k e. Z ) -> k e. ( ZZ>= ` M ) )
206		fzopth	|- ( k e. ( ZZ>= ` M ) -> ( ( M ... k ) = ( M ... n ) <-> ( M = M /\ k = n ) ) )
207	205 206	syl	|- ( ( ph /\ k e. Z ) -> ( ( M ... k ) = ( M ... n ) <-> ( M = M /\ k = n ) ) )
208	203 207	bitrd	|- ( ( ph /\ k e. Z ) -> ( dom ( G ` k ) = ( M ... n ) <-> ( M = M /\ k = n ) ) )
209		simpr	|- ( ( M = M /\ k = n ) -> k = n )
210	208 209	biimtrdi	|- ( ( ph /\ k e. Z ) -> ( dom ( G ` k ) = ( M ... n ) -> k = n ) )
211	32 210	syl5	|- ( ( ph /\ k e. Z ) -> ( ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps ) -> k = n ) )
212		oveq2	|- ( n = k -> ( M ... n ) = ( M ... k ) )
213	212	feq2d	|- ( n = k -> ( ( G ` k ) : ( M ... n ) --> A <-> ( G ` k ) : ( M ... k ) --> A ) )
214	4	sbcbidv	|- ( n = k -> ( [. ( G ` k ) / g ]. ps <-> [. ( G ` k ) / g ]. th ) )
215	213 214	anbi12d	|- ( n = k -> ( ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps ) <-> ( ( G ` k ) : ( M ... k ) --> A /\ [. ( G ` k ) / g ]. th ) ) )
216	215	equcoms	|- ( k = n -> ( ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps ) <-> ( ( G ` k ) : ( M ... k ) --> A /\ [. ( G ` k ) / g ]. th ) ) )
217	216	biimpcd	|- ( ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps ) -> ( k = n -> ( ( G ` k ) : ( M ... k ) --> A /\ [. ( G ` k ) / g ]. th ) ) )
218	211 217	sylcom	|- ( ( ph /\ k e. Z ) -> ( ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps ) -> ( ( G ` k ) : ( M ... k ) --> A /\ [. ( G ` k ) / g ]. th ) ) )
219	218	rexlimdvw	|- ( ( ph /\ k e. Z ) -> ( E. n e. Z ( ( G ` k ) : ( M ... n ) --> A /\ [. ( G ` k ) / g ]. ps ) -> ( ( G ` k ) : ( M ... k ) --> A /\ [. ( G ` k ) / g ]. th ) ) )
220	30 219	mpd	|- ( ( ph /\ k e. Z ) -> ( ( G ` k ) : ( M ... k ) --> A /\ [. ( G ` k ) / g ]. th ) )
221	220	simpld	|- ( ( ph /\ k e. Z ) -> ( G ` k ) : ( M ... k ) --> A )
222		eluzfz2	|- ( k e. ( ZZ>= ` M ) -> k e. ( M ... k ) )
223	205 222	syl	|- ( ( ph /\ k e. Z ) -> k e. ( M ... k ) )
224	221 223	ffvelcdmd	|- ( ( ph /\ k e. Z ) -> ( ( G ` k ) ` k ) e. A )
225	55	cbvmptv	|- ( m e. Z |-> ( ( G ` m ) ` m ) ) = ( k e. Z |-> ( ( G ` k ) ` k ) )
226	12 224 225	fmptdf	|- ( ph -> ( m e. Z |-> ( ( G ` m ) ` m ) ) : Z --> A )
227	220	simprd	|- ( ( ph /\ k e. Z ) -> [. ( G ` k ) / g ]. th )
228	197 227	sbceq1dd	|- ( ( ph /\ k e. Z ) -> [. ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) / g ]. th )
229	228	ex	|- ( ph -> ( k e. Z -> [. ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) / g ]. th ) )
230	12 229	ralrimi	|- ( ph -> A. k e. Z [. ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) / g ]. th )
231		mpteq1	|- ( ( M ... n ) = ( M ... k ) -> ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) = ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) )
232		dfsbcq	|- ( ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) = ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) -> ( [. ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) / g ]. ps <-> [. ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) / g ]. ps ) )
233	212 231 232	3syl	|- ( n = k -> ( [. ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) / g ]. ps <-> [. ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) / g ]. ps ) )
234	4	sbcbidv	|- ( n = k -> ( [. ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) / g ]. ps <-> [. ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) / g ]. th ) )
235	233 234	bitrd	|- ( n = k -> ( [. ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) / g ]. ps <-> [. ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) / g ]. th ) )
236	235	cbvralvw	|- ( A. n e. Z [. ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) / g ]. ps <-> A. k e. Z [. ( m e. ( M ... k ) |-> ( ( G ` m ) ` m ) ) / g ]. th )
237	230 236	sylibr	|- ( ph -> A. n e. Z [. ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) / g ]. ps )
238	80	mptex	|- ( m e. Z |-> ( ( G ` m ) ` m ) ) e. _V
239		feq1	|- ( f = ( m e. Z |-> ( ( G ` m ) ` m ) ) -> ( f : Z --> A <-> ( m e. Z |-> ( ( G ` m ) ` m ) ) : Z --> A ) )
240		vex	|- f e. _V
241	240	resex	|- ( f |` ( M ... n ) ) e. _V
242	241 2	sbcie	|- ( [. ( f |` ( M ... n ) ) / g ]. ps <-> ch )
243		reseq1	|- ( f = ( m e. Z |-> ( ( G ` m ) ` m ) ) -> ( f |` ( M ... n ) ) = ( ( m e. Z |-> ( ( G ` m ) ` m ) ) |` ( M ... n ) ) )
244		fzssuz	|- ( M ... n ) C_ ( ZZ>= ` M )
245	244 1	sseqtrri	|- ( M ... n ) C_ Z
246		resmpt	|- ( ( M ... n ) C_ Z -> ( ( m e. Z |-> ( ( G ` m ) ` m ) ) |` ( M ... n ) ) = ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) )
247	245 246	ax-mp	|- ( ( m e. Z |-> ( ( G ` m ) ` m ) ) |` ( M ... n ) ) = ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) )
248	243 247	eqtrdi	|- ( f = ( m e. Z |-> ( ( G ` m ) ` m ) ) -> ( f |` ( M ... n ) ) = ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) )
249	248	sbceq1d	|- ( f = ( m e. Z |-> ( ( G ` m ) ` m ) ) -> ( [. ( f |` ( M ... n ) ) / g ]. ps <-> [. ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) / g ]. ps ) )
250	242 249	bitr3id	|- ( f = ( m e. Z |-> ( ( G ` m ) ` m ) ) -> ( ch <-> [. ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) / g ]. ps ) )
251	250	ralbidv	|- ( f = ( m e. Z |-> ( ( G ` m ) ` m ) ) -> ( A. n e. Z ch <-> A. n e. Z [. ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) / g ]. ps ) )
252	239 251	anbi12d	|- ( f = ( m e. Z |-> ( ( G ` m ) ` m ) ) -> ( ( f : Z --> A /\ A. n e. Z ch ) <-> ( ( m e. Z |-> ( ( G ` m ) ` m ) ) : Z --> A /\ A. n e. Z [. ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) / g ]. ps ) ) )
253	238 252	spcev	|- ( ( ( m e. Z |-> ( ( G ` m ) ` m ) ) : Z --> A /\ A. n e. Z [. ( m e. ( M ... n ) |-> ( ( G ` m ) ` m ) ) / g ]. ps ) -> E. f ( f : Z --> A /\ A. n e. Z ch ) )
254	226 237 253	syl2anc	|- ( ph -> E. f ( f : Z --> A /\ A. n e. Z ch ) )