Theorem poimirlem19

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