Theorem poimirlem16

Description: Lemma for poimir establishing the vertices of the simplex of poimirlem17 . (Contributed by Brendan Leahy, 21-Aug-2020)

	Ref	Expression
Hypotheses	poimir.0	|- ( ph -> N e. NN )
	poimirlem22.s	|- S = { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) }
	poimirlem22.1	|- ( ph -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
	poimirlem22.2	|- ( ph -> T e. S )
	poimirlem18.3	|- ( ( ph /\ n e. ( 1 ... N ) ) -> E. p e. ran F ( p ` n ) =/= K )
	poimirlem18.4	|- ( ph -> ( 2nd ` T ) = 0 )
Assertion	poimirlem16	|- ( ph -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		poimir.0	|- ( ph -> N e. NN )
2		poimirlem22.s	|- S = { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) }
3		poimirlem22.1	|- ( ph -> F : ( 0 ... ( N - 1 ) ) --> ( ( 0 ... K ) ^m ( 1 ... N ) ) )
4		poimirlem22.2	|- ( ph -> T e. S )
5		poimirlem18.3	|- ( ( ph /\ n e. ( 1 ... N ) ) -> E. p e. ran F ( p ` n ) =/= K )
6		poimirlem18.4	|- ( ph -> ( 2nd ` T ) = 0 )
7		fveq2	|- ( t = T -> ( 2nd ` t ) = ( 2nd ` T ) )
8	7	breq2d	|- ( t = T -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` T ) ) )
9	8	ifbid	|- ( t = T -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) )
10		2fveq3	|- ( t = T -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) )
11		2fveq3	|- ( t = T -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` T ) ) )
12	11	imaeq1d	|- ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) )
13	12	xpeq1d	|- ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) )
14	11	imaeq1d	|- ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) )
15	14	xpeq1d	|- ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
16	13 15	uneq12d	|- ( t = T -> ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
17	10 16	oveq12d	|- ( t = T -> ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
18	9 17	csbeq12dv	|- ( t = T -> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
19	18	mpteq2dv	|- ( t = T -> ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
20	19	eqeq2d	|- ( t = T -> ( F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) <-> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
21	20 2	elrab2	|- ( T e. S <-> ( T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) /\ F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
22	21	simprbi	|- ( T e. S -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
23	4 22	syl	|- ( ph -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
24		elrabi	|- ( T e. { t e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) | F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) } -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
25	24 2	eleq2s	|- ( T e. S -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
26	4 25	syl	|- ( ph -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
27		xp1st	|- ( T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
28	26 27	syl	|- ( ph -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
29		xp1st	|- ( ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
30	28 29	syl	|- ( ph -> ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
31		elmapfn	|- ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
32	30 31	syl	|- ( ph -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
33	32	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
34		1ex	|- 1 e. _V
35		fnconstg	|- ( 1 e. _V -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) )
36	34 35	ax-mp	|- ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) )
37		c0ex	|- 0 e. _V
38		fnconstg	|- ( 0 e. _V -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
39	37 38	ax-mp	|- ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) )
40	36 39	pm3.2i	|- ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
41		xp2nd	|- ( ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
42	28 41	syl	|- ( ph -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
43		fvex	|- ( 2nd ` ( 1st ` T ) ) e. _V
44		f1oeq1	|- ( f = ( 2nd ` ( 1st ` T ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
45	43 44	elab	|- ( ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
46	42 45	sylib	|- ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
47		dff1o3	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( 2nd ` ( 1st ` T ) ) ) )
48	47	simprbi	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' ( 2nd ` ( 1st ` T ) ) )
49	46 48	syl	|- ( ph -> Fun `' ( 2nd ` ( 1st ` T ) ) )
50		imain	|- ( Fun `' ( 2nd ` ( 1st ` T ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
51	49 50	syl	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
52		elfznn0	|- ( y e. ( 0 ... ( N - 1 ) ) -> y e. NN0 )
53		nn0p1nn	|- ( y e. NN0 -> ( y + 1 ) e. NN )
54	52 53	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. NN )
55	54	nnred	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. RR )
56	55	ltp1d	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) < ( ( y + 1 ) + 1 ) )
57		fzdisj	|- ( ( y + 1 ) < ( ( y + 1 ) + 1 ) -> ( ( 1 ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) = (/) )
58	56 57	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( 1 ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) = (/) )
59	58	imaeq2d	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " (/) ) )
60		ima0	|- ( ( 2nd ` ( 1st ` T ) ) " (/) ) = (/)
61	59 60	eqtrdi	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) )
62	51 61	sylan9req	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) )
63		fnun	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
64	40 62 63	sylancr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
65		imaundi	|- ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
66		nnuz	|- NN = ( ZZ>= ` 1 )
67	54 66	eleqtrdi	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. ( ZZ>= ` 1 ) )
68		peano2uz	|- ( ( y + 1 ) e. ( ZZ>= ` 1 ) -> ( ( y + 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
69	67 68	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
70	1	nncnd	|- ( ph -> N e. CC )
71		npcan1	|- ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
72	70 71	syl	|- ( ph -> ( ( N - 1 ) + 1 ) = N )
73	72	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) = N )
74		elfzuz3	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` y ) )
75		eluzp1p1	|- ( ( N - 1 ) e. ( ZZ>= ` y ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
76	74 75	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
77	76	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
78	73 77	eqeltrrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ZZ>= ` ( y + 1 ) ) )
79		fzsplit2	|- ( ( ( ( y + 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` ( y + 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) )
80	69 78 79	syl2an2	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) )
81	80	imaeq2d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
82		f1ofo	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
83		foima	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
84	46 82 83	3syl	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
85	84	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
86	81 85	eqtr3d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( 1 ... N ) )
87	65 86	eqtr3id	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( 1 ... N ) )
88	87	fneq2d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) <-> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) ) )
89	64 88	mpbid	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
90		ovexd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ... N ) e. _V )
91		inidm	|- ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
92		eqidd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) = ( ( 1st ` ( 1st ` T ) ) ` n ) )
93		eqidd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
94	33 89 90 90 91 92 93	offval	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) = ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) ) )
95		oveq1	|- ( 1 = if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) -> ( 1 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) = ( if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) )
96	95	eqeq2d	|- ( 1 = if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( 1 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) <-> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) ) )
97		oveq1	|- ( 0 = if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) -> ( 0 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) = ( if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) )
98	97	eqeq2d	|- ( 0 = if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( 0 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) <-> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) ) )
99		1p0e1	|- ( 1 + 0 ) = 1
100	99	eqcomi	|- 1 = ( 1 + 0 )
101		f1ofn	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
102	46 101	syl	|- ( ph -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
103	102	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
104		fzss2	|- ( N e. ( ZZ>= ` ( y + 1 ) ) -> ( 1 ... ( y + 1 ) ) C_ ( 1 ... N ) )
105	78 104	syl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ... ( y + 1 ) ) C_ ( 1 ... N ) )
106		eluzfz1	|- ( ( y + 1 ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( y + 1 ) ) )
107	67 106	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> 1 e. ( 1 ... ( y + 1 ) ) )
108	107	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> 1 e. ( 1 ... ( y + 1 ) ) )
109		fnfvima	|- ( ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) /\ ( 1 ... ( y + 1 ) ) C_ ( 1 ... N ) /\ 1 e. ( 1 ... ( y + 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) )
110	103 105 108 109	syl3anc	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) )
111		fvun1	|- ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) /\ ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) /\ ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
112	36 39 111	mp3an12	|- ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) /\ ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
113	62 110 112	syl2anc	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
114	34	fvconst2	|- ( ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = 1 )
115	110 114	syl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = 1 )
116	113 115	eqtrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = 1 )
117		simpr	|- ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> n e. ( 1 ... ( N - 1 ) ) )
118	1	nnzd	|- ( ph -> N e. ZZ )
119		peano2zm	|- ( N e. ZZ -> ( N - 1 ) e. ZZ )
120	118 119	syl	|- ( ph -> ( N - 1 ) e. ZZ )
121		1z	|- 1 e. ZZ
122	120 121	jctil	|- ( ph -> ( 1 e. ZZ /\ ( N - 1 ) e. ZZ ) )
123		elfzelz	|- ( n e. ( 1 ... ( N - 1 ) ) -> n e. ZZ )
124	123 121	jctir	|- ( n e. ( 1 ... ( N - 1 ) ) -> ( n e. ZZ /\ 1 e. ZZ ) )
125		fzaddel	|- ( ( ( 1 e. ZZ /\ ( N - 1 ) e. ZZ ) /\ ( n e. ZZ /\ 1 e. ZZ ) ) -> ( n e. ( 1 ... ( N - 1 ) ) <-> ( n + 1 ) e. ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
126	122 124 125	syl2an	|- ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> ( n e. ( 1 ... ( N - 1 ) ) <-> ( n + 1 ) e. ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
127	117 126	mpbid	|- ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> ( n + 1 ) e. ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) )
128	72	oveq2d	|- ( ph -> ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) = ( ( 1 + 1 ) ... N ) )
129	128	adantr	|- ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) = ( ( 1 + 1 ) ... N ) )
130	127 129	eleqtrd	|- ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> ( n + 1 ) e. ( ( 1 + 1 ) ... N ) )
131	130	ralrimiva	|- ( ph -> A. n e. ( 1 ... ( N - 1 ) ) ( n + 1 ) e. ( ( 1 + 1 ) ... N ) )
132		simpr	|- ( ( ph /\ y e. ( ( 1 + 1 ) ... N ) ) -> y e. ( ( 1 + 1 ) ... N ) )
133		peano2z	|- ( 1 e. ZZ -> ( 1 + 1 ) e. ZZ )
134	121 133	ax-mp	|- ( 1 + 1 ) e. ZZ
135	118 134	jctil	|- ( ph -> ( ( 1 + 1 ) e. ZZ /\ N e. ZZ ) )
136		elfzelz	|- ( y e. ( ( 1 + 1 ) ... N ) -> y e. ZZ )
137	136 121	jctir	|- ( y e. ( ( 1 + 1 ) ... N ) -> ( y e. ZZ /\ 1 e. ZZ ) )
138		fzsubel	|- ( ( ( ( 1 + 1 ) e. ZZ /\ N e. ZZ ) /\ ( y e. ZZ /\ 1 e. ZZ ) ) -> ( y e. ( ( 1 + 1 ) ... N ) <-> ( y - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) ) )
139	135 137 138	syl2an	|- ( ( ph /\ y e. ( ( 1 + 1 ) ... N ) ) -> ( y e. ( ( 1 + 1 ) ... N ) <-> ( y - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) ) )
140	132 139	mpbid	|- ( ( ph /\ y e. ( ( 1 + 1 ) ... N ) ) -> ( y - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) )
141		ax-1cn	|- 1 e. CC
142	141 141	pncan3oi	|- ( ( 1 + 1 ) - 1 ) = 1
143	142	oveq1i	|- ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) = ( 1 ... ( N - 1 ) )
144	140 143	eleqtrdi	|- ( ( ph /\ y e. ( ( 1 + 1 ) ... N ) ) -> ( y - 1 ) e. ( 1 ... ( N - 1 ) ) )
145	136	zcnd	|- ( y e. ( ( 1 + 1 ) ... N ) -> y e. CC )
146		elfznn	|- ( n e. ( 1 ... ( N - 1 ) ) -> n e. NN )
147	146	nncnd	|- ( n e. ( 1 ... ( N - 1 ) ) -> n e. CC )
148		subadd2	|- ( ( y e. CC /\ 1 e. CC /\ n e. CC ) -> ( ( y - 1 ) = n <-> ( n + 1 ) = y ) )
149	141 148	mp3an2	|- ( ( y e. CC /\ n e. CC ) -> ( ( y - 1 ) = n <-> ( n + 1 ) = y ) )
150	149	bicomd	|- ( ( y e. CC /\ n e. CC ) -> ( ( n + 1 ) = y <-> ( y - 1 ) = n ) )
151		eqcom	|- ( ( n + 1 ) = y <-> y = ( n + 1 ) )
152		eqcom	|- ( ( y - 1 ) = n <-> n = ( y - 1 ) )
153	150 151 152	3bitr3g	|- ( ( y e. CC /\ n e. CC ) -> ( y = ( n + 1 ) <-> n = ( y - 1 ) ) )
154	145 147 153	syl2an	|- ( ( y e. ( ( 1 + 1 ) ... N ) /\ n e. ( 1 ... ( N - 1 ) ) ) -> ( y = ( n + 1 ) <-> n = ( y - 1 ) ) )
155	154	ralrimiva	|- ( y e. ( ( 1 + 1 ) ... N ) -> A. n e. ( 1 ... ( N - 1 ) ) ( y = ( n + 1 ) <-> n = ( y - 1 ) ) )
156	155	adantl	|- ( ( ph /\ y e. ( ( 1 + 1 ) ... N ) ) -> A. n e. ( 1 ... ( N - 1 ) ) ( y = ( n + 1 ) <-> n = ( y - 1 ) ) )
157		reu6i	|- ( ( ( y - 1 ) e. ( 1 ... ( N - 1 ) ) /\ A. n e. ( 1 ... ( N - 1 ) ) ( y = ( n + 1 ) <-> n = ( y - 1 ) ) ) -> E! n e. ( 1 ... ( N - 1 ) ) y = ( n + 1 ) )
158	144 156 157	syl2anc	|- ( ( ph /\ y e. ( ( 1 + 1 ) ... N ) ) -> E! n e. ( 1 ... ( N - 1 ) ) y = ( n + 1 ) )
159	158	ralrimiva	|- ( ph -> A. y e. ( ( 1 + 1 ) ... N ) E! n e. ( 1 ... ( N - 1 ) ) y = ( n + 1 ) )
160		eqid	|- ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) = ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) )
161	160	f1ompt	|- ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) : ( 1 ... ( N - 1 ) ) -1-1-onto-> ( ( 1 + 1 ) ... N ) <-> ( A. n e. ( 1 ... ( N - 1 ) ) ( n + 1 ) e. ( ( 1 + 1 ) ... N ) /\ A. y e. ( ( 1 + 1 ) ... N ) E! n e. ( 1 ... ( N - 1 ) ) y = ( n + 1 ) ) )
162	131 159 161	sylanbrc	|- ( ph -> ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) : ( 1 ... ( N - 1 ) ) -1-1-onto-> ( ( 1 + 1 ) ... N ) )
163		f1osng	|- ( ( N e. NN /\ 1 e. _V ) -> { <. N , 1 >. } : { N } -1-1-onto-> { 1 } )
164	1 34 163	sylancl	|- ( ph -> { <. N , 1 >. } : { N } -1-1-onto-> { 1 } )
165	1	nnred	|- ( ph -> N e. RR )
166	165	ltm1d	|- ( ph -> ( N - 1 ) < N )
167	120	zred	|- ( ph -> ( N - 1 ) e. RR )
168	167 165	ltnled	|- ( ph -> ( ( N - 1 ) < N <-> -. N <_ ( N - 1 ) ) )
169	166 168	mpbid	|- ( ph -> -. N <_ ( N - 1 ) )
170		elfzle2	|- ( N e. ( 1 ... ( N - 1 ) ) -> N <_ ( N - 1 ) )
171	169 170	nsyl	|- ( ph -> -. N e. ( 1 ... ( N - 1 ) ) )
172		disjsn	|- ( ( ( 1 ... ( N - 1 ) ) i^i { N } ) = (/) <-> -. N e. ( 1 ... ( N - 1 ) ) )
173	171 172	sylibr	|- ( ph -> ( ( 1 ... ( N - 1 ) ) i^i { N } ) = (/) )
174		1re	|- 1 e. RR
175	174	ltp1i	|- 1 < ( 1 + 1 )
176	174 174	readdcli	|- ( 1 + 1 ) e. RR
177	174 176	ltnlei	|- ( 1 < ( 1 + 1 ) <-> -. ( 1 + 1 ) <_ 1 )
178	175 177	mpbi	|- -. ( 1 + 1 ) <_ 1
179		elfzle1	|- ( 1 e. ( ( 1 + 1 ) ... N ) -> ( 1 + 1 ) <_ 1 )
180	178 179	mto	|- -. 1 e. ( ( 1 + 1 ) ... N )
181		disjsn	|- ( ( ( ( 1 + 1 ) ... N ) i^i { 1 } ) = (/) <-> -. 1 e. ( ( 1 + 1 ) ... N ) )
182	180 181	mpbir	|- ( ( ( 1 + 1 ) ... N ) i^i { 1 } ) = (/)
183		f1oun	|- ( ( ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) : ( 1 ... ( N - 1 ) ) -1-1-onto-> ( ( 1 + 1 ) ... N ) /\ { <. N , 1 >. } : { N } -1-1-onto-> { 1 } ) /\ ( ( ( 1 ... ( N - 1 ) ) i^i { N } ) = (/) /\ ( ( ( 1 + 1 ) ... N ) i^i { 1 } ) = (/) ) ) -> ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) u. { <. N , 1 >. } ) : ( ( 1 ... ( N - 1 ) ) u. { N } ) -1-1-onto-> ( ( ( 1 + 1 ) ... N ) u. { 1 } ) )
184	182 183	mpanr2	|- ( ( ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) : ( 1 ... ( N - 1 ) ) -1-1-onto-> ( ( 1 + 1 ) ... N ) /\ { <. N , 1 >. } : { N } -1-1-onto-> { 1 } ) /\ ( ( 1 ... ( N - 1 ) ) i^i { N } ) = (/) ) -> ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) u. { <. N , 1 >. } ) : ( ( 1 ... ( N - 1 ) ) u. { N } ) -1-1-onto-> ( ( ( 1 + 1 ) ... N ) u. { 1 } ) )
185	162 164 173 184	syl21anc	|- ( ph -> ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) u. { <. N , 1 >. } ) : ( ( 1 ... ( N - 1 ) ) u. { N } ) -1-1-onto-> ( ( ( 1 + 1 ) ... N ) u. { 1 } ) )
186	34	a1i	|- ( ph -> 1 e. _V )
187	1 66	eleqtrdi	|- ( ph -> N e. ( ZZ>= ` 1 ) )
188	72 187	eqeltrd	|- ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
189		uzid	|- ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
190		peano2uz	|- ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
191	120 189 190	3syl	|- ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
192	72 191	eqeltrrd	|- ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
193		fzsplit2	|- ( ( ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` ( N - 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
194	188 192 193	syl2anc	|- ( ph -> ( 1 ... N ) = ( ( 1 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
195	72	oveq1d	|- ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = ( N ... N ) )
196		fzsn	|- ( N e. ZZ -> ( N ... N ) = { N } )
197	118 196	syl	|- ( ph -> ( N ... N ) = { N } )
198	195 197	eqtrd	|- ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = { N } )
199	198	uneq2d	|- ( ph -> ( ( 1 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) = ( ( 1 ... ( N - 1 ) ) u. { N } ) )
200	194 199	eqtr2d	|- ( ph -> ( ( 1 ... ( N - 1 ) ) u. { N } ) = ( 1 ... N ) )
201		iftrue	|- ( n = N -> if ( n = N , 1 , ( n + 1 ) ) = 1 )
202	201	adantl	|- ( ( ph /\ n = N ) -> if ( n = N , 1 , ( n + 1 ) ) = 1 )
203	1 186 200 202	fmptapd	|- ( ph -> ( ( n e. ( 1 ... ( N - 1 ) ) |-> if ( n = N , 1 , ( n + 1 ) ) ) u. { <. N , 1 >. } ) = ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) )
204		eleq1	|- ( n = N -> ( n e. ( 1 ... ( N - 1 ) ) <-> N e. ( 1 ... ( N - 1 ) ) ) )
205	204	notbid	|- ( n = N -> ( -. n e. ( 1 ... ( N - 1 ) ) <-> -. N e. ( 1 ... ( N - 1 ) ) ) )
206	171 205	syl5ibrcom	|- ( ph -> ( n = N -> -. n e. ( 1 ... ( N - 1 ) ) ) )
207	206	necon2ad	|- ( ph -> ( n e. ( 1 ... ( N - 1 ) ) -> n =/= N ) )
208	207	imp	|- ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> n =/= N )
209		ifnefalse	|- ( n =/= N -> if ( n = N , 1 , ( n + 1 ) ) = ( n + 1 ) )
210	208 209	syl	|- ( ( ph /\ n e. ( 1 ... ( N - 1 ) ) ) -> if ( n = N , 1 , ( n + 1 ) ) = ( n + 1 ) )
211	210	mpteq2dva	|- ( ph -> ( n e. ( 1 ... ( N - 1 ) ) |-> if ( n = N , 1 , ( n + 1 ) ) ) = ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) )
212	211	uneq1d	|- ( ph -> ( ( n e. ( 1 ... ( N - 1 ) ) |-> if ( n = N , 1 , ( n + 1 ) ) ) u. { <. N , 1 >. } ) = ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) u. { <. N , 1 >. } ) )
213	203 212	eqtr3d	|- ( ph -> ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) = ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) u. { <. N , 1 >. } ) )
214	194 199	eqtrd	|- ( ph -> ( 1 ... N ) = ( ( 1 ... ( N - 1 ) ) u. { N } ) )
215		uzid	|- ( 1 e. ZZ -> 1 e. ( ZZ>= ` 1 ) )
216		peano2uz	|- ( 1 e. ( ZZ>= ` 1 ) -> ( 1 + 1 ) e. ( ZZ>= ` 1 ) )
217	121 215 216	mp2b	|- ( 1 + 1 ) e. ( ZZ>= ` 1 )
218		fzsplit2	|- ( ( ( 1 + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` 1 ) ) -> ( 1 ... N ) = ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... N ) ) )
219	217 187 218	sylancr	|- ( ph -> ( 1 ... N ) = ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... N ) ) )
220		fzsn	|- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
221	121 220	ax-mp	|- ( 1 ... 1 ) = { 1 }
222	221	uneq1i	|- ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... N ) ) = ( { 1 } u. ( ( 1 + 1 ) ... N ) )
223	222	equncomi	|- ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... N ) ) = ( ( ( 1 + 1 ) ... N ) u. { 1 } )
224	219 223	eqtrdi	|- ( ph -> ( 1 ... N ) = ( ( ( 1 + 1 ) ... N ) u. { 1 } ) )
225	213 214 224	f1oeq123d	|- ( ph -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( n e. ( 1 ... ( N - 1 ) ) |-> ( n + 1 ) ) u. { <. N , 1 >. } ) : ( ( 1 ... ( N - 1 ) ) u. { N } ) -1-1-onto-> ( ( ( 1 + 1 ) ... N ) u. { 1 } ) ) )
226	185 225	mpbird	|- ( ph -> ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
227		f1oco	|- ( ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
228	46 226 227	syl2anc	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
229		dff1o3	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) ) )
230	229	simprbi	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) )
231	228 230	syl	|- ( ph -> Fun `' ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) )
232		imain	|- ( Fun `' ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( 1 ... y ) i^i ( ( y + 1 ) ... N ) ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) i^i ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) ) )
233	231 232	syl	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( 1 ... y ) i^i ( ( y + 1 ) ... N ) ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) i^i ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) ) )
234	52	nn0red	|- ( y e. ( 0 ... ( N - 1 ) ) -> y e. RR )
235	234	ltp1d	|- ( y e. ( 0 ... ( N - 1 ) ) -> y < ( y + 1 ) )
236		fzdisj	|- ( y < ( y + 1 ) -> ( ( 1 ... y ) i^i ( ( y + 1 ) ... N ) ) = (/) )
237	235 236	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( 1 ... y ) i^i ( ( y + 1 ) ... N ) ) = (/) )
238	237	imaeq2d	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( 1 ... y ) i^i ( ( y + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " (/) ) )
239		ima0	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " (/) ) = (/)
240	238 239	eqtrdi	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( 1 ... y ) i^i ( ( y + 1 ) ... N ) ) ) = (/) )
241	233 240	sylan9req	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) i^i ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) ) = (/) )
242		imassrn	|- ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... N ) ) C_ ran ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) )
243		f1of	|- ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) : ( 1 ... N ) --> ( 1 ... N ) )
244		frn	|- ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) : ( 1 ... N ) --> ( 1 ... N ) -> ran ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) C_ ( 1 ... N ) )
245	226 243 244	3syl	|- ( ph -> ran ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) C_ ( 1 ... N ) )
246	242 245	sstrid	|- ( ph -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... N ) ) C_ ( 1 ... N ) )
247	246	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... N ) ) C_ ( 1 ... N ) )
248		elfz1end	|- ( N e. NN <-> N e. ( 1 ... N ) )
249	1 248	sylib	|- ( ph -> N e. ( 1 ... N ) )
250		eqid	|- ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) = ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) )
251	201 250 34	fvmpt	|- ( N e. ( 1 ... N ) -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ` N ) = 1 )
252	249 251	syl	|- ( ph -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ` N ) = 1 )
253	252	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ` N ) = 1 )
254		f1ofn	|- ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) Fn ( 1 ... N ) )
255	226 254	syl	|- ( ph -> ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) Fn ( 1 ... N ) )
256	255	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) Fn ( 1 ... N ) )
257		fzss1	|- ( ( y + 1 ) e. ( ZZ>= ` 1 ) -> ( ( y + 1 ) ... N ) C_ ( 1 ... N ) )
258	67 257	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) ... N ) C_ ( 1 ... N ) )
259	258	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( y + 1 ) ... N ) C_ ( 1 ... N ) )
260		eluzfz2	|- ( N e. ( ZZ>= ` ( y + 1 ) ) -> N e. ( ( y + 1 ) ... N ) )
261	78 260	syl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ( y + 1 ) ... N ) )
262		fnfvima	|- ( ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) Fn ( 1 ... N ) /\ ( ( y + 1 ) ... N ) C_ ( 1 ... N ) /\ N e. ( ( y + 1 ) ... N ) ) -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ` N ) e. ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... N ) ) )
263	256 259 261 262	syl3anc	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ` N ) e. ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... N ) ) )
264	253 263	eqeltrrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> 1 e. ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... N ) ) )
265		fnfvima	|- ( ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) /\ ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... N ) ) C_ ( 1 ... N ) /\ 1 e. ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... N ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... N ) ) ) )
266	103 247 264 265	syl3anc	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... N ) ) ) )
267		imaco	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... N ) ) )
268	266 267	eleqtrrdi	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) )
269		fnconstg	|- ( 1 e. _V -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) Fn ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) )
270	34 269	ax-mp	|- ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) Fn ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) )
271		fnconstg	|- ( 0 e. _V -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) Fn ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) )
272	37 271	ax-mp	|- ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) Fn ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) )
273		fvun2	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) Fn ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) /\ ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) Fn ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) /\ ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) i^i ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) ) = (/) /\ ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
274	270 272 273	mp3an12	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) i^i ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) ) = (/) /\ ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
275	241 268 274	syl2anc	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
276	37	fvconst2	|- ( ( ( 2nd ` ( 1st ` T ) ) ` 1 ) e. ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = 0 )
277	268 276	syl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = 0 )
278	275 277	eqtrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = 0 )
279	278	oveq2d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) ) = ( 1 + 0 ) )
280	100 116 279	3eqtr4a	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( 1 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) ) )
281		fveq2	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
282		fveq2	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
283	282	oveq2d	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) -> ( 1 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) = ( 1 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) ) )
284	281 283	eqeq12d	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( 1 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) <-> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) = ( 1 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) ) ) )
285	280 284	syl5ibrcom	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( 1 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) ) )
286	285	imp	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( 1 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) )
287	286	adantlr	|- ( ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) /\ n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( 1 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) )
288		eldifsn	|- ( n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) <-> ( n e. ( 1 ... N ) /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
289		df-ne	|- ( n =/= ( ( 2nd ` ( 1st ` T ) ) ` 1 ) <-> -. n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) )
290	289	anbi2i	|- ( ( n e. ( 1 ... N ) /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) <-> ( n e. ( 1 ... N ) /\ -. n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
291	288 290	bitri	|- ( n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) <-> ( n e. ( 1 ... N ) /\ -. n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) )
292		fnconstg	|- ( 1 e. _V -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
293	34 292	ax-mp	|- ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) )
294	293 39	pm3.2i	|- ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
295		imain	|- ( Fun `' ( 2nd ` ( 1st ` T ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( ( 1 + 1 ) ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
296	49 295	syl	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( ( 1 + 1 ) ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
297		fzdisj	|- ( ( y + 1 ) < ( ( y + 1 ) + 1 ) -> ( ( ( 1 + 1 ) ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) = (/) )
298	56 297	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( ( 1 + 1 ) ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) = (/) )
299	298	imaeq2d	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( ( 1 + 1 ) ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " (/) ) )
300	299 60	eqtrdi	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( ( 1 + 1 ) ... ( y + 1 ) ) i^i ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) )
301	296 300	sylan9req	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) )
302		fnun	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = (/) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
303	294 301 302	sylancr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
304		imaundi	|- ( ( 2nd ` ( 1st ` T ) ) " ( ( ( 1 + 1 ) ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
305		fzpred	|- ( N e. ( ZZ>= ` 1 ) -> ( 1 ... N ) = ( { 1 } u. ( ( 1 + 1 ) ... N ) ) )
306	187 305	syl	|- ( ph -> ( 1 ... N ) = ( { 1 } u. ( ( 1 + 1 ) ... N ) ) )
307		uncom	|- ( { 1 } u. ( ( 1 + 1 ) ... N ) ) = ( ( ( 1 + 1 ) ... N ) u. { 1 } )
308	306 307	eqtrdi	|- ( ph -> ( 1 ... N ) = ( ( ( 1 + 1 ) ... N ) u. { 1 } ) )
309	308	difeq1d	|- ( ph -> ( ( 1 ... N ) \ { 1 } ) = ( ( ( ( 1 + 1 ) ... N ) u. { 1 } ) \ { 1 } ) )
310		difun2	|- ( ( ( ( 1 + 1 ) ... N ) u. { 1 } ) \ { 1 } ) = ( ( ( 1 + 1 ) ... N ) \ { 1 } )
311		disj3	|- ( ( ( ( 1 + 1 ) ... N ) i^i { 1 } ) = (/) <-> ( ( 1 + 1 ) ... N ) = ( ( ( 1 + 1 ) ... N ) \ { 1 } ) )
312	182 311	mpbi	|- ( ( 1 + 1 ) ... N ) = ( ( ( 1 + 1 ) ... N ) \ { 1 } )
313	310 312	eqtr4i	|- ( ( ( ( 1 + 1 ) ... N ) u. { 1 } ) \ { 1 } ) = ( ( 1 + 1 ) ... N )
314	309 313	eqtrdi	|- ( ph -> ( ( 1 ... N ) \ { 1 } ) = ( ( 1 + 1 ) ... N ) )
315	314	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 1 ... N ) \ { 1 } ) = ( ( 1 + 1 ) ... N ) )
316		eluzp1p1	|- ( ( y + 1 ) e. ( ZZ>= ` 1 ) -> ( ( y + 1 ) + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
317	67 316	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
318		fzsplit2	|- ( ( ( ( y + 1 ) + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) /\ N e. ( ZZ>= ` ( y + 1 ) ) ) -> ( ( 1 + 1 ) ... N ) = ( ( ( 1 + 1 ) ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) )
319	317 78 318	syl2an2	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 1 + 1 ) ... N ) = ( ( ( 1 + 1 ) ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) )
320	315 319	eqtrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 1 ... N ) \ { 1 } ) = ( ( ( 1 + 1 ) ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) )
321	320	imaeq2d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { 1 } ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( ( 1 + 1 ) ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
322		imadif	|- ( Fun `' ( 2nd ` ( 1st ` T ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { 1 } ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` T ) ) " { 1 } ) ) )
323	49 322	syl	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { 1 } ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` T ) ) " { 1 } ) ) )
324		eluzfz1	|- ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
325	187 324	syl	|- ( ph -> 1 e. ( 1 ... N ) )
326		fnsnfv	|- ( ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) /\ 1 e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } = ( ( 2nd ` ( 1st ` T ) ) " { 1 } ) )
327	102 325 326	syl2anc	|- ( ph -> { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } = ( ( 2nd ` ( 1st ` T ) ) " { 1 } ) )
328	327	eqcomd	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " { 1 } ) = { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } )
329	84 328	difeq12d	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` T ) ) " { 1 } ) ) = ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) )
330	323 329	eqtrd	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { 1 } ) ) = ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) )
331	330	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { 1 } ) ) = ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) )
332	321 331	eqtr3d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( ( 1 + 1 ) ... ( y + 1 ) ) u. ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) )
333	304 332	eqtr3id	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) )
334	333	fneq2d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) <-> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) ) )
335	303 334	mpbid	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) )
336		disjdifr	|- ( ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) i^i { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) = (/)
337		fnconstg	|- ( 1 e. _V -> ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) Fn { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } )
338	34 337	ax-mp	|- ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) Fn { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) }
339		fvun1	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) /\ ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) Fn { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } /\ ( ( ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) i^i { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) = (/) /\ n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
340	338 339	mp3an2	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) /\ ( ( ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) i^i { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) = (/) /\ n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
341		fnconstg	|- ( 0 e. _V -> ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) Fn { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } )
342	37 341	ax-mp	|- ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) Fn { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) }
343		fvun1	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) /\ ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) Fn { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } /\ ( ( ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) i^i { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) = (/) /\ n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
344	342 343	mp3an2	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) /\ ( ( ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) i^i { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) = (/) /\ n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
345	340 344	eqtr4d	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) /\ ( ( ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) i^i { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) = (/) /\ n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) ) ` n ) = ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) ) ` n ) )
346	336 345	mpanr1	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) /\ n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) ) ` n ) = ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) ) ` n ) )
347	335 346	sylan	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) ) ` n ) = ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) ) ` n ) )
348	291 347	sylan2br	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( n e. ( 1 ... N ) /\ -. n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) ) ` n ) = ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) ) ` n ) )
349	348	anassrs	|- ( ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) /\ -. n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) ) ` n ) = ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) ) ` n ) )
350		fzpred	|- ( ( y + 1 ) e. ( ZZ>= ` 1 ) -> ( 1 ... ( y + 1 ) ) = ( { 1 } u. ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
351	67 350	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( 1 ... ( y + 1 ) ) = ( { 1 } u. ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
352	351	imaeq2d	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( { 1 } u. ( ( 1 + 1 ) ... ( y + 1 ) ) ) ) )
353	352	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( { 1 } u. ( ( 1 + 1 ) ... ( y + 1 ) ) ) ) )
354	327	uneq1d	|- ( ph -> ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } u. ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " { 1 } ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) ) )
355		uncom	|- ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) u. { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) = ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } u. ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
356		imaundi	|- ( ( 2nd ` ( 1st ` T ) ) " ( { 1 } u. ( ( 1 + 1 ) ... ( y + 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " { 1 } ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
357	354 355 356	3eqtr4g	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) u. { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) = ( ( 2nd ` ( 1st ` T ) ) " ( { 1 } u. ( ( 1 + 1 ) ... ( y + 1 ) ) ) ) )
358	357	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) u. { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) = ( ( 2nd ` ( 1st ` T ) ) " ( { 1 } u. ( ( 1 + 1 ) ... ( y + 1 ) ) ) ) )
359	353 358	eqtr4d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) u. { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) )
360	359	xpeq1d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) u. { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) X. { 1 } ) )
361		xpundir	|- ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) u. { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } ) X. { 1 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) )
362	360 361	eqtrdi	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) ) )
363	362	uneq1d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
364		un23	|- ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) )
365	363 364	eqtrdi	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) ) )
366	365	fveq1d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) ) ` n ) )
367	366	ad2antrr	|- ( ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) /\ -. n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 1 } ) ) ` n ) )
368		imaco	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( 1 ... y ) ) )
369		df-ima	|- ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( 1 ... y ) ) = ran ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) |` ( 1 ... y ) )
370		peano2uz	|- ( ( N - 1 ) e. ( ZZ>= ` y ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` y ) )
371	74 370	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` y ) )
372	371	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` y ) )
373	73 372	eqeltrrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ZZ>= ` y ) )
374		fzss2	|- ( N e. ( ZZ>= ` y ) -> ( 1 ... y ) C_ ( 1 ... N ) )
375	373 374	syl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ... y ) C_ ( 1 ... N ) )
376	375	resmptd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) |` ( 1 ... y ) ) = ( n e. ( 1 ... y ) |-> if ( n = N , 1 , ( n + 1 ) ) ) )
377		fzss2	|- ( ( N - 1 ) e. ( ZZ>= ` y ) -> ( 1 ... y ) C_ ( 1 ... ( N - 1 ) ) )
378	74 377	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( 1 ... y ) C_ ( 1 ... ( N - 1 ) ) )
379	378	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ... y ) C_ ( 1 ... ( N - 1 ) ) )
380	171	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> -. N e. ( 1 ... ( N - 1 ) ) )
381	379 380	ssneldd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> -. N e. ( 1 ... y ) )
382		eleq1	|- ( n = N -> ( n e. ( 1 ... y ) <-> N e. ( 1 ... y ) ) )
383	382	notbid	|- ( n = N -> ( -. n e. ( 1 ... y ) <-> -. N e. ( 1 ... y ) ) )
384	381 383	syl5ibrcom	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( n = N -> -. n e. ( 1 ... y ) ) )
385	384	necon2ad	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( n e. ( 1 ... y ) -> n =/= N ) )
386	385	imp	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... y ) ) -> n =/= N )
387	386 209	syl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... y ) ) -> if ( n = N , 1 , ( n + 1 ) ) = ( n + 1 ) )
388	387	mpteq2dva	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( n e. ( 1 ... y ) |-> if ( n = N , 1 , ( n + 1 ) ) ) = ( n e. ( 1 ... y ) |-> ( n + 1 ) ) )
389	376 388	eqtrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) |` ( 1 ... y ) ) = ( n e. ( 1 ... y ) |-> ( n + 1 ) ) )
390	389	rneqd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ran ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) |` ( 1 ... y ) ) = ran ( n e. ( 1 ... y ) |-> ( n + 1 ) ) )
391	369 390	syl5eq	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( 1 ... y ) ) = ran ( n e. ( 1 ... y ) |-> ( n + 1 ) ) )
392		eqid	|- ( n e. ( 1 ... y ) |-> ( n + 1 ) ) = ( n e. ( 1 ... y ) |-> ( n + 1 ) )
393	392	elrnmpt	|- ( j e. _V -> ( j e. ran ( n e. ( 1 ... y ) |-> ( n + 1 ) ) <-> E. n e. ( 1 ... y ) j = ( n + 1 ) ) )
394	393	elv	|- ( j e. ran ( n e. ( 1 ... y ) |-> ( n + 1 ) ) <-> E. n e. ( 1 ... y ) j = ( n + 1 ) )
395		elfzelz	|- ( y e. ( 0 ... ( N - 1 ) ) -> y e. ZZ )
396	395	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y e. ZZ )
397		simpr	|- ( ( y e. ZZ /\ n e. ( 1 ... y ) ) -> n e. ( 1 ... y ) )
398	121	jctl	|- ( y e. ZZ -> ( 1 e. ZZ /\ y e. ZZ ) )
399		elfzelz	|- ( n e. ( 1 ... y ) -> n e. ZZ )
400	399 121	jctir	|- ( n e. ( 1 ... y ) -> ( n e. ZZ /\ 1 e. ZZ ) )
401		fzaddel	|- ( ( ( 1 e. ZZ /\ y e. ZZ ) /\ ( n e. ZZ /\ 1 e. ZZ ) ) -> ( n e. ( 1 ... y ) <-> ( n + 1 ) e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
402	398 400 401	syl2an	|- ( ( y e. ZZ /\ n e. ( 1 ... y ) ) -> ( n e. ( 1 ... y ) <-> ( n + 1 ) e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
403	397 402	mpbid	|- ( ( y e. ZZ /\ n e. ( 1 ... y ) ) -> ( n + 1 ) e. ( ( 1 + 1 ) ... ( y + 1 ) ) )
404		eleq1	|- ( j = ( n + 1 ) -> ( j e. ( ( 1 + 1 ) ... ( y + 1 ) ) <-> ( n + 1 ) e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
405	403 404	syl5ibrcom	|- ( ( y e. ZZ /\ n e. ( 1 ... y ) ) -> ( j = ( n + 1 ) -> j e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
406	405	rexlimdva	|- ( y e. ZZ -> ( E. n e. ( 1 ... y ) j = ( n + 1 ) -> j e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
407		elfzelz	|- ( j e. ( ( 1 + 1 ) ... ( y + 1 ) ) -> j e. ZZ )
408	407	zcnd	|- ( j e. ( ( 1 + 1 ) ... ( y + 1 ) ) -> j e. CC )
409		npcan1	|- ( j e. CC -> ( ( j - 1 ) + 1 ) = j )
410	408 409	syl	|- ( j e. ( ( 1 + 1 ) ... ( y + 1 ) ) -> ( ( j - 1 ) + 1 ) = j )
411	410	eleq1d	|- ( j e. ( ( 1 + 1 ) ... ( y + 1 ) ) -> ( ( ( j - 1 ) + 1 ) e. ( ( 1 + 1 ) ... ( y + 1 ) ) <-> j e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
412	411	ibir	|- ( j e. ( ( 1 + 1 ) ... ( y + 1 ) ) -> ( ( j - 1 ) + 1 ) e. ( ( 1 + 1 ) ... ( y + 1 ) ) )
413	412	adantl	|- ( ( y e. ZZ /\ j e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) -> ( ( j - 1 ) + 1 ) e. ( ( 1 + 1 ) ... ( y + 1 ) ) )
414		peano2zm	|- ( j e. ZZ -> ( j - 1 ) e. ZZ )
415	407 414	syl	|- ( j e. ( ( 1 + 1 ) ... ( y + 1 ) ) -> ( j - 1 ) e. ZZ )
416	415 121	jctir	|- ( j e. ( ( 1 + 1 ) ... ( y + 1 ) ) -> ( ( j - 1 ) e. ZZ /\ 1 e. ZZ ) )
417		fzaddel	|- ( ( ( 1 e. ZZ /\ y e. ZZ ) /\ ( ( j - 1 ) e. ZZ /\ 1 e. ZZ ) ) -> ( ( j - 1 ) e. ( 1 ... y ) <-> ( ( j - 1 ) + 1 ) e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
418	398 416 417	syl2an	|- ( ( y e. ZZ /\ j e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) -> ( ( j - 1 ) e. ( 1 ... y ) <-> ( ( j - 1 ) + 1 ) e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
419	413 418	mpbird	|- ( ( y e. ZZ /\ j e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) -> ( j - 1 ) e. ( 1 ... y ) )
420	408	adantl	|- ( ( y e. ZZ /\ j e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) -> j e. CC )
421	409	eqcomd	|- ( j e. CC -> j = ( ( j - 1 ) + 1 ) )
422	420 421	syl	|- ( ( y e. ZZ /\ j e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) -> j = ( ( j - 1 ) + 1 ) )
423		oveq1	|- ( n = ( j - 1 ) -> ( n + 1 ) = ( ( j - 1 ) + 1 ) )
424	423	rspceeqv	|- ( ( ( j - 1 ) e. ( 1 ... y ) /\ j = ( ( j - 1 ) + 1 ) ) -> E. n e. ( 1 ... y ) j = ( n + 1 ) )
425	419 422 424	syl2anc	|- ( ( y e. ZZ /\ j e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) -> E. n e. ( 1 ... y ) j = ( n + 1 ) )
426	425	ex	|- ( y e. ZZ -> ( j e. ( ( 1 + 1 ) ... ( y + 1 ) ) -> E. n e. ( 1 ... y ) j = ( n + 1 ) ) )
427	406 426	impbid	|- ( y e. ZZ -> ( E. n e. ( 1 ... y ) j = ( n + 1 ) <-> j e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
428	396 427	syl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( E. n e. ( 1 ... y ) j = ( n + 1 ) <-> j e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
429	394 428	syl5bb	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( j e. ran ( n e. ( 1 ... y ) |-> ( n + 1 ) ) <-> j e. ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
430	429	eqrdv	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ran ( n e. ( 1 ... y ) |-> ( n + 1 ) ) = ( ( 1 + 1 ) ... ( y + 1 ) ) )
431	391 430	eqtrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( 1 ... y ) ) = ( ( 1 + 1 ) ... ( y + 1 ) ) )
432	431	imaeq2d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( 1 ... y ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
433	368 432	syl5eq	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) )
434	433	xpeq1d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) )
435		imaundi	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( { N } u. ( ( y + 1 ) ... ( N - 1 ) ) ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " { N } ) u. ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... ( N - 1 ) ) ) )
436		imaco	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " { N } ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " { N } ) )
437		imaco	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... ( N - 1 ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... ( N - 1 ) ) ) )
438	436 437	uneq12i	|- ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " { N } ) u. ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... ( N - 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " { N } ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... ( N - 1 ) ) ) ) )
439	435 438	eqtri	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( { N } u. ( ( y + 1 ) ... ( N - 1 ) ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " { N } ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... ( N - 1 ) ) ) ) )
440	192	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ZZ>= ` ( N - 1 ) ) )
441		fzsplit2	|- ( ( ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) /\ N e. ( ZZ>= ` ( N - 1 ) ) ) -> ( ( y + 1 ) ... N ) = ( ( ( y + 1 ) ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
442	76 440 441	syl2an2	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( y + 1 ) ... N ) = ( ( ( y + 1 ) ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
443	198	uneq2d	|- ( ph -> ( ( ( y + 1 ) ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) = ( ( ( y + 1 ) ... ( N - 1 ) ) u. { N } ) )
444	443	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( y + 1 ) ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) = ( ( ( y + 1 ) ... ( N - 1 ) ) u. { N } ) )
445	442 444	eqtrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( y + 1 ) ... N ) = ( ( ( y + 1 ) ... ( N - 1 ) ) u. { N } ) )
446		uncom	|- ( ( ( y + 1 ) ... ( N - 1 ) ) u. { N } ) = ( { N } u. ( ( y + 1 ) ... ( N - 1 ) ) )
447	445 446	eqtrdi	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( y + 1 ) ... N ) = ( { N } u. ( ( y + 1 ) ... ( N - 1 ) ) ) )
448	447	imaeq2d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( { N } u. ( ( y + 1 ) ... ( N - 1 ) ) ) ) )
449	252	sneqd	|- ( ph -> { ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ` N ) } = { 1 } )
450		fnsnfv	|- ( ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) Fn ( 1 ... N ) /\ N e. ( 1 ... N ) ) -> { ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ` N ) } = ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " { N } ) )
451	255 249 450	syl2anc	|- ( ph -> { ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ` N ) } = ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " { N } ) )
452	449 451	eqtr3d	|- ( ph -> { 1 } = ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " { N } ) )
453	452	imaeq2d	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " { 1 } ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " { N } ) ) )
454	327 453	eqtrd	|- ( ph -> { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } = ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " { N } ) ) )
455	454	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } = ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " { N } ) ) )
456		df-ima	|- ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... ( N - 1 ) ) ) = ran ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) |` ( ( y + 1 ) ... ( N - 1 ) ) )
457		fzss1	|- ( ( y + 1 ) e. ( ZZ>= ` 1 ) -> ( ( y + 1 ) ... ( N - 1 ) ) C_ ( 1 ... ( N - 1 ) ) )
458	67 457	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) ... ( N - 1 ) ) C_ ( 1 ... ( N - 1 ) ) )
459		fzss2	|- ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
460	192 459	syl	|- ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
461	458 460	sylan9ssr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( y + 1 ) ... ( N - 1 ) ) C_ ( 1 ... N ) )
462	461	resmptd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) |` ( ( y + 1 ) ... ( N - 1 ) ) ) = ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> if ( n = N , 1 , ( n + 1 ) ) ) )
463		elfzle2	|- ( N e. ( ( y + 1 ) ... ( N - 1 ) ) -> N <_ ( N - 1 ) )
464	169 463	nsyl	|- ( ph -> -. N e. ( ( y + 1 ) ... ( N - 1 ) ) )
465		eleq1	|- ( n = N -> ( n e. ( ( y + 1 ) ... ( N - 1 ) ) <-> N e. ( ( y + 1 ) ... ( N - 1 ) ) ) )
466	465	notbid	|- ( n = N -> ( -. n e. ( ( y + 1 ) ... ( N - 1 ) ) <-> -. N e. ( ( y + 1 ) ... ( N - 1 ) ) ) )
467	464 466	syl5ibrcom	|- ( ph -> ( n = N -> -. n e. ( ( y + 1 ) ... ( N - 1 ) ) ) )
468	467	con2d	|- ( ph -> ( n e. ( ( y + 1 ) ... ( N - 1 ) ) -> -. n = N ) )
469	468	imp	|- ( ( ph /\ n e. ( ( y + 1 ) ... ( N - 1 ) ) ) -> -. n = N )
470	469	iffalsed	|- ( ( ph /\ n e. ( ( y + 1 ) ... ( N - 1 ) ) ) -> if ( n = N , 1 , ( n + 1 ) ) = ( n + 1 ) )
471	470	mpteq2dva	|- ( ph -> ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> if ( n = N , 1 , ( n + 1 ) ) ) = ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> ( n + 1 ) ) )
472	471	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> if ( n = N , 1 , ( n + 1 ) ) ) = ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> ( n + 1 ) ) )
473	462 472	eqtrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) |` ( ( y + 1 ) ... ( N - 1 ) ) ) = ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> ( n + 1 ) ) )
474	473	rneqd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ran ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) |` ( ( y + 1 ) ... ( N - 1 ) ) ) = ran ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> ( n + 1 ) ) )
475	456 474	syl5eq	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... ( N - 1 ) ) ) = ran ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> ( n + 1 ) ) )
476		elfzelz	|- ( j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) -> j e. ZZ )
477	476	zcnd	|- ( j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) -> j e. CC )
478	477 409	syl	|- ( j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) -> ( ( j - 1 ) + 1 ) = j )
479	478	eleq1d	|- ( j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) -> ( ( ( j - 1 ) + 1 ) e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) <-> j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
480	479	ibir	|- ( j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) -> ( ( j - 1 ) + 1 ) e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) )
481	480	adantl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) ) -> ( ( j - 1 ) + 1 ) e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) )
482	54	nnzd	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. ZZ )
483	120 482	anim12ci	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( y + 1 ) e. ZZ /\ ( N - 1 ) e. ZZ ) )
484	476 414	syl	|- ( j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) -> ( j - 1 ) e. ZZ )
485	484 121	jctir	|- ( j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) -> ( ( j - 1 ) e. ZZ /\ 1 e. ZZ ) )
486		fzaddel	|- ( ( ( ( y + 1 ) e. ZZ /\ ( N - 1 ) e. ZZ ) /\ ( ( j - 1 ) e. ZZ /\ 1 e. ZZ ) ) -> ( ( j - 1 ) e. ( ( y + 1 ) ... ( N - 1 ) ) <-> ( ( j - 1 ) + 1 ) e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
487	483 485 486	syl2an	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) ) -> ( ( j - 1 ) e. ( ( y + 1 ) ... ( N - 1 ) ) <-> ( ( j - 1 ) + 1 ) e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
488	481 487	mpbird	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) ) -> ( j - 1 ) e. ( ( y + 1 ) ... ( N - 1 ) ) )
489	477 421	syl	|- ( j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) -> j = ( ( j - 1 ) + 1 ) )
490	489	adantl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) ) -> j = ( ( j - 1 ) + 1 ) )
491	423	rspceeqv	|- ( ( ( j - 1 ) e. ( ( y + 1 ) ... ( N - 1 ) ) /\ j = ( ( j - 1 ) + 1 ) ) -> E. n e. ( ( y + 1 ) ... ( N - 1 ) ) j = ( n + 1 ) )
492	488 490 491	syl2anc	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) ) -> E. n e. ( ( y + 1 ) ... ( N - 1 ) ) j = ( n + 1 ) )
493	492	ex	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) -> E. n e. ( ( y + 1 ) ... ( N - 1 ) ) j = ( n + 1 ) ) )
494		simpr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( ( y + 1 ) ... ( N - 1 ) ) ) -> n e. ( ( y + 1 ) ... ( N - 1 ) ) )
495		elfzelz	|- ( n e. ( ( y + 1 ) ... ( N - 1 ) ) -> n e. ZZ )
496	495 121	jctir	|- ( n e. ( ( y + 1 ) ... ( N - 1 ) ) -> ( n e. ZZ /\ 1 e. ZZ ) )
497		fzaddel	|- ( ( ( ( y + 1 ) e. ZZ /\ ( N - 1 ) e. ZZ ) /\ ( n e. ZZ /\ 1 e. ZZ ) ) -> ( n e. ( ( y + 1 ) ... ( N - 1 ) ) <-> ( n + 1 ) e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
498	483 496 497	syl2an	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( ( y + 1 ) ... ( N - 1 ) ) ) -> ( n e. ( ( y + 1 ) ... ( N - 1 ) ) <-> ( n + 1 ) e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
499	494 498	mpbid	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( ( y + 1 ) ... ( N - 1 ) ) ) -> ( n + 1 ) e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) )
500		eleq1	|- ( j = ( n + 1 ) -> ( j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) <-> ( n + 1 ) e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
501	499 500	syl5ibrcom	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( ( y + 1 ) ... ( N - 1 ) ) ) -> ( j = ( n + 1 ) -> j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
502	501	rexlimdva	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( E. n e. ( ( y + 1 ) ... ( N - 1 ) ) j = ( n + 1 ) -> j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
503	493 502	impbid	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) <-> E. n e. ( ( y + 1 ) ... ( N - 1 ) ) j = ( n + 1 ) ) )
504		eqid	|- ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> ( n + 1 ) ) = ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> ( n + 1 ) )
505	504	elrnmpt	|- ( j e. _V -> ( j e. ran ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> ( n + 1 ) ) <-> E. n e. ( ( y + 1 ) ... ( N - 1 ) ) j = ( n + 1 ) ) )
506	505	elv	|- ( j e. ran ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> ( n + 1 ) ) <-> E. n e. ( ( y + 1 ) ... ( N - 1 ) ) j = ( n + 1 ) )
507	503 506	bitr4di	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( j e. ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) <-> j e. ran ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> ( n + 1 ) ) ) )
508	507	eqrdv	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) = ran ( n e. ( ( y + 1 ) ... ( N - 1 ) ) |-> ( n + 1 ) ) )
509	72	oveq2d	|- ( ph -> ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) = ( ( ( y + 1 ) + 1 ) ... N ) )
510	509	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( y + 1 ) + 1 ) ... ( ( N - 1 ) + 1 ) ) = ( ( ( y + 1 ) + 1 ) ... N ) )
511	475 508 510	3eqtr2rd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( y + 1 ) + 1 ) ... N ) = ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... ( N - 1 ) ) ) )
512	511	imaeq2d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... ( N - 1 ) ) ) ) )
513	455 512	uneq12d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " { N } ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) " ( ( y + 1 ) ... ( N - 1 ) ) ) ) ) )
514	439 448 513	3eqtr4a	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) = ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) )
515	514	xpeq1d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) = ( ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) X. { 0 } ) )
516		xpundir	|- ( ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } u. ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) X. { 0 } ) = ( ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) )
517	515 516	eqtrdi	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) = ( ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
518	434 517	uneq12d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
519		unass	|- ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
520		un23	|- ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) )
521	519 520	eqtr3i	|- ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) )
522	518 521	eqtrdi	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) ) )
523	522	fveq1d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) ) ` n ) )
524	523	ad2antrr	|- ( ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) /\ -. n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 + 1 ) ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` 1 ) } X. { 0 } ) ) ` n ) )
525	349 367 524	3eqtr4d	|- ( ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) /\ -. n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
526		snssi	|- ( 1 e. CC -> { 1 } C_ CC )
527	141 526	ax-mp	|- { 1 } C_ CC
528		0cn	|- 0 e. CC
529		snssi	|- ( 0 e. CC -> { 0 } C_ CC )
530	528 529	ax-mp	|- { 0 } C_ CC
531	527 530	unssi	|- ( { 1 } u. { 0 } ) C_ CC
532	34	fconst	|- ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) : ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) --> { 1 }
533	37	fconst	|- ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) : ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) --> { 0 }
534	532 533	pm3.2i	|- ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) : ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) --> { 1 } /\ ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) : ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) --> { 0 } )
535		fun	|- ( ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) : ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) --> { 1 } /\ ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) : ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) --> { 0 } ) /\ ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) i^i ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) ) = (/) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) : ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) u. ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) )
536	534 241 535	sylancr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) : ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) u. ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) )
537		imaundi	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( 1 ... y ) u. ( ( y + 1 ) ... N ) ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) u. ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) )
538		fzsplit2	|- ( ( ( y + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` y ) ) -> ( 1 ... N ) = ( ( 1 ... y ) u. ( ( y + 1 ) ... N ) ) )
539	67 373 538	syl2an2	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... y ) u. ( ( y + 1 ) ... N ) ) )
540	539	imaeq2d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... N ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( 1 ... y ) u. ( ( y + 1 ) ... N ) ) ) )
541		f1ofo	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
542		foima	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
543	228 541 542	3syl	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
544	543	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
545	540 544	eqtr3d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( 1 ... y ) u. ( ( y + 1 ) ... N ) ) ) = ( 1 ... N ) )
546	537 545	eqtr3id	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) u. ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) ) = ( 1 ... N ) )
547	546	feq2d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) : ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) u. ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) ) --> ( { 1 } u. { 0 } ) <-> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) : ( 1 ... N ) --> ( { 1 } u. { 0 } ) ) )
548	536 547	mpbid	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) : ( 1 ... N ) --> ( { 1 } u. { 0 } ) )
549	548	ffvelrnda	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) e. ( { 1 } u. { 0 } ) )
550	531 549	sselid	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) e. CC )
551	550	addid2d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) -> ( 0 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) = ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
552	551	adantr	|- ( ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) /\ -. n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) -> ( 0 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) = ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
553	525 552	eqtr4d	|- ( ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) /\ -. n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( 0 + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) )
554	96 98 287 553	ifbothda	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) )
555	554	oveq2d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` n ) + ( if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) ) )
556		elmapi	|- ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
557	30 556	syl	|- ( ph -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
558	557	ffvelrnda	|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. ( 0 ..^ K ) )
559		elfzonn0	|- ( ( ( 1st ` ( 1st ` T ) ) ` n ) e. ( 0 ..^ K ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. NN0 )
560	558 559	syl	|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. NN0 )
561	560	nn0cnd	|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. CC )
562	561	adantlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. CC )
563	141 528	ifcli	|- if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) e. CC
564	563	a1i	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) -> if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) e. CC )
565	562 564 550	addassd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` n ) + ( if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) ) )
566	555 565	eqtr4d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) = ( ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) )
567	566	mpteq2dva	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) ) = ( n e. ( 1 ... N ) |-> ( ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) ) )
568	94 567	eqtrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) = ( n e. ( 1 ... N ) |-> ( ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) ) )
569	6	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 2nd ` T ) = 0 )
570		elfzle1	|- ( y e. ( 0 ... ( N - 1 ) ) -> 0 <_ y )
571	570	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> 0 <_ y )
572	569 571	eqbrtrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 2nd ` T ) <_ y )
573		0re	|- 0 e. RR
574	6 573	eqeltrdi	|- ( ph -> ( 2nd ` T ) e. RR )
575		lenlt	|- ( ( ( 2nd ` T ) e. RR /\ y e. RR ) -> ( ( 2nd ` T ) <_ y <-> -. y < ( 2nd ` T ) ) )
576	574 234 575	syl2an	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) <_ y <-> -. y < ( 2nd ` T ) ) )
577	572 576	mpbid	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> -. y < ( 2nd ` T ) )
578	577	iffalsed	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = ( y + 1 ) )
579	578	csbeq1d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ ( y + 1 ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
580		ovex	|- ( y + 1 ) e. _V
581		oveq2	|- ( j = ( y + 1 ) -> ( 1 ... j ) = ( 1 ... ( y + 1 ) ) )
582	581	imaeq2d	|- ( j = ( y + 1 ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) )
583	582	xpeq1d	|- ( j = ( y + 1 ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) )
584		oveq1	|- ( j = ( y + 1 ) -> ( j + 1 ) = ( ( y + 1 ) + 1 ) )
585	584	oveq1d	|- ( j = ( y + 1 ) -> ( ( j + 1 ) ... N ) = ( ( ( y + 1 ) + 1 ) ... N ) )
586	585	imaeq2d	|- ( j = ( y + 1 ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
587	586	xpeq1d	|- ( j = ( y + 1 ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) )
588	583 587	uneq12d	|- ( j = ( y + 1 ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
589	588	oveq2d	|- ( j = ( y + 1 ) -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
590	580 589	csbie	|- [_ ( y + 1 ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
591	579 590	eqtrdi	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
592		ovexd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) e. _V )
593		fvexd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) e. _V )
594		eqidd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) = ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) )
595	548	ffnd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
596		nfcv	|- F/_ n ( 2nd ` ( 1st ` T ) )
597		nfmpt1	|- F/_ n ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) )
598	596 597	nfco	|- F/_ n ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) )
599		nfcv	|- F/_ n ( 1 ... y )
600	598 599	nfima	|- F/_ n ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) )
601		nfcv	|- F/_ n { 1 }
602	600 601	nfxp	|- F/_ n ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } )
603		nfcv	|- F/_ n ( ( y + 1 ) ... N )
604	598 603	nfima	|- F/_ n ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) )
605		nfcv	|- F/_ n { 0 }
606	604 605	nfxp	|- F/_ n ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } )
607	602 606	nfun	|- F/_ n ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) )
608	607	dffn5f	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) <-> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) = ( n e. ( 1 ... N ) |-> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) )
609	595 608	sylib	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) = ( n e. ( 1 ... N ) |-> ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) )
610	90 592 593 594 609	offval2	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) = ( n e. ( 1 ... N ) |-> ( ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) + ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) ) )
611	568 591 610	3eqtr4rd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
612	611	mpteq2dva	|- ( ph -> ( y e. ( 0 ... ( N - 1 ) ) |-> ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
613	23 612	eqtr4d	|- ( ph -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) + if ( n = ( ( 2nd ` ( 1st ` T ) ) ` 1 ) , 1 , 0 ) ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = N , 1 , ( n + 1 ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) )