Theorem poimirlem15

Description: Lemma for poimir , that the face in poimirlem22 is a face. (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 )
	poimirlem15.3	|- ( ph -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
Assertion	poimirlem15	|- ( ph -> <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. e. S )

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		poimirlem15.3	|- ( ph -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
6		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 ) ) )
7	6 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 ) ) )
8	4 7	syl	|- ( ph -> T e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
9		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 ) } ) )
10		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 ) ) )
11	8 9 10	3syl	|- ( ph -> ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
12		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 ) } )
13	8 9 12	3syl	|- ( ph -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
14		fvex	|- ( 2nd ` ( 1st ` T ) ) e. _V
15		f1oeq1	|- ( f = ( 2nd ` ( 1st ` T ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
16	14 15	elab	|- ( ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
17	13 16	sylib	|- ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
18		elfznn	|- ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( 2nd ` T ) e. NN )
19	5 18	syl	|- ( ph -> ( 2nd ` T ) e. NN )
20	19	nnred	|- ( ph -> ( 2nd ` T ) e. RR )
21	20	ltp1d	|- ( ph -> ( 2nd ` T ) < ( ( 2nd ` T ) + 1 ) )
22	20 21	ltned	|- ( ph -> ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) )
23	22	necomd	|- ( ph -> ( ( 2nd ` T ) + 1 ) =/= ( 2nd ` T ) )
24		fvex	|- ( 2nd ` T ) e. _V
25		ovex	|- ( ( 2nd ` T ) + 1 ) e. _V
26		f1oprg	|- ( ( ( ( 2nd ` T ) e. _V /\ ( ( 2nd ` T ) + 1 ) e. _V ) /\ ( ( ( 2nd ` T ) + 1 ) e. _V /\ ( 2nd ` T ) e. _V ) ) -> ( ( ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) /\ ( ( 2nd ` T ) + 1 ) =/= ( 2nd ` T ) ) -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } ) )
27	24 25 25 24 26	mp4an	|- ( ( ( 2nd ` T ) =/= ( ( 2nd ` T ) + 1 ) /\ ( ( 2nd ` T ) + 1 ) =/= ( 2nd ` T ) ) -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } )
28	22 23 27	syl2anc	|- ( ph -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } )
29		prcom	|- { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } = { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) }
30		f1oeq3	|- ( { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } = { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } <-> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
31	29 30	ax-mp	|- ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } <-> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
32	28 31	sylib	|- ( ph -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
33		f1oi	|- ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) : ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -1-1-onto-> ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
34		disjdif	|- ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = (/)
35		f1oun	|- ( ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } /\ ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) : ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -1-1-onto-> ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) /\ ( ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = (/) /\ ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = (/) ) ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) : ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -1-1-onto-> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
36	34 34 35	mpanr12	|- ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } /\ ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) : ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -1-1-onto-> ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) : ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -1-1-onto-> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
37	32 33 36	sylancl	|- ( ph -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) : ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -1-1-onto-> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
38	1	nncnd	|- ( ph -> N e. CC )
39		npcan1	|- ( N e. CC -> ( ( N - 1 ) + 1 ) = N )
40	38 39	syl	|- ( ph -> ( ( N - 1 ) + 1 ) = N )
41	1	nnzd	|- ( ph -> N e. ZZ )
42		peano2zm	|- ( N e. ZZ -> ( N - 1 ) e. ZZ )
43	41 42	syl	|- ( ph -> ( N - 1 ) e. ZZ )
44		uzid	|- ( ( N - 1 ) e. ZZ -> ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
45		peano2uz	|- ( ( N - 1 ) e. ( ZZ>= ` ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
46	43 44 45	3syl	|- ( ph -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( N - 1 ) ) )
47	40 46	eqeltrrd	|- ( ph -> N e. ( ZZ>= ` ( N - 1 ) ) )
48		fzss2	|- ( N e. ( ZZ>= ` ( N - 1 ) ) -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
49	47 48	syl	|- ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 1 ... N ) )
50	49 5	sseldd	|- ( ph -> ( 2nd ` T ) e. ( 1 ... N ) )
51	19	peano2nnd	|- ( ph -> ( ( 2nd ` T ) + 1 ) e. NN )
52	43	zred	|- ( ph -> ( N - 1 ) e. RR )
53	1	nnred	|- ( ph -> N e. RR )
54		elfzle2	|- ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( 2nd ` T ) <_ ( N - 1 ) )
55	5 54	syl	|- ( ph -> ( 2nd ` T ) <_ ( N - 1 ) )
56	53	ltm1d	|- ( ph -> ( N - 1 ) < N )
57	20 52 53 55 56	lelttrd	|- ( ph -> ( 2nd ` T ) < N )
58	19	nnzd	|- ( ph -> ( 2nd ` T ) e. ZZ )
59		zltp1le	|- ( ( ( 2nd ` T ) e. ZZ /\ N e. ZZ ) -> ( ( 2nd ` T ) < N <-> ( ( 2nd ` T ) + 1 ) <_ N ) )
60	58 41 59	syl2anc	|- ( ph -> ( ( 2nd ` T ) < N <-> ( ( 2nd ` T ) + 1 ) <_ N ) )
61	57 60	mpbid	|- ( ph -> ( ( 2nd ` T ) + 1 ) <_ N )
62		fznn	|- ( N e. ZZ -> ( ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) <-> ( ( ( 2nd ` T ) + 1 ) e. NN /\ ( ( 2nd ` T ) + 1 ) <_ N ) ) )
63	41 62	syl	|- ( ph -> ( ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) <-> ( ( ( 2nd ` T ) + 1 ) e. NN /\ ( ( 2nd ` T ) + 1 ) <_ N ) ) )
64	51 61 63	mpbir2and	|- ( ph -> ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) )
65		prssi	|- ( ( ( 2nd ` T ) e. ( 1 ... N ) /\ ( ( 2nd ` T ) + 1 ) e. ( 1 ... N ) ) -> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... N ) )
66	50 64 65	syl2anc	|- ( ph -> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... N ) )
67		undif	|- ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... N ) <-> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( 1 ... N ) )
68	66 67	sylib	|- ( ph -> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( 1 ... N ) )
69		f1oeq23	|- ( ( ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( 1 ... N ) /\ ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( 1 ... N ) ) -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) : ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -1-1-onto-> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) <-> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
70	68 68 69	syl2anc	|- ( ph -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) : ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) -1-1-onto-> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) <-> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
71	37 70	mpbid	|- ( ph -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
72		f1oco	|- ( ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) /\ ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) -> ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
73	17 71 72	syl2anc	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
74		prex	|- { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } e. _V
75		ovex	|- ( 1 ... N ) e. _V
76		difexg	|- ( ( 1 ... N ) e. _V -> ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) e. _V )
77		resiexg	|- ( ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) e. _V -> ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) e. _V )
78	75 76 77	mp2b	|- ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) e. _V
79	74 78	unex	|- ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) e. _V
80	14 79	coex	|- ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) e. _V
81		f1oeq1	|- ( f = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
82	80 81	elab	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
83	73 82	sylibr	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
84		opelxpi	|- ( ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) /\ ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
85	11 83 84	syl2anc	|- ( ph -> <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
86		fz1ssfz0	|- ( 1 ... N ) C_ ( 0 ... N )
87	49 86	sstrdi	|- ( ph -> ( 1 ... ( N - 1 ) ) C_ ( 0 ... N ) )
88	87 5	sseldd	|- ( ph -> ( 2nd ` T ) e. ( 0 ... N ) )
89		opelxpi	|- ( ( <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) /\ ( 2nd ` T ) e. ( 0 ... N ) ) -> <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
90	85 88 89	syl2anc	|- ( ph -> <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. e. ( ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) X. ( 0 ... N ) ) )
91		fveq2	|- ( t = T -> ( 2nd ` t ) = ( 2nd ` T ) )
92	91	breq2d	|- ( t = T -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` T ) ) )
93	92	ifbid	|- ( t = T -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) )
94	93	csbeq1d	|- ( 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 } ) ) ) )
95		2fveq3	|- ( t = T -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) )
96		2fveq3	|- ( t = T -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` T ) ) )
97	96	imaeq1d	|- ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) )
98	97	xpeq1d	|- ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) )
99	96	imaeq1d	|- ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) )
100	99	xpeq1d	|- ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
101	98 100	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 } ) ) )
102	95 101	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 } ) ) ) )
103	102	csbeq2dv	|- ( 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 } ) ) ) )
104	94 103	eqtrd	|- ( 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 } ) ) ) )
105	104	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 } ) ) ) ) )
106	105	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 } ) ) ) ) ) )
107	106 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 } ) ) ) ) ) )
108	107	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 } ) ) ) ) )
109	4 108	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 } ) ) ) ) )
110		imaco	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... y ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( 1 ... y ) ) )
111		f1ofn	|- ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } Fn { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
112	28 111	syl	|- ( ph -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } Fn { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
113	112	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } Fn { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
114		incom	|- ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( 1 ... y ) ) = ( ( 1 ... y ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
115		elfznn0	|- ( y e. ( 0 ... ( N - 1 ) ) -> y e. NN0 )
116	115	nn0red	|- ( y e. ( 0 ... ( N - 1 ) ) -> y e. RR )
117		ltnle	|- ( ( y e. RR /\ ( 2nd ` T ) e. RR ) -> ( y < ( 2nd ` T ) <-> -. ( 2nd ` T ) <_ y ) )
118	116 20 117	syl2anr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( y < ( 2nd ` T ) <-> -. ( 2nd ` T ) <_ y ) )
119	118	biimpa	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> -. ( 2nd ` T ) <_ y )
120		elfzle2	|- ( ( 2nd ` T ) e. ( 1 ... y ) -> ( 2nd ` T ) <_ y )
121	119 120	nsyl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> -. ( 2nd ` T ) e. ( 1 ... y ) )
122		disjsn	|- ( ( ( 1 ... y ) i^i { ( 2nd ` T ) } ) = (/) <-> -. ( 2nd ` T ) e. ( 1 ... y ) )
123	121 122	sylibr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( 1 ... y ) i^i { ( 2nd ` T ) } ) = (/) )
124	116	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> y e. RR )
125	20	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( 2nd ` T ) e. RR )
126	51	nnred	|- ( ph -> ( ( 2nd ` T ) + 1 ) e. RR )
127	126	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( 2nd ` T ) + 1 ) e. RR )
128		simpr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> y < ( 2nd ` T ) )
129	21	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( 2nd ` T ) < ( ( 2nd ` T ) + 1 ) )
130	124 125 127 128 129	lttrd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> y < ( ( 2nd ` T ) + 1 ) )
131		ltnle	|- ( ( y e. RR /\ ( ( 2nd ` T ) + 1 ) e. RR ) -> ( y < ( ( 2nd ` T ) + 1 ) <-> -. ( ( 2nd ` T ) + 1 ) <_ y ) )
132	116 126 131	syl2anr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( y < ( ( 2nd ` T ) + 1 ) <-> -. ( ( 2nd ` T ) + 1 ) <_ y ) )
133	132	adantr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( y < ( ( 2nd ` T ) + 1 ) <-> -. ( ( 2nd ` T ) + 1 ) <_ y ) )
134	130 133	mpbid	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> -. ( ( 2nd ` T ) + 1 ) <_ y )
135		elfzle2	|- ( ( ( 2nd ` T ) + 1 ) e. ( 1 ... y ) -> ( ( 2nd ` T ) + 1 ) <_ y )
136	134 135	nsyl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> -. ( ( 2nd ` T ) + 1 ) e. ( 1 ... y ) )
137		disjsn	|- ( ( ( 1 ... y ) i^i { ( ( 2nd ` T ) + 1 ) } ) = (/) <-> -. ( ( 2nd ` T ) + 1 ) e. ( 1 ... y ) )
138	136 137	sylibr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( 1 ... y ) i^i { ( ( 2nd ` T ) + 1 ) } ) = (/) )
139	123 138	uneq12d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( ( 1 ... y ) i^i { ( 2nd ` T ) } ) u. ( ( 1 ... y ) i^i { ( ( 2nd ` T ) + 1 ) } ) ) = ( (/) u. (/) ) )
140		df-pr	|- { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } = ( { ( 2nd ` T ) } u. { ( ( 2nd ` T ) + 1 ) } )
141	140	ineq2i	|- ( ( 1 ... y ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( 1 ... y ) i^i ( { ( 2nd ` T ) } u. { ( ( 2nd ` T ) + 1 ) } ) )
142		indi	|- ( ( 1 ... y ) i^i ( { ( 2nd ` T ) } u. { ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( 1 ... y ) i^i { ( 2nd ` T ) } ) u. ( ( 1 ... y ) i^i { ( ( 2nd ` T ) + 1 ) } ) )
143	141 142	eqtr2i	|- ( ( ( 1 ... y ) i^i { ( 2nd ` T ) } ) u. ( ( 1 ... y ) i^i { ( ( 2nd ` T ) + 1 ) } ) ) = ( ( 1 ... y ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
144		un0	|- ( (/) u. (/) ) = (/)
145	139 143 144	3eqtr3g	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( 1 ... y ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) )
146	114 145	syl5eq	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( 1 ... y ) ) = (/) )
147		fnimadisj	|- ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } Fn { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } /\ ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( 1 ... y ) ) = (/) ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( 1 ... y ) ) = (/) )
148	113 146 147	syl2anc	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( 1 ... y ) ) = (/) )
149	40	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) = N )
150		elfzuz3	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( N - 1 ) e. ( ZZ>= ` y ) )
151		peano2uz	|- ( ( N - 1 ) e. ( ZZ>= ` y ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` y ) )
152	150 151	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` y ) )
153	152	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` y ) )
154	149 153	eqeltrrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ZZ>= ` y ) )
155		fzss2	|- ( N e. ( ZZ>= ` y ) -> ( 1 ... y ) C_ ( 1 ... N ) )
156		reldisj	|- ( ( 1 ... y ) C_ ( 1 ... N ) -> ( ( ( 1 ... y ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) <-> ( 1 ... y ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
157	154 155 156	3syl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 1 ... y ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) <-> ( 1 ... y ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
158	157	adantr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( ( 1 ... y ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) <-> ( 1 ... y ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
159	145 158	mpbid	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( 1 ... y ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
160		resiima	|- ( ( 1 ... y ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( 1 ... y ) ) = ( 1 ... y ) )
161	159 160	syl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( 1 ... y ) ) = ( 1 ... y ) )
162	148 161	uneq12d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( 1 ... y ) ) u. ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( 1 ... y ) ) ) = ( (/) u. ( 1 ... y ) ) )
163		imaundir	|- ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( 1 ... y ) ) = ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( 1 ... y ) ) u. ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( 1 ... y ) ) )
164		uncom	|- ( (/) u. ( 1 ... y ) ) = ( ( 1 ... y ) u. (/) )
165		un0	|- ( ( 1 ... y ) u. (/) ) = ( 1 ... y )
166	164 165	eqtr2i	|- ( 1 ... y ) = ( (/) u. ( 1 ... y ) )
167	162 163 166	3eqtr4g	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( 1 ... y ) ) = ( 1 ... y ) )
168	167	imaeq2d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( 1 ... y ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) )
169	110 168	syl5eq	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... y ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) )
170	169	xpeq1d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) )
171		imaco	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( y + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( ( y + 1 ) ... N ) ) )
172		imaundir	|- ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( ( y + 1 ) ... N ) ) = ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( y + 1 ) ... N ) ) u. ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( y + 1 ) ... N ) ) )
173		imassrn	|- ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( y + 1 ) ... N ) ) C_ ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. }
174	173	a1i	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( y + 1 ) ... N ) ) C_ ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } )
175		fnima	|- ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } Fn { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } )
176	28 111 175	3syl	|- ( ph -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } )
177	176	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } )
178		elfzelz	|- ( y e. ( 0 ... ( N - 1 ) ) -> y e. ZZ )
179		zltp1le	|- ( ( y e. ZZ /\ ( 2nd ` T ) e. ZZ ) -> ( y < ( 2nd ` T ) <-> ( y + 1 ) <_ ( 2nd ` T ) ) )
180	178 58 179	syl2anr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( y < ( 2nd ` T ) <-> ( y + 1 ) <_ ( 2nd ` T ) ) )
181	180	biimpa	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( y + 1 ) <_ ( 2nd ` T ) )
182	20 53 57	ltled	|- ( ph -> ( 2nd ` T ) <_ N )
183	182	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( 2nd ` T ) <_ N )
184	58	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 2nd ` T ) e. ZZ )
185		nn0p1nn	|- ( y e. NN0 -> ( y + 1 ) e. NN )
186	115 185	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. NN )
187	186	nnzd	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. ZZ )
188	187	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( y + 1 ) e. ZZ )
189	41	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. ZZ )
190		elfz	|- ( ( ( 2nd ` T ) e. ZZ /\ ( y + 1 ) e. ZZ /\ N e. ZZ ) -> ( ( 2nd ` T ) e. ( ( y + 1 ) ... N ) <-> ( ( y + 1 ) <_ ( 2nd ` T ) /\ ( 2nd ` T ) <_ N ) ) )
191	184 188 189 190	syl3anc	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) e. ( ( y + 1 ) ... N ) <-> ( ( y + 1 ) <_ ( 2nd ` T ) /\ ( 2nd ` T ) <_ N ) ) )
192	191	adantr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( 2nd ` T ) e. ( ( y + 1 ) ... N ) <-> ( ( y + 1 ) <_ ( 2nd ` T ) /\ ( 2nd ` T ) <_ N ) ) )
193	181 183 192	mpbir2and	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( 2nd ` T ) e. ( ( y + 1 ) ... N ) )
194		1red	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> 1 e. RR )
195		ltle	|- ( ( y e. RR /\ ( 2nd ` T ) e. RR ) -> ( y < ( 2nd ` T ) -> y <_ ( 2nd ` T ) ) )
196	116 20 195	syl2anr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( y < ( 2nd ` T ) -> y <_ ( 2nd ` T ) ) )
197	196	imp	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> y <_ ( 2nd ` T ) )
198	124 125 194 197	leadd1dd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( y + 1 ) <_ ( ( 2nd ` T ) + 1 ) )
199	61	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( 2nd ` T ) + 1 ) <_ N )
200	58	peano2zd	|- ( ph -> ( ( 2nd ` T ) + 1 ) e. ZZ )
201	200	adantr	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) + 1 ) e. ZZ )
202		elfz	|- ( ( ( ( 2nd ` T ) + 1 ) e. ZZ /\ ( y + 1 ) e. ZZ /\ N e. ZZ ) -> ( ( ( 2nd ` T ) + 1 ) e. ( ( y + 1 ) ... N ) <-> ( ( y + 1 ) <_ ( ( 2nd ` T ) + 1 ) /\ ( ( 2nd ` T ) + 1 ) <_ N ) ) )
203	201 188 189 202	syl3anc	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` T ) + 1 ) e. ( ( y + 1 ) ... N ) <-> ( ( y + 1 ) <_ ( ( 2nd ` T ) + 1 ) /\ ( ( 2nd ` T ) + 1 ) <_ N ) ) )
204	203	adantr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( ( 2nd ` T ) + 1 ) e. ( ( y + 1 ) ... N ) <-> ( ( y + 1 ) <_ ( ( 2nd ` T ) + 1 ) /\ ( ( 2nd ` T ) + 1 ) <_ N ) ) )
205	198 199 204	mpbir2and	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( 2nd ` T ) + 1 ) e. ( ( y + 1 ) ... N ) )
206		prssi	|- ( ( ( 2nd ` T ) e. ( ( y + 1 ) ... N ) /\ ( ( 2nd ` T ) + 1 ) e. ( ( y + 1 ) ... N ) ) -> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( ( y + 1 ) ... N ) )
207	193 205 206	syl2anc	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( ( y + 1 ) ... N ) )
208		imass2	|- ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( ( y + 1 ) ... N ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( y + 1 ) ... N ) ) )
209	207 208	syl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( y + 1 ) ... N ) ) )
210	177 209	eqsstrrd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } C_ ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( y + 1 ) ... N ) ) )
211	174 210	eqssd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( y + 1 ) ... N ) ) = ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } )
212		f1ofo	|- ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -1-1-onto-> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -onto-> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } )
213		forn	|- ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } : { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } -onto-> { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } -> ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } = { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } )
214	28 212 213	3syl	|- ( ph -> ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } = { ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) } )
215	214 29	eqtrdi	|- ( ph -> ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } = { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
216	215	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } = { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
217	211 216	eqtrd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( y + 1 ) ... N ) ) = { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
218		undif	|- ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( ( y + 1 ) ... N ) <-> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( y + 1 ) ... N ) )
219	207 218	sylib	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( y + 1 ) ... N ) )
220	219	imaeq2d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( y + 1 ) ... N ) ) )
221		fnresi	|- ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) Fn ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
222		incom	|- ( ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
223	222 34	eqtri	|- ( ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/)
224		fnimadisj	|- ( ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) Fn ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) /\ ( ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) )
225	221 223 224	mp2an	|- ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/)
226	225	a1i	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) )
227		nnuz	|- NN = ( ZZ>= ` 1 )
228	186 227	eleqtrdi	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. ( ZZ>= ` 1 ) )
229		fzss1	|- ( ( y + 1 ) e. ( ZZ>= ` 1 ) -> ( ( y + 1 ) ... N ) C_ ( 1 ... N ) )
230	228 229	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) ... N ) C_ ( 1 ... N ) )
231	230	ssdifd	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
232		resiima	|- ( ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
233	231 232	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
234	233	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
235	226 234	uneq12d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( (/) u. ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
236		imaundi	|- ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
237		uncom	|- ( (/) u. ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. (/) )
238		un0	|- ( ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. (/) ) = ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
239	237 238	eqtr2i	|- ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( (/) u. ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
240	235 236 239	3eqtr4g	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
241	220 240	eqtr3d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( y + 1 ) ... N ) ) = ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
242	217 241	uneq12d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( y + 1 ) ... N ) ) u. ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( y + 1 ) ... N ) ) ) = ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
243	172 242	syl5eq	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( ( y + 1 ) ... N ) ) = ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
244	243 219	eqtrd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( ( y + 1 ) ... N ) ) = ( ( y + 1 ) ... N ) )
245	244	imaeq2d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( ( y + 1 ) ... N ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) )
246	171 245	syl5eq	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( y + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) )
247	246	xpeq1d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) )
248	170 247	uneq12d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) )
249	248	oveq2d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) )
250		iftrue	|- ( y < ( 2nd ` T ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = y )
251	250	csbeq1d	|- ( y < ( 2nd ` T ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ y / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
252		vex	|- y e. _V
253		oveq2	|- ( j = y -> ( 1 ... j ) = ( 1 ... y ) )
254	253	imaeq2d	|- ( j = y -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... y ) ) )
255	254	xpeq1d	|- ( j = y -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) )
256		oveq1	|- ( j = y -> ( j + 1 ) = ( y + 1 ) )
257	256	oveq1d	|- ( j = y -> ( ( j + 1 ) ... N ) = ( ( y + 1 ) ... N ) )
258	257	imaeq2d	|- ( j = y -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( y + 1 ) ... N ) ) )
259	258	xpeq1d	|- ( j = y -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) )
260	255 259	uneq12d	|- ( j = y -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) )
261	260	oveq2d	|- ( j = y -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) )
262	252 261	csbie	|- [_ y / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) )
263	251 262	eqtrdi	|- ( y < ( 2nd ` T ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) )
264	263	adantl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) )
265	250	csbeq1d	|- ( y < ( 2nd ` 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 } ) ) ) = [_ y / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
266	253	imaeq2d	|- ( j = y -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) )
267	266	xpeq1d	|- ( j = y -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) )
268	257	imaeq2d	|- ( j = y -> ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) )
269	268	xpeq1d	|- ( j = y -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) )
270	267 269	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 } ) ) )
271	270	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 } ) ) ) )
272	252 271	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 } ) ) )
273	265 272	eqtrdi	|- ( y < ( 2nd ` 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 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) )
274	273	adantl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` 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 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) ) ) )
275	249 264 274	3eqtr4d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( 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 } ) ) ) )
276		lenlt	|- ( ( ( 2nd ` T ) e. RR /\ y e. RR ) -> ( ( 2nd ` T ) <_ y <-> -. y < ( 2nd ` T ) ) )
277	20 116 276	syl2an	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) <_ y <-> -. y < ( 2nd ` T ) ) )
278	277	biimpar	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < ( 2nd ` T ) ) -> ( 2nd ` T ) <_ y )
279		imaco	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... ( y + 1 ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( 1 ... ( y + 1 ) ) ) )
280		imaundir	|- ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( 1 ... ( y + 1 ) ) ) = ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( 1 ... ( y + 1 ) ) ) u. ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( 1 ... ( y + 1 ) ) ) )
281		imassrn	|- ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( 1 ... ( y + 1 ) ) ) C_ ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. }
282	281	a1i	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( 1 ... ( y + 1 ) ) ) C_ ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } )
283	176	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } )
284	19	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) e. NN )
285	20	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) e. RR )
286	116	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> y e. RR )
287	186	nnred	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. RR )
288	287	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( y + 1 ) e. RR )
289		simpr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) <_ y )
290	116	lep1d	|- ( y e. ( 0 ... ( N - 1 ) ) -> y <_ ( y + 1 ) )
291	290	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> y <_ ( y + 1 ) )
292	285 286 288 289 291	letrd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) <_ ( y + 1 ) )
293		fznn	|- ( ( y + 1 ) e. ZZ -> ( ( 2nd ` T ) e. ( 1 ... ( y + 1 ) ) <-> ( ( 2nd ` T ) e. NN /\ ( 2nd ` T ) <_ ( y + 1 ) ) ) )
294	187 293	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( 2nd ` T ) e. ( 1 ... ( y + 1 ) ) <-> ( ( 2nd ` T ) e. NN /\ ( 2nd ` T ) <_ ( y + 1 ) ) ) )
295	294	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) e. ( 1 ... ( y + 1 ) ) <-> ( ( 2nd ` T ) e. NN /\ ( 2nd ` T ) <_ ( y + 1 ) ) ) )
296	284 292 295	mpbir2and	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) e. ( 1 ... ( y + 1 ) ) )
297	51	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) + 1 ) e. NN )
298		1red	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> 1 e. RR )
299	285 286 298 289	leadd1dd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) + 1 ) <_ ( y + 1 ) )
300		fznn	|- ( ( y + 1 ) e. ZZ -> ( ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( y + 1 ) ) <-> ( ( ( 2nd ` T ) + 1 ) e. NN /\ ( ( 2nd ` T ) + 1 ) <_ ( y + 1 ) ) ) )
301	187 300	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( y + 1 ) ) <-> ( ( ( 2nd ` T ) + 1 ) e. NN /\ ( ( 2nd ` T ) + 1 ) <_ ( y + 1 ) ) ) )
302	301	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( y + 1 ) ) <-> ( ( ( 2nd ` T ) + 1 ) e. NN /\ ( ( 2nd ` T ) + 1 ) <_ ( y + 1 ) ) ) )
303	297 299 302	mpbir2and	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( y + 1 ) ) )
304		prssi	|- ( ( ( 2nd ` T ) e. ( 1 ... ( y + 1 ) ) /\ ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( y + 1 ) ) ) -> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... ( y + 1 ) ) )
305	296 303 304	syl2anc	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... ( y + 1 ) ) )
306		imass2	|- ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... ( y + 1 ) ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( 1 ... ( y + 1 ) ) ) )
307	305 306	syl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( 1 ... ( y + 1 ) ) ) )
308	283 307	eqsstrrd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } C_ ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( 1 ... ( y + 1 ) ) ) )
309	282 308	eqssd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( 1 ... ( y + 1 ) ) ) = ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } )
310	215	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ran { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } = { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
311	309 310	eqtrd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( 1 ... ( y + 1 ) ) ) = { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
312		undif	|- ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... ( y + 1 ) ) <-> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( 1 ... ( y + 1 ) ) )
313	305 312	sylib	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( 1 ... ( y + 1 ) ) )
314	313	imaeq2d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( 1 ... ( y + 1 ) ) ) )
315	225	a1i	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) )
316		eluzp1p1	|- ( ( N - 1 ) e. ( ZZ>= ` y ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
317	150 316	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
318	317	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
319	149 318	eqeltrrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ZZ>= ` ( y + 1 ) ) )
320		fzss2	|- ( N e. ( ZZ>= ` ( y + 1 ) ) -> ( 1 ... ( y + 1 ) ) C_ ( 1 ... N ) )
321	319 320	syl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ... ( y + 1 ) ) C_ ( 1 ... N ) )
322	321	ssdifd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
323	322	adantr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
324		resiima	|- ( ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
325	323 324	syl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
326	315 325	uneq12d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( (/) u. ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
327		imaundi	|- ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
328		uncom	|- ( (/) u. ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. (/) )
329		un0	|- ( ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. (/) ) = ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
330	328 329	eqtr2i	|- ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( (/) u. ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
331	326 327 330	3eqtr4g	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) = ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
332	314 331	eqtr3d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( 1 ... ( y + 1 ) ) ) = ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
333	311 332	uneq12d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( 1 ... ( y + 1 ) ) ) u. ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( 1 ... ( y + 1 ) ) ) ) = ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
334	280 333	syl5eq	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( 1 ... ( y + 1 ) ) ) = ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } u. ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
335	334 313	eqtrd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( 1 ... ( y + 1 ) ) ) = ( 1 ... ( y + 1 ) ) )
336	335	imaeq2d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( 1 ... ( y + 1 ) ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) )
337	279 336	syl5eq	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... ( y + 1 ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) )
338	337	xpeq1d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) )
339		imaco	|- ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
340	112	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } Fn { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
341		incom	|- ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( ( ( y + 1 ) + 1 ) ... N ) ) = ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
342	126	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) + 1 ) e. RR )
343	186	peano2nnd	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) + 1 ) e. NN )
344	343	nnred	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) + 1 ) e. RR )
345	344	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( y + 1 ) + 1 ) e. RR )
346	21	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) < ( ( 2nd ` T ) + 1 ) )
347	116	ltp1d	|- ( y e. ( 0 ... ( N - 1 ) ) -> y < ( y + 1 ) )
348	347	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> y < ( y + 1 ) )
349	285 286 288 289 348	lelttrd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) < ( y + 1 ) )
350	285 288 298 349	ltadd1dd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) + 1 ) < ( ( y + 1 ) + 1 ) )
351	285 342 345 346 350	lttrd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) < ( ( y + 1 ) + 1 ) )
352		ltnle	|- ( ( ( 2nd ` T ) e. RR /\ ( ( y + 1 ) + 1 ) e. RR ) -> ( ( 2nd ` T ) < ( ( y + 1 ) + 1 ) <-> -. ( ( y + 1 ) + 1 ) <_ ( 2nd ` T ) ) )
353	20 344 352	syl2an	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) < ( ( y + 1 ) + 1 ) <-> -. ( ( y + 1 ) + 1 ) <_ ( 2nd ` T ) ) )
354	353	adantr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) < ( ( y + 1 ) + 1 ) <-> -. ( ( y + 1 ) + 1 ) <_ ( 2nd ` T ) ) )
355	351 354	mpbid	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> -. ( ( y + 1 ) + 1 ) <_ ( 2nd ` T ) )
356		elfzle1	|- ( ( 2nd ` T ) e. ( ( ( y + 1 ) + 1 ) ... N ) -> ( ( y + 1 ) + 1 ) <_ ( 2nd ` T ) )
357	355 356	nsyl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> -. ( 2nd ` T ) e. ( ( ( y + 1 ) + 1 ) ... N ) )
358		disjsn	|- ( ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) } ) = (/) <-> -. ( 2nd ` T ) e. ( ( ( y + 1 ) + 1 ) ... N ) )
359	357 358	sylibr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) } ) = (/) )
360		ltnle	|- ( ( ( ( 2nd ` T ) + 1 ) e. RR /\ ( ( y + 1 ) + 1 ) e. RR ) -> ( ( ( 2nd ` T ) + 1 ) < ( ( y + 1 ) + 1 ) <-> -. ( ( y + 1 ) + 1 ) <_ ( ( 2nd ` T ) + 1 ) ) )
361	126 344 360	syl2an	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` T ) + 1 ) < ( ( y + 1 ) + 1 ) <-> -. ( ( y + 1 ) + 1 ) <_ ( ( 2nd ` T ) + 1 ) ) )
362	361	adantr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( 2nd ` T ) + 1 ) < ( ( y + 1 ) + 1 ) <-> -. ( ( y + 1 ) + 1 ) <_ ( ( 2nd ` T ) + 1 ) ) )
363	350 362	mpbid	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> -. ( ( y + 1 ) + 1 ) <_ ( ( 2nd ` T ) + 1 ) )
364		elfzle1	|- ( ( ( 2nd ` T ) + 1 ) e. ( ( ( y + 1 ) + 1 ) ... N ) -> ( ( y + 1 ) + 1 ) <_ ( ( 2nd ` T ) + 1 ) )
365	363 364	nsyl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> -. ( ( 2nd ` T ) + 1 ) e. ( ( ( y + 1 ) + 1 ) ... N ) )
366		disjsn	|- ( ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( ( 2nd ` T ) + 1 ) } ) = (/) <-> -. ( ( 2nd ` T ) + 1 ) e. ( ( ( y + 1 ) + 1 ) ... N ) )
367	365 366	sylibr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( ( 2nd ` T ) + 1 ) } ) = (/) )
368	359 367	uneq12d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) } ) u. ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( ( 2nd ` T ) + 1 ) } ) ) = ( (/) u. (/) ) )
369	140	ineq2i	|- ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( ( ( ( y + 1 ) + 1 ) ... N ) i^i ( { ( 2nd ` T ) } u. { ( ( 2nd ` T ) + 1 ) } ) )
370		indi	|- ( ( ( ( y + 1 ) + 1 ) ... N ) i^i ( { ( 2nd ` T ) } u. { ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) } ) u. ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( ( 2nd ` T ) + 1 ) } ) )
371	369 370	eqtr2i	|- ( ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) } ) u. ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
372	368 371 144	3eqtr3g	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) )
373	341 372	syl5eq	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( ( ( y + 1 ) + 1 ) ... N ) ) = (/) )
374		fnimadisj	|- ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } Fn { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } /\ ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( ( ( y + 1 ) + 1 ) ... N ) ) = (/) ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( ( y + 1 ) + 1 ) ... N ) ) = (/) )
375	340 373 374	syl2anc	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( ( y + 1 ) + 1 ) ... N ) ) = (/) )
376	343 227	eleqtrdi	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
377		fzss1	|- ( ( ( y + 1 ) + 1 ) e. ( ZZ>= ` 1 ) -> ( ( ( y + 1 ) + 1 ) ... N ) C_ ( 1 ... N ) )
378		reldisj	|- ( ( ( ( y + 1 ) + 1 ) ... N ) C_ ( 1 ... N ) -> ( ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) <-> ( ( ( y + 1 ) + 1 ) ... N ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
379	376 377 378	3syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) <-> ( ( ( y + 1 ) + 1 ) ... N ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
380	379	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) <-> ( ( ( y + 1 ) + 1 ) ... N ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) )
381	372 380	mpbid	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( y + 1 ) + 1 ) ... N ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
382		resiima	|- ( ( ( ( y + 1 ) + 1 ) ... N ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) = ( ( ( y + 1 ) + 1 ) ... N ) )
383	381 382	syl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) = ( ( ( y + 1 ) + 1 ) ... N ) )
384	375 383	uneq12d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( ( y + 1 ) + 1 ) ... N ) ) u. ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( (/) u. ( ( ( y + 1 ) + 1 ) ... N ) ) )
385		imaundir	|- ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) = ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( ( y + 1 ) + 1 ) ... N ) ) u. ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
386		uncom	|- ( (/) u. ( ( ( y + 1 ) + 1 ) ... N ) ) = ( ( ( ( y + 1 ) + 1 ) ... N ) u. (/) )
387		un0	|- ( ( ( ( y + 1 ) + 1 ) ... N ) u. (/) ) = ( ( ( y + 1 ) + 1 ) ... N )
388	386 387	eqtr2i	|- ( ( ( y + 1 ) + 1 ) ... N ) = ( (/) u. ( ( ( y + 1 ) + 1 ) ... N ) )
389	384 385 388	3eqtr4g	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) = ( ( ( y + 1 ) + 1 ) ... N ) )
390	389	imaeq2d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
391	339 390	syl5eq	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
392	391	xpeq1d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) )
393	338 392	uneq12d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
394	278 393	syldan	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < ( 2nd ` T ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
395	394	oveq2d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < ( 2nd ` T ) ) -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
396		iffalse	|- ( -. y < ( 2nd ` T ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = ( y + 1 ) )
397	396	csbeq1d	|- ( -. y < ( 2nd ` T ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = [_ ( y + 1 ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
398		ovex	|- ( y + 1 ) e. _V
399		oveq2	|- ( j = ( y + 1 ) -> ( 1 ... j ) = ( 1 ... ( y + 1 ) ) )
400	399	imaeq2d	|- ( j = ( y + 1 ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... ( y + 1 ) ) ) )
401	400	xpeq1d	|- ( j = ( y + 1 ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) )
402		oveq1	|- ( j = ( y + 1 ) -> ( j + 1 ) = ( ( y + 1 ) + 1 ) )
403	402	oveq1d	|- ( j = ( y + 1 ) -> ( ( j + 1 ) ... N ) = ( ( ( y + 1 ) + 1 ) ... N ) )
404	403	imaeq2d	|- ( j = ( y + 1 ) -> ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
405	404	xpeq1d	|- ( j = ( y + 1 ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) )
406	401 405	uneq12d	|- ( j = ( y + 1 ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
407	406	oveq2d	|- ( j = ( y + 1 ) -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
408	398 407	csbie	|- [_ ( y + 1 ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
409	397 408	eqtrdi	|- ( -. y < ( 2nd ` T ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
410	409	adantl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < ( 2nd ` T ) ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
411	396	csbeq1d	|- ( -. y < ( 2nd ` 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 } ) ) ) = [_ ( y + 1 ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
412	399	imaeq2d	|- ( j = ( y + 1 ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) )
413	412	xpeq1d	|- ( j = ( y + 1 ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) )
414	403	imaeq2d	|- ( j = ( y + 1 ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
415	414	xpeq1d	|- ( j = ( y + 1 ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) )
416	413 415	uneq12d	|- ( j = ( y + 1 ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
417	416	oveq2d	|- ( j = ( y + 1 ) -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
418	398 417	csbie	|- [_ ( y + 1 ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) )
419	411 418	eqtrdi	|- ( -. y < ( 2nd ` 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 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
420	419	adantl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < ( 2nd ` 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 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) ) ) )
421	395 410 420	3eqtr4d	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < ( 2nd ` T ) ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( 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 } ) ) ) )
422	275 421	pm2.61dan	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( 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 } ) ) ) )
423	422	mpteq2dva	|- ( ph -> ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( 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 } ) ) ) ) )
424	109 423	eqtr4d	|- ( ph -> F = ( y e. ( 0 ... ( N - 1 ) ) |-> [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
425		opex	|- <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. e. _V
426	425 24	op1std	|- ( t = <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. -> ( 1st ` t ) = <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. )
427	425 24	op2ndd	|- ( t = <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. -> ( 2nd ` t ) = ( 2nd ` T ) )
428		breq2	|- ( ( 2nd ` t ) = ( 2nd ` T ) -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` T ) ) )
429	428	ifbid	|- ( ( 2nd ` t ) = ( 2nd ` T ) -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) )
430	429	csbeq1d	|- ( ( 2nd ` t ) = ( 2nd ` 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 } ) ) ) )
431		fvex	|- ( 1st ` ( 1st ` T ) ) e. _V
432	431 80	op1std	|- ( ( 1st ` t ) = <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) )
433	431 80	op2ndd	|- ( ( 1st ` t ) = <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. -> ( 2nd ` ( 1st ` t ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) )
434		id	|- ( ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) )
435		imaeq1	|- ( ( 2nd ` ( 1st ` t ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) )
436	435	xpeq1d	|- ( ( 2nd ` ( 1st ` t ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) )
437		imaeq1	|- ( ( 2nd ` ( 1st ` t ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) )
438	437	xpeq1d	|- ( ( 2nd ` ( 1st ` t ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
439	436 438	uneq12d	|- ( ( 2nd ` ( 1st ` t ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) -> ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) )
440	434 439	oveqan12d	|- ( ( ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) /\ ( 2nd ` ( 1st ` t ) ) = ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) ) -> ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
441	432 433 440	syl2anc	|- ( ( 1st ` t ) = <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. -> ( ( 1st ` ( 1st ` t ) ) oF + ( ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
442	441	csbeq2dv	|- ( ( 1st ` t ) = <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 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 } ) ) ) = [_ if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
443	430 442	sylan9eqr	|- ( ( ( 1st ` t ) = <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. /\ ( 2nd ` t ) = ( 2nd ` 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 ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
444	426 427 443	syl2anc	|- ( t = <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` 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 ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
445	444	mpteq2dv	|- ( t = <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` 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 ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) )
446	445	eqeq2d	|- ( t = <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` 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 ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
447	446 2	elrab2	|- ( <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. e. S <-> ( <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` 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 ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) ) ) )
448	90 424 447	sylanbrc	|- ( ph -> <. <. ( 1st ` ( 1st ` T ) ) , ( ( 2nd ` ( 1st ` T ) ) o. ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } u. ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) ) ) >. , ( 2nd ` T ) >. e. S )