Theorem poimirlem20

Description: Lemma for poimir establishing existence for poimirlem21 . (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	poimirlem20	|- ( ph -> E. z e. S z =/= T )

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		oveq2	|- ( 1 = if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - 1 ) = ( ( ( 1st ` ( 1st ` T ) ) ` n ) - if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) ) )
8	7	eleq1d	|- ( 1 = if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) -> ( ( ( ( 1st ` ( 1st ` T ) ) ` n ) - 1 ) e. ( 0 ..^ K ) <-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) ) e. ( 0 ..^ K ) ) )
9		oveq2	|- ( 0 = if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - 0 ) = ( ( ( 1st ` ( 1st ` T ) ) ` n ) - if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) ) )
10	9	eleq1d	|- ( 0 = if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) -> ( ( ( ( 1st ` ( 1st ` T ) ) ` n ) - 0 ) e. ( 0 ..^ K ) <-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) ) e. ( 0 ..^ K ) ) )
11		fveq2	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) = ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) )
12	11	oveq1d	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - 1 ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) - 1 ) )
13	12	adantl	|- ( ( ph /\ n = ( ( 2nd ` ( 1st ` T ) ) ` N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - 1 ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) - 1 ) )
14		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 ) ) )
15	14 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 ) ) )
16	4 15	syl	|- ( ph -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
17		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 ) } ) )
18	16 17	syl	|- ( ph -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
19		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 ) ) )
20	18 19	syl	|- ( ph -> ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
21		elmapi	|- ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
22	20 21	syl	|- ( ph -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
23		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 ) } )
24	18 23	syl	|- ( ph -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
25		fvex	|- ( 2nd ` ( 1st ` T ) ) e. _V
26		f1oeq1	|- ( f = ( 2nd ` ( 1st ` T ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
27	25 26	elab	|- ( ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
28	24 27	sylib	|- ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
29		f1of	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 1 ... N ) )
30	28 29	syl	|- ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 1 ... N ) )
31		elfz1end	|- ( N e. NN <-> N e. ( 1 ... N ) )
32	1 31	sylib	|- ( ph -> N e. ( 1 ... N ) )
33	30 32	ffvelrnd	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) ` N ) e. ( 1 ... N ) )
34	22 33	ffvelrnd	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. ( 0 ..^ K ) )
35		elfzonn0	|- ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. ( 0 ..^ K ) -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. NN0 )
36	34 35	syl	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. NN0 )
37		fvex	|- ( ( 2nd ` ( 1st ` T ) ) ` N ) e. _V
38		eleq1	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) -> ( n e. ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` T ) ) ` N ) e. ( 1 ... N ) ) )
39	38	anbi2d	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) -> ( ( ph /\ n e. ( 1 ... N ) ) <-> ( ph /\ ( ( 2nd ` ( 1st ` T ) ) ` N ) e. ( 1 ... N ) ) ) )
40		fveq2	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) -> ( p ` n ) = ( p ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) )
41	40	neeq1d	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) -> ( ( p ` n ) =/= 0 <-> ( p ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) =/= 0 ) )
42	41	rexbidv	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) -> ( E. p e. ran F ( p ` n ) =/= 0 <-> E. p e. ran F ( p ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) =/= 0 ) )
43	39 42	imbi12d	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) -> ( ( ( ph /\ n e. ( 1 ... N ) ) -> E. p e. ran F ( p ` n ) =/= 0 ) <-> ( ( ph /\ ( ( 2nd ` ( 1st ` T ) ) ` N ) e. ( 1 ... N ) ) -> E. p e. ran F ( p ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) =/= 0 ) ) )
44	37 43 5	vtocl	|- ( ( ph /\ ( ( 2nd ` ( 1st ` T ) ) ` N ) e. ( 1 ... N ) ) -> E. p e. ran F ( p ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) =/= 0 )
45	33 44	mpdan	|- ( ph -> E. p e. ran F ( p ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) =/= 0 )
46		fveq1	|- ( p = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) -> ( p ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) )
47	22	ffnd	|- ( ph -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
48	47	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
49		1ex	|- 1 e. _V
50		fnconstg	|- ( 1 e. _V -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) )
51	49 50	ax-mp	|- ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) )
52		c0ex	|- 0 e. _V
53		fnconstg	|- ( 0 e. _V -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) )
54	52 53	ax-mp	|- ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) )
55	51 54	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 ) ) )
56		dff1o3	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( 2nd ` ( 1st ` T ) ) ) )
57	56	simprbi	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' ( 2nd ` ( 1st ` T ) ) )
58	28 57	syl	|- ( ph -> Fun `' ( 2nd ` ( 1st ` T ) ) )
59		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 ) ) ) )
60	58 59	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 ) ) ) )
61		elfznn0	|- ( y e. ( 0 ... ( N - 1 ) ) -> y e. NN0 )
62	61	nn0red	|- ( y e. ( 0 ... ( N - 1 ) ) -> y e. RR )
63	62	ltp1d	|- ( y e. ( 0 ... ( N - 1 ) ) -> y < ( y + 1 ) )
64		fzdisj	|- ( y < ( y + 1 ) -> ( ( 1 ... y ) i^i ( ( y + 1 ) ... N ) ) = (/) )
65	63 64	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( 1 ... y ) i^i ( ( y + 1 ) ... N ) ) = (/) )
66	65	imaeq2d	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... y ) i^i ( ( y + 1 ) ... N ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " (/) ) )
67		ima0	|- ( ( 2nd ` ( 1st ` T ) ) " (/) ) = (/)
68	66 67	eqtrdi	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... y ) i^i ( ( y + 1 ) ... N ) ) ) = (/) )
69	60 68	sylan9req	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) ) = (/) )
70		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 ) ) ) )
71	55 69 70	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 ) ) ) )
72		imaundi	|- ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... y ) u. ( ( y + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) )
73		nn0p1nn	|- ( y e. NN0 -> ( y + 1 ) e. NN )
74		nnuz	|- NN = ( ZZ>= ` 1 )
75	73 74	eleqtrdi	|- ( y e. NN0 -> ( y + 1 ) e. ( ZZ>= ` 1 ) )
76	61 75	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. ( ZZ>= ` 1 ) )
77	76	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( y + 1 ) e. ( ZZ>= ` 1 ) )
78	1	nncnd	|- ( ph -> N e. CC )
79		npcan1	|- ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
80	78 79	syl	|- ( ph -> ( ( N - 1 ) + 1 ) = N )
81	80	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) = N )
82		elfzuz3	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` y ) )
83		peano2uz	|- ( ( N - 1 ) e. ( ZZ>= ` y ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` y ) )
84	82 83	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` y ) )
85	84	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` y ) )
86	81 85	eqeltrrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ZZ>= ` y ) )
87		fzsplit2	|- ( ( ( y + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` y ) ) -> ( 1 ... N ) = ( ( 1 ... y ) u. ( ( y + 1 ) ... N ) ) )
88	77 86 87	syl2anc	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... y ) u. ( ( y + 1 ) ... N ) ) )
89	88	imaeq2d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... y ) u. ( ( y + 1 ) ... N ) ) ) )
90		f1ofo	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
91		foima	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
92	28 90 91	3syl	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
93	92	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
94	89 93	eqtr3d	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... y ) u. ( ( y + 1 ) ... N ) ) ) = ( 1 ... N ) )
95	72 94	eqtr3id	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) ) = ( 1 ... N ) )
96	95	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 ) ) )
97	71 96	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 ) )
98		ovex	|- ( 1 ... N ) e. _V
99	98	a1i	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ... N ) e. _V )
100		inidm	|- ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
101		eqidd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( ( 2nd ` ( 1st ` T ) ) ` N ) e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) = ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) )
102		f1ofn	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
103	28 102	syl	|- ( ph -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
104	103	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
105		fzss1	|- ( ( y + 1 ) e. ( ZZ>= ` 1 ) -> ( ( y + 1 ) ... N ) C_ ( 1 ... N ) )
106	76 105	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) ... N ) C_ ( 1 ... N ) )
107	106	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( y + 1 ) ... N ) C_ ( 1 ... N ) )
108		eluzp1p1	|- ( ( N - 1 ) e. ( ZZ>= ` y ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
109		uzss	|- ( ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) -> ( ZZ>= ` ( ( N - 1 ) + 1 ) ) C_ ( ZZ>= ` ( y + 1 ) ) )
110	82 108 109	3syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ZZ>= ` ( ( N - 1 ) + 1 ) ) C_ ( ZZ>= ` ( y + 1 ) ) )
111	110	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ZZ>= ` ( ( N - 1 ) + 1 ) ) C_ ( ZZ>= ` ( y + 1 ) ) )
112	1	nnzd	|- ( ph -> N e. ZZ )
113	112	uzidd	|- ( ph -> N e. ( ZZ>= ` N ) )
114	80	fveq2d	|- ( ph -> ( ZZ>= ` ( ( N - 1 ) + 1 ) ) = ( ZZ>= ` N ) )
115	113 114	eleqtrrd	|- ( ph -> N e. ( ZZ>= ` ( ( N - 1 ) + 1 ) ) )
116	115	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ZZ>= ` ( ( N - 1 ) + 1 ) ) )
117	111 116	sseldd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ZZ>= ` ( y + 1 ) ) )
118		eluzfz2	|- ( N e. ( ZZ>= ` ( y + 1 ) ) -> N e. ( ( y + 1 ) ... N ) )
119	117 118	syl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ( y + 1 ) ... N ) )
120		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 ) ) )
121	104 107 119 120	syl3anc	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` ( 1st ` T ) ) ` N ) e. ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) )
122		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 ) ) )
123	51 54 122	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 ) ) )
124	69 121 123	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 ) ) )
125	52	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 )
126	121 125	syl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) = 0 )
127	124 126	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 )
128	127	adantr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( ( 2nd ` ( 1st ` T ) ) ` N ) e. ( 1 ... N ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) = 0 )
129	48 97 99 99 100 101 128	ofval	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( ( 2nd ` ( 1st ` T ) ) ` N ) e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) + 0 ) )
130	33 129	mpidan	|- ( ( 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 } ) ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) + 0 ) )
131	36	nn0cnd	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. CC )
132	131	addid1d	|- ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) + 0 ) = ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) )
133	132	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) + 0 ) = ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) )
134	130 133	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 } ) ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) = ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) )
135	46 134	sylan9eqr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ p = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ( p ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) = ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) )
136	135	adantllr	|- ( ( ( ( ph /\ p e. ran F ) /\ y e. ( 0 ... ( N - 1 ) ) ) /\ p = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) -> ( p ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) = ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) )
137		fveq2	|- ( t = T -> ( 2nd ` t ) = ( 2nd ` T ) )
138	137	breq2d	|- ( t = T -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` T ) ) )
139	138	ifbid	|- ( t = T -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) )
140		2fveq3	|- ( t = T -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) )
141		2fveq3	|- ( t = T -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` T ) ) )
142	141	imaeq1d	|- ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) )
143	142	xpeq1d	|- ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) )
144	141	imaeq1d	|- ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) )
145	144	xpeq1d	|- ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
146	143 145	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 } ) ) )
147	140 146	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 } ) ) ) )
148	139 147	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 } ) ) ) )
149	148	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 } ) ) ) ) )
150	149	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 } ) ) ) ) ) )
151	150 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 } ) ) ) ) ) )
152	151	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 } ) ) ) ) )
153	4 152	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 } ) ) ) ) )
154	62	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y e. RR )
155		peano2zm	|- ( N e. ZZ -> ( N - 1 ) e. ZZ )
156	112 155	syl	|- ( ph -> ( N - 1 ) e. ZZ )
157	156	zred	|- ( ph -> ( N - 1 ) e. RR )
158	157	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( N - 1 ) e. RR )
159	1	nnred	|- ( ph -> N e. RR )
160	159	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. RR )
161		elfzle2	|- ( y e. ( 0 ... ( N - 1 ) ) -> y <_ ( N - 1 ) )
162	161	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y <_ ( N - 1 ) )
163	159	ltm1d	|- ( ph -> ( N - 1 ) < N )
164	163	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( N - 1 ) < N )
165	154 158 160 162 164	lelttrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y < N )
166	6	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 2nd ` T ) = N )
167	165 166	breqtrrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> y < ( 2nd ` T ) )
168	167	iftrued	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = y )
169	168	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 } ) ) ) )
170		vex	|- y e. _V
171		oveq2	|- ( j = y -> ( 1 ... j ) = ( 1 ... y ) )
172	171	imaeq2d	|- ( j = y -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) )
173	172	xpeq1d	|- ( j = y -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) )
174		oveq1	|- ( j = y -> ( j + 1 ) = ( y + 1 ) )
175	174	oveq1d	|- ( j = y -> ( ( j + 1 ) ... N ) = ( ( y + 1 ) ... N ) )
176	175	imaeq2d	|- ( j = y -> ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) )
177	176	xpeq1d	|- ( j = y -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) )
178	173 177	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 } ) ) )
179	178	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 } ) ) ) )
180	170 179	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 } ) ) )
181	169 180	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 } ) ) ) )
182	181	mpteq2dva	|- ( 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 e. ( 0 ... ( N - 1 ) ) |-> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
183	153 182	eqtrd	|- ( ph -> F = ( 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 } ) ) ) ) )
184	183	rneqd	|- ( ph -> ran F = ran ( 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 } ) ) ) ) )
185	184	eleq2d	|- ( ph -> ( p e. ran F <-> p e. ran ( 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 } ) ) ) ) ) )
186		eqid	|- ( 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 } ) ) ) ) = ( 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 } ) ) ) )
187		ovex	|- ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V
188	186 187	elrnmpti	|- ( p e. ran ( 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 } ) ) ) ) <-> E. y e. ( 0 ... ( N - 1 ) ) p = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) )
189	185 188	bitrdi	|- ( ph -> ( p e. ran F <-> E. y e. ( 0 ... ( N - 1 ) ) p = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
190	189	biimpa	|- ( ( ph /\ p e. ran F ) -> E. y e. ( 0 ... ( N - 1 ) ) p = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) )
191	136 190	r19.29a	|- ( ( ph /\ p e. ran F ) -> ( p ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) = ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) )
192	191	neeq1d	|- ( ( ph /\ p e. ran F ) -> ( ( p ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) =/= 0 <-> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) =/= 0 ) )
193	192	biimpd	|- ( ( ph /\ p e. ran F ) -> ( ( p ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) =/= 0 -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) =/= 0 ) )
194	193	rexlimdva	|- ( ph -> ( E. p e. ran F ( p ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) =/= 0 -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) =/= 0 ) )
195	45 194	mpd	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) =/= 0 )
196		elnnne0	|- ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. NN <-> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. NN0 /\ ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) =/= 0 ) )
197	36 195 196	sylanbrc	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. NN )
198		nnm1nn0	|- ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. NN -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) - 1 ) e. NN0 )
199	197 198	syl	|- ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) - 1 ) e. NN0 )
200		elfzo0	|- ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. ( 0 ..^ K ) <-> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. NN0 /\ K e. NN /\ ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) < K ) )
201	34 200	sylib	|- ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. NN0 /\ K e. NN /\ ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) < K ) )
202	201	simp2d	|- ( ph -> K e. NN )
203	199	nn0red	|- ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) - 1 ) e. RR )
204	36	nn0red	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. RR )
205	202	nnred	|- ( ph -> K e. RR )
206	204	ltm1d	|- ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) - 1 ) < ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) )
207		elfzolt2	|- ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) e. ( 0 ..^ K ) -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) < K )
208	34 207	syl	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) < K )
209	203 204 205 206 208	lttrd	|- ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) - 1 ) < K )
210		elfzo0	|- ( ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) - 1 ) e. ( 0 ..^ K ) <-> ( ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) - 1 ) e. NN0 /\ K e. NN /\ ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) - 1 ) < K ) )
211	199 202 209 210	syl3anbrc	|- ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) - 1 ) e. ( 0 ..^ K ) )
212	211	adantr	|- ( ( ph /\ n = ( ( 2nd ` ( 1st ` T ) ) ` N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` N ) ) - 1 ) e. ( 0 ..^ K ) )
213	13 212	eqeltrd	|- ( ( ph /\ n = ( ( 2nd ` ( 1st ` T ) ) ` N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - 1 ) e. ( 0 ..^ K ) )
214	213	adantlr	|- ( ( ( ph /\ n e. ( 1 ... N ) ) /\ n = ( ( 2nd ` ( 1st ` T ) ) ` N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - 1 ) e. ( 0 ..^ K ) )
215	22	ffvelrnda	|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. ( 0 ..^ K ) )
216		elfzonn0	|- ( ( ( 1st ` ( 1st ` T ) ) ` n ) e. ( 0 ..^ K ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. NN0 )
217	215 216	syl	|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. NN0 )
218	217	nn0cnd	|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) e. CC )
219	218	subid1d	|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - 0 ) = ( ( 1st ` ( 1st ` T ) ) ` n ) )
220	219 215	eqeltrd	|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - 0 ) e. ( 0 ..^ K ) )
221	220	adantr	|- ( ( ( ph /\ n e. ( 1 ... N ) ) /\ -. n = ( ( 2nd ` ( 1st ` T ) ) ` N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - 0 ) e. ( 0 ..^ K ) )
222	8 10 214 221	ifbothda	|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) ) e. ( 0 ..^ K ) )
223	222	fmpttd	|- ( ph -> ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
224		ovex	|- ( 0 ..^ K ) e. _V
225	224 98	elmap	|- ( ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) <-> ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
226	223 225	sylibr	|- ( ph -> ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
227		simpr	|- ( ( ph /\ n e. ( ( 1 + 1 ) ... N ) ) -> n e. ( ( 1 + 1 ) ... N ) )
228		1z	|- 1 e. ZZ
229		peano2z	|- ( 1 e. ZZ -> ( 1 + 1 ) e. ZZ )
230	228 229	ax-mp	|- ( 1 + 1 ) e. ZZ
231	112 230	jctil	|- ( ph -> ( ( 1 + 1 ) e. ZZ /\ N e. ZZ ) )
232		elfzelz	|- ( n e. ( ( 1 + 1 ) ... N ) -> n e. ZZ )
233	232 228	jctir	|- ( n e. ( ( 1 + 1 ) ... N ) -> ( n e. ZZ /\ 1 e. ZZ ) )
234		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 ) ) ) )
235	231 233 234	syl2an	|- ( ( ph /\ n e. ( ( 1 + 1 ) ... N ) ) -> ( n e. ( ( 1 + 1 ) ... N ) <-> ( n - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) ) )
236	227 235	mpbid	|- ( ( ph /\ n e. ( ( 1 + 1 ) ... N ) ) -> ( n - 1 ) e. ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) )
237		ax-1cn	|- 1 e. CC
238	237 237	pncan3oi	|- ( ( 1 + 1 ) - 1 ) = 1
239	238	oveq1i	|- ( ( ( 1 + 1 ) - 1 ) ... ( N - 1 ) ) = ( 1 ... ( N - 1 ) )
240	236 239	eleqtrdi	|- ( ( ph /\ n e. ( ( 1 + 1 ) ... N ) ) -> ( n - 1 ) e. ( 1 ... ( N - 1 ) ) )
241	240	ralrimiva	|- ( ph -> A. n e. ( ( 1 + 1 ) ... N ) ( n - 1 ) e. ( 1 ... ( N - 1 ) ) )
242		simpr	|- ( ( ph /\ y e. ( 1 ... ( N - 1 ) ) ) -> y e. ( 1 ... ( N - 1 ) ) )
243	156 228	jctil	|- ( ph -> ( 1 e. ZZ /\ ( N - 1 ) e. ZZ ) )
244		elfzelz	|- ( y e. ( 1 ... ( N - 1 ) ) -> y e. ZZ )
245	244 228	jctir	|- ( y e. ( 1 ... ( N - 1 ) ) -> ( y e. ZZ /\ 1 e. ZZ ) )
246		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 ) ) ) )
247	243 245 246	syl2an	|- ( ( ph /\ y e. ( 1 ... ( N - 1 ) ) ) -> ( y e. ( 1 ... ( N - 1 ) ) <-> ( y + 1 ) e. ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) ) )
248	242 247	mpbid	|- ( ( ph /\ y e. ( 1 ... ( N - 1 ) ) ) -> ( y + 1 ) e. ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) )
249	80	oveq2d	|- ( ph -> ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) = ( ( 1 + 1 ) ... N ) )
250	249	adantr	|- ( ( ph /\ y e. ( 1 ... ( N - 1 ) ) ) -> ( ( 1 + 1 ) ... ( ( N - 1 ) + 1 ) ) = ( ( 1 + 1 ) ... N ) )
251	248 250	eleqtrd	|- ( ( ph /\ y e. ( 1 ... ( N - 1 ) ) ) -> ( y + 1 ) e. ( ( 1 + 1 ) ... N ) )
252	232	zcnd	|- ( n e. ( ( 1 + 1 ) ... N ) -> n e. CC )
253	244	zcnd	|- ( y e. ( 1 ... ( N - 1 ) ) -> y e. CC )
254		subadd2	|- ( ( n e. CC /\ 1 e. CC /\ y e. CC ) -> ( ( n - 1 ) = y <-> ( y + 1 ) = n ) )
255	237 254	mp3an2	|- ( ( n e. CC /\ y e. CC ) -> ( ( n - 1 ) = y <-> ( y + 1 ) = n ) )
256		eqcom	|- ( y = ( n - 1 ) <-> ( n - 1 ) = y )
257		eqcom	|- ( n = ( y + 1 ) <-> ( y + 1 ) = n )
258	255 256 257	3bitr4g	|- ( ( n e. CC /\ y e. CC ) -> ( y = ( n - 1 ) <-> n = ( y + 1 ) ) )
259	252 253 258	syl2anr	|- ( ( y e. ( 1 ... ( N - 1 ) ) /\ n e. ( ( 1 + 1 ) ... N ) ) -> ( y = ( n - 1 ) <-> n = ( y + 1 ) ) )
260	259	ralrimiva	|- ( y e. ( 1 ... ( N - 1 ) ) -> A. n e. ( ( 1 + 1 ) ... N ) ( y = ( n - 1 ) <-> n = ( y + 1 ) ) )
261	260	adantl	|- ( ( ph /\ y e. ( 1 ... ( N - 1 ) ) ) -> A. n e. ( ( 1 + 1 ) ... N ) ( y = ( n - 1 ) <-> n = ( y + 1 ) ) )
262		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 ) )
263	251 261 262	syl2anc	|- ( ( ph /\ y e. ( 1 ... ( N - 1 ) ) ) -> E! n e. ( ( 1 + 1 ) ... N ) y = ( n - 1 ) )
264	263	ralrimiva	|- ( ph -> A. y e. ( 1 ... ( N - 1 ) ) E! n e. ( ( 1 + 1 ) ... N ) y = ( n - 1 ) )
265		eqid	|- ( n e. ( ( 1 + 1 ) ... N ) |-> ( n - 1 ) ) = ( n e. ( ( 1 + 1 ) ... N ) |-> ( n - 1 ) )
266	265	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 ) ) )
267	241 264 266	sylanbrc	|- ( ph -> ( n e. ( ( 1 + 1 ) ... N ) |-> ( n - 1 ) ) : ( ( 1 + 1 ) ... N ) -1-1-onto-> ( 1 ... ( N - 1 ) ) )
268		f1osng	|- ( ( 1 e. _V /\ N e. NN ) -> { <. 1 , N >. } : { 1 } -1-1-onto-> { N } )
269	49 1 268	sylancr	|- ( ph -> { <. 1 , N >. } : { 1 } -1-1-onto-> { N } )
270	157 159	ltnled	|- ( ph -> ( ( N - 1 ) < N <-> -. N <_ ( N - 1 ) ) )
271	163 270	mpbid	|- ( ph -> -. N <_ ( N - 1 ) )
272		elfzle2	|- ( N e. ( 1 ... ( N - 1 ) ) -> N <_ ( N - 1 ) )
273	271 272	nsyl	|- ( ph -> -. N e. ( 1 ... ( N - 1 ) ) )
274		disjsn	|- ( ( ( 1 ... ( N - 1 ) ) i^i { N } ) = (/) <-> -. N e. ( 1 ... ( N - 1 ) ) )
275	273 274	sylibr	|- ( ph -> ( ( 1 ... ( N - 1 ) ) i^i { N } ) = (/) )
276		1re	|- 1 e. RR
277	276	ltp1i	|- 1 < ( 1 + 1 )
278	230	zrei	|- ( 1 + 1 ) e. RR
279	276 278	ltnlei	|- ( 1 < ( 1 + 1 ) <-> -. ( 1 + 1 ) <_ 1 )
280	277 279	mpbi	|- -. ( 1 + 1 ) <_ 1
281		elfzle1	|- ( 1 e. ( ( 1 + 1 ) ... N ) -> ( 1 + 1 ) <_ 1 )
282	280 281	mto	|- -. 1 e. ( ( 1 + 1 ) ... N )
283		disjsn	|- ( ( ( ( 1 + 1 ) ... N ) i^i { 1 } ) = (/) <-> -. 1 e. ( ( 1 + 1 ) ... N ) )
284	282 283	mpbir	|- ( ( ( 1 + 1 ) ... N ) i^i { 1 } ) = (/)
285		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 } ) )
286	284 285	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 } ) )
287	267 269 275 286	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 } ) )
288		eleq1	|- ( n = 1 -> ( n e. ( ( 1 + 1 ) ... N ) <-> 1 e. ( ( 1 + 1 ) ... N ) ) )
289	282 288	mtbiri	|- ( n = 1 -> -. n e. ( ( 1 + 1 ) ... N ) )
290	289	necon2ai	|- ( n e. ( ( 1 + 1 ) ... N ) -> n =/= 1 )
291		ifnefalse	|- ( n =/= 1 -> if ( n = 1 , N , ( n - 1 ) ) = ( n - 1 ) )
292	290 291	syl	|- ( n e. ( ( 1 + 1 ) ... N ) -> if ( n = 1 , N , ( n - 1 ) ) = ( n - 1 ) )
293	292	mpteq2ia	|- ( n e. ( ( 1 + 1 ) ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) = ( n e. ( ( 1 + 1 ) ... N ) |-> ( n - 1 ) )
294	293	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 >. } )
295	49	a1i	|- ( ph -> 1 e. _V )
296	1 74	eleqtrdi	|- ( ph -> N e. ( ZZ>= ` 1 ) )
297		fzpred	|- ( N e. ( ZZ>= ` 1 ) -> ( 1 ... N ) = ( { 1 } u. ( ( 1 + 1 ) ... N ) ) )
298	296 297	syl	|- ( ph -> ( 1 ... N ) = ( { 1 } u. ( ( 1 + 1 ) ... N ) ) )
299		uncom	|- ( { 1 } u. ( ( 1 + 1 ) ... N ) ) = ( ( ( 1 + 1 ) ... N ) u. { 1 } )
300	298 299	eqtr2di	|- ( ph -> ( ( ( 1 + 1 ) ... N ) u. { 1 } ) = ( 1 ... N ) )
301		iftrue	|- ( n = 1 -> if ( n = 1 , N , ( n - 1 ) ) = N )
302	301	adantl	|- ( ( ph /\ n = 1 ) -> if ( n = 1 , N , ( n - 1 ) ) = N )
303	295 1 300 302	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 ) ) ) )
304	294 303	eqtr3id	|- ( ph -> ( ( n e. ( ( 1 + 1 ) ... N ) |-> ( n - 1 ) ) u. { <. 1 , N >. } ) = ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) )
305	80 296	eqeltrd	|- ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
306		uzid	|- ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
307		peano2uz	|- ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
308	156 306 307	3syl	|- ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
309	80 308	eqeltrrd	|- ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
310		fzsplit2	|- ( ( ( ( N - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` ( N - 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
311	305 309 310	syl2anc	|- ( ph -> ( 1 ... N ) = ( ( 1 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) )
312	80	oveq1d	|- ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = ( N ... N ) )
313		fzsn	|- ( N e. ZZ -> ( N ... N ) = { N } )
314	112 313	syl	|- ( ph -> ( N ... N ) = { N } )
315	312 314	eqtrd	|- ( ph -> ( ( ( N - 1 ) + 1 ) ... N ) = { N } )
316	315	uneq2d	|- ( ph -> ( ( 1 ... ( N - 1 ) ) u. ( ( ( N - 1 ) + 1 ) ... N ) ) = ( ( 1 ... ( N - 1 ) ) u. { N } ) )
317	311 316	eqtr2d	|- ( ph -> ( ( 1 ... ( N - 1 ) ) u. { N } ) = ( 1 ... N ) )
318	304 300 317	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 ) ) )
319	287 318	mpbid	|- ( ph -> ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
320		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 ) )
321	28 319 320	syl2anc	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
322	98	mptex	|- ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) e. _V
323	25 322	coex	|- ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) e. _V
324		f1oeq1	|- ( f = ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) -> ( f : ( 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 ) ) )
325	323 324	elab	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) e. { f | f : ( 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 ) )
326	321 325	sylibr	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
327	226 326	opelxpd	|- ( ph -> <. ( 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 ) ) ) ) >. e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
328	1	nnnn0d	|- ( ph -> N e. NN0 )
329		0elfz	|- ( N e. NN0 -> 0 e. ( 0 ... N ) )
330	328 329	syl	|- ( ph -> 0 e. ( 0 ... N ) )
331	327 330	opelxpd	|- ( ph -> <. <. ( 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 ) ) ) ) >. , 0 >. e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
332	1 2 3 4 5 6	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 } ) ) ) ) )
333		elfzle1	|- ( y e. ( 0 ... ( N - 1 ) ) -> 0 <_ y )
334		0re	|- 0 e. RR
335		lenlt	|- ( ( 0 e. RR /\ y e. RR ) -> ( 0 <_ y <-> -. y < 0 ) )
336	334 62 335	sylancr	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( 0 <_ y <-> -. y < 0 ) )
337	333 336	mpbid	|- ( y e. ( 0 ... ( N - 1 ) ) -> -. y < 0 )
338	337	iffalsed	|- ( y e. ( 0 ... ( N - 1 ) ) -> if ( y < 0 , y , ( y + 1 ) ) = ( y + 1 ) )
339	338	csbeq1d	|- ( y e. ( 0 ... ( N - 1 ) ) -> [_ if ( y < 0 , y , ( y + 1 ) ) / j ]_ ( ( 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 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ ( y + 1 ) / j ]_ ( ( 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 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
340		ovex	|- ( y + 1 ) e. _V
341		oveq2	|- ( j = ( y + 1 ) -> ( 1 ... j ) = ( 1 ... ( y + 1 ) ) )
342	341	imaeq2d	|- ( j = ( y + 1 ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( 1 ... j ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( 1 ... ( y + 1 ) ) ) )
343	342	xpeq1d	|- ( j = ( y + 1 ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) )
344		oveq1	|- ( j = ( y + 1 ) -> ( j + 1 ) = ( ( y + 1 ) + 1 ) )
345	344	oveq1d	|- ( j = ( y + 1 ) -> ( ( j + 1 ) ... N ) = ( ( ( y + 1 ) + 1 ) ... N ) )
346	345	imaeq2d	|- ( j = ( y + 1 ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
347	346	xpeq1d	|- ( j = ( y + 1 ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) )
348	343 347	uneq12d	|- ( j = ( y + 1 ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 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 } ) ) )
349	348	oveq2d	|- ( j = ( y + 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 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 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 } ) ) ) )
350	340 349	csbie	|- [_ ( y + 1 ) / j ]_ ( ( 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 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 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 } ) ) )
351	339 350	eqtrdi	|- ( y e. ( 0 ... ( N - 1 ) ) -> [_ if ( y < 0 , y , ( y + 1 ) ) / j ]_ ( ( 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 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 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 } ) ) ) )
352	351	mpteq2ia	|- ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < 0 , y , ( y + 1 ) ) / j ]_ ( ( 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 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) = ( 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 } ) ) ) )
353	332 352	eqtr4di	|- ( ph -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < 0 , y , ( y + 1 ) ) / j ]_ ( ( 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 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
354		opex	|- <. ( 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 ) ) ) ) >. e. _V
355	354 52	op2ndd	|- ( t = <. <. ( 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 ) ) ) ) >. , 0 >. -> ( 2nd ` t ) = 0 )
356	355	breq2d	|- ( t = <. <. ( 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 ) ) ) ) >. , 0 >. -> ( y < ( 2nd ` t ) <-> y < 0 ) )
357	356	ifbid	|- ( t = <. <. ( 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 ) ) ) ) >. , 0 >. -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < 0 , y , ( y + 1 ) ) )
358	354 52	op1std	|- ( t = <. <. ( 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 ) ) ) ) >. , 0 >. -> ( 1st ` t ) = <. ( 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 ) ) ) ) >. )
359	98	mptex	|- ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) ) ) e. _V
360	359 323	op1std	|- ( ( 1st ` t ) = <. ( 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 ) ) ) ) >. -> ( 1st ` ( 1st ` t ) ) = ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) ) ) )
361	358 360	syl	|- ( t = <. <. ( 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 ) ) ) ) >. , 0 >. -> ( 1st ` ( 1st ` t ) ) = ( n e. ( 1 ... N ) |-> ( ( ( 1st ` ( 1st ` T ) ) ` n ) - if ( n = ( ( 2nd ` ( 1st ` T ) ) ` N ) , 1 , 0 ) ) ) )
362	359 323	op2ndd	|- ( ( 1st ` t ) = <. ( 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 ) ) ) ) >. -> ( 2nd ` ( 1st ` t ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) )
363	358 362	syl	|- ( t = <. <. ( 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 ) ) ) ) >. , 0 >. -> ( 2nd ` ( 1st ` t ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) )
364	363	imaeq1d	|- ( t = <. <. ( 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 ) ) ) ) >. , 0 >. -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( 1 ... j ) ) )
365	364	xpeq1d	|- ( t = <. <. ( 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 ) ) ) ) >. , 0 >. -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) )
366	363	imaeq1d	|- ( t = <. <. ( 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 ) ) ) ) >. , 0 >. -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) )
367	366	xpeq1d	|- ( t = <. <. ( 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 ) ) ) ) >. , 0 >. -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
368	365 367	uneq12d	|- ( t = <. <. ( 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 ) ) ) ) >. , 0 >. -> ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
369	361 368	oveq12d	|- ( t = <. <. ( 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 ) ) ) ) >. , 0 >. -> ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 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 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
370	357 369	csbeq12dv	|- ( t = <. <. ( 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 ) ) ) ) >. , 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 } ) ) ) = [_ if ( y < 0 , y , ( y + 1 ) ) / j ]_ ( ( 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 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
371	370	mpteq2dv	|- ( t = <. <. ( 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 ) ) ) ) >. , 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 } ) ) ) ) = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < 0 , y , ( y + 1 ) ) / j ]_ ( ( 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 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
372	371	eqeq2d	|- ( t = <. <. ( 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 ) ) ) ) >. , 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 } ) ) ) ) <-> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < 0 , y , ( y + 1 ) ) / j ]_ ( ( 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 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
373	372 2	elrab2	|- ( <. <. ( 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 ) ) ) ) >. , 0 >. e. S <-> ( <. <. ( 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 ) ) ) ) >. , 0 >. 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 < 0 , y , ( y + 1 ) ) / j ]_ ( ( 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 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( n e. ( 1 ... N ) |-> if ( n = 1 , N , ( n - 1 ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
374	331 353 373	sylanbrc	|- ( ph -> <. <. ( 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 ) ) ) ) >. , 0 >. e. S )
375	354 52	op2ndd	|- ( T = <. <. ( 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 ) ) ) ) >. , 0 >. -> ( 2nd ` T ) = 0 )
376	375	eqcoms	|- ( <. <. ( 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 ) ) ) ) >. , 0 >. = T -> ( 2nd ` T ) = 0 )
377	1	nnne0d	|- ( ph -> N =/= 0 )
378	377	necomd	|- ( ph -> 0 =/= N )
379		neeq1	|- ( ( 2nd ` T ) = 0 -> ( ( 2nd ` T ) =/= N <-> 0 =/= N ) )
380	378 379	syl5ibrcom	|- ( ph -> ( ( 2nd ` T ) = 0 -> ( 2nd ` T ) =/= N ) )
381	376 380	syl5	|- ( ph -> ( <. <. ( 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 ) ) ) ) >. , 0 >. = T -> ( 2nd ` T ) =/= N ) )
382	381	necon2d	|- ( ph -> ( ( 2nd ` T ) = 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 ) ) ) ) >. , 0 >. =/= T ) )
383	6 382	mpd	|- ( ph -> <. <. ( 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 ) ) ) ) >. , 0 >. =/= T )
384		neeq1	|- ( z = <. <. ( 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 ) ) ) ) >. , 0 >. -> ( z =/= T <-> <. <. ( 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 ) ) ) ) >. , 0 >. =/= T ) )
385	384	rspcev	|- ( ( <. <. ( 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 ) ) ) ) >. , 0 >. e. S /\ <. <. ( 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 ) ) ) ) >. , 0 >. =/= T ) -> E. z e. S z =/= T )
386	374 383 385	syl2anc	|- ( ph -> E. z e. S z =/= T )