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	eqtrid	|- ( ( ( 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	eqtrid	|- ( ( ( 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		disjdifr	|- ( ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/)
223		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 ) } ) = (/) )
224	221 222 223	mp2an	|- ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/)
225	224	a1i	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ y < ( 2nd ` T ) ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) )
226		nnuz	|- NN = ( ZZ>= ` 1 )
227	186 226	eleqtrdi	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. ( ZZ>= ` 1 ) )
228		fzss1	|- ( ( y + 1 ) e. ( ZZ>= ` 1 ) -> ( ( y + 1 ) ... N ) C_ ( 1 ... N ) )
229	227 228	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) ... N ) C_ ( 1 ... N ) )
230	229	ssdifd	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
231		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 ) } ) )
232	230 231	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 ) } ) )
233	232	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 ) } ) )
234	225 233	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 ) } ) ) )
235		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 ) } ) ) )
236		uncom	|- ( (/) u. ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. (/) )
237		un0	|- ( ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. (/) ) = ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
238	236 237	eqtr2i	|- ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( (/) u. ( ( ( y + 1 ) ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
239	234 235 238	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 ) } ) )
240	220 239	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 ) } ) )
241	217 240	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 ) } ) ) )
242	172 241	eqtrid	|- ( ( ( 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 ) } ) ) )
243	242 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 ) )
244	243	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 ) ) )
245	171 244	eqtrid	|- ( ( ( 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 ) ) )
246	245	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 } ) )
247	170 246	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 } ) ) )
248	247	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 } ) ) ) )
249		iftrue	|- ( y < ( 2nd ` T ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = y )
250	249	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 } ) ) ) )
251		vex	|- y e. _V
252		oveq2	|- ( j = y -> ( 1 ... j ) = ( 1 ... y ) )
253	252	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 ) ) )
254	253	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 } ) )
255		oveq1	|- ( j = y -> ( j + 1 ) = ( y + 1 ) )
256	255	oveq1d	|- ( j = y -> ( ( j + 1 ) ... N ) = ( ( y + 1 ) ... N ) )
257	256	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 ) ) )
258	257	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 } ) )
259	254 258	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 } ) ) )
260	259	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 } ) ) ) )
261	251 260	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 } ) ) )
262	250 261	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 } ) ) ) )
263	262	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 } ) ) ) )
264	249	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 } ) ) ) )
265	252	imaeq2d	|- ( j = y -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) )
266	265	xpeq1d	|- ( j = y -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... y ) ) X. { 1 } ) )
267	256	imaeq2d	|- ( j = y -> ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) )
268	267	xpeq1d	|- ( j = y -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( y + 1 ) ... N ) ) X. { 0 } ) )
269	266 268	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 } ) ) )
270	269	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 } ) ) ) )
271	251 270	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 } ) ) )
272	264 271	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 } ) ) ) )
273	272	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 } ) ) ) )
274	248 263 273	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 } ) ) ) )
275		lenlt	|- ( ( ( 2nd ` T ) e. RR /\ y e. RR ) -> ( ( 2nd ` T ) <_ y <-> -. y < ( 2nd ` T ) ) )
276	20 116 275	syl2an	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) <_ y <-> -. y < ( 2nd ` T ) ) )
277	276	biimpar	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ -. y < ( 2nd ` T ) ) -> ( 2nd ` T ) <_ y )
278		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 ) ) ) )
279		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 ) ) ) )
280		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 ) >. }
281	280	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 ) >. } )
282	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 ) >. } )
283	19	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) e. NN )
284	20	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) e. RR )
285	116	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> y e. RR )
286	186	nnred	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( y + 1 ) e. RR )
287	286	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( y + 1 ) e. RR )
288		simpr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) <_ y )
289	116	lep1d	|- ( y e. ( 0 ... ( N - 1 ) ) -> y <_ ( y + 1 ) )
290	289	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> y <_ ( y + 1 ) )
291	284 285 287 288 290	letrd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) <_ ( y + 1 ) )
292		fznn	|- ( ( y + 1 ) e. ZZ -> ( ( 2nd ` T ) e. ( 1 ... ( y + 1 ) ) <-> ( ( 2nd ` T ) e. NN /\ ( 2nd ` T ) <_ ( y + 1 ) ) ) )
293	187 292	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( 2nd ` T ) e. ( 1 ... ( y + 1 ) ) <-> ( ( 2nd ` T ) e. NN /\ ( 2nd ` T ) <_ ( y + 1 ) ) ) )
294	293	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) e. ( 1 ... ( y + 1 ) ) <-> ( ( 2nd ` T ) e. NN /\ ( 2nd ` T ) <_ ( y + 1 ) ) ) )
295	283 291 294	mpbir2and	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) e. ( 1 ... ( y + 1 ) ) )
296	51	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) + 1 ) e. NN )
297		1red	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> 1 e. RR )
298	284 285 297 288	leadd1dd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) + 1 ) <_ ( y + 1 ) )
299		fznn	|- ( ( y + 1 ) e. ZZ -> ( ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( y + 1 ) ) <-> ( ( ( 2nd ` T ) + 1 ) e. NN /\ ( ( 2nd ` T ) + 1 ) <_ ( y + 1 ) ) ) )
300	187 299	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( y + 1 ) ) <-> ( ( ( 2nd ` T ) + 1 ) e. NN /\ ( ( 2nd ` T ) + 1 ) <_ ( y + 1 ) ) ) )
301	300	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 ) ) ) )
302	296 298 301	mpbir2and	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( y + 1 ) ) )
303		prssi	|- ( ( ( 2nd ` T ) e. ( 1 ... ( y + 1 ) ) /\ ( ( 2nd ` T ) + 1 ) e. ( 1 ... ( y + 1 ) ) ) -> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... ( y + 1 ) ) )
304	295 302 303	syl2anc	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } C_ ( 1 ... ( y + 1 ) ) )
305		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 ) ) ) )
306	304 305	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 ) ) ) )
307	282 306	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 ) ) ) )
308	281 307	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 ) >. } )
309	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 ) } )
310	308 309	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 ) } )
311		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 ) ) )
312	304 311	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 ) ) )
313	312	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 ) ) ) )
314	224	a1i	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( _I |` ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) " { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) )
315		eluzp1p1	|- ( ( N - 1 ) e. ( ZZ>= ` y ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
316	150 315	syl	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
317	316	adantl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) e. ( ZZ>= ` ( y + 1 ) ) )
318	149 317	eqeltrrd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> N e. ( ZZ>= ` ( y + 1 ) ) )
319		fzss2	|- ( N e. ( ZZ>= ` ( y + 1 ) ) -> ( 1 ... ( y + 1 ) ) C_ ( 1 ... N ) )
320	318 319	syl	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( 1 ... ( y + 1 ) ) C_ ( 1 ... N ) )
321	320	ssdifd	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
322	321	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 ) } ) )
323		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 ) } ) )
324	322 323	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 ) } ) )
325	314 324	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 ) } ) ) )
326		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 ) } ) ) )
327		uncom	|- ( (/) u. ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) ) = ( ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. (/) )
328		un0	|- ( ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) u. (/) ) = ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
329	327 328	eqtr2i	|- ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = ( (/) u. ( ( 1 ... ( y + 1 ) ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
330	325 326 329	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 ) } ) )
331	313 330	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 ) } ) )
332	310 331	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 ) } ) ) )
333	279 332	eqtrid	|- ( ( ( 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 ) } ) ) )
334	333 312	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 ) ) )
335	334	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 ) ) ) )
336	278 335	eqtrid	|- ( ( ( 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 ) ) ) )
337	336	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 } ) )
338		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 ) ) )
339	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 ) } )
340		incom	|- ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( ( ( y + 1 ) + 1 ) ... N ) ) = ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } )
341	126	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) + 1 ) e. RR )
342	186	peano2nnd	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) + 1 ) e. NN )
343	342	nnred	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) + 1 ) e. RR )
344	343	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( y + 1 ) + 1 ) e. RR )
345	21	ad2antrr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) < ( ( 2nd ` T ) + 1 ) )
346	116	ltp1d	|- ( y e. ( 0 ... ( N - 1 ) ) -> y < ( y + 1 ) )
347	346	ad2antlr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> y < ( y + 1 ) )
348	284 285 287 288 347	lelttrd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) < ( y + 1 ) )
349	284 287 297 348	ltadd1dd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) + 1 ) < ( ( y + 1 ) + 1 ) )
350	284 341 344 345 349	lttrd	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( 2nd ` T ) < ( ( y + 1 ) + 1 ) )
351		ltnle	|- ( ( ( 2nd ` T ) e. RR /\ ( ( y + 1 ) + 1 ) e. RR ) -> ( ( 2nd ` T ) < ( ( y + 1 ) + 1 ) <-> -. ( ( y + 1 ) + 1 ) <_ ( 2nd ` T ) ) )
352	20 343 351	syl2an	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( 2nd ` T ) < ( ( y + 1 ) + 1 ) <-> -. ( ( y + 1 ) + 1 ) <_ ( 2nd ` T ) ) )
353	352	adantr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( 2nd ` T ) < ( ( y + 1 ) + 1 ) <-> -. ( ( y + 1 ) + 1 ) <_ ( 2nd ` T ) ) )
354	350 353	mpbid	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> -. ( ( y + 1 ) + 1 ) <_ ( 2nd ` T ) )
355		elfzle1	|- ( ( 2nd ` T ) e. ( ( ( y + 1 ) + 1 ) ... N ) -> ( ( y + 1 ) + 1 ) <_ ( 2nd ` T ) )
356	354 355	nsyl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> -. ( 2nd ` T ) e. ( ( ( y + 1 ) + 1 ) ... N ) )
357		disjsn	|- ( ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) } ) = (/) <-> -. ( 2nd ` T ) e. ( ( ( y + 1 ) + 1 ) ... N ) )
358	356 357	sylibr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) } ) = (/) )
359		ltnle	|- ( ( ( ( 2nd ` T ) + 1 ) e. RR /\ ( ( y + 1 ) + 1 ) e. RR ) -> ( ( ( 2nd ` T ) + 1 ) < ( ( y + 1 ) + 1 ) <-> -. ( ( y + 1 ) + 1 ) <_ ( ( 2nd ` T ) + 1 ) ) )
360	126 343 359	syl2an	|- ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) -> ( ( ( 2nd ` T ) + 1 ) < ( ( y + 1 ) + 1 ) <-> -. ( ( y + 1 ) + 1 ) <_ ( ( 2nd ` T ) + 1 ) ) )
361	360	adantr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( 2nd ` T ) + 1 ) < ( ( y + 1 ) + 1 ) <-> -. ( ( y + 1 ) + 1 ) <_ ( ( 2nd ` T ) + 1 ) ) )
362	349 361	mpbid	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> -. ( ( y + 1 ) + 1 ) <_ ( ( 2nd ` T ) + 1 ) )
363		elfzle1	|- ( ( ( 2nd ` T ) + 1 ) e. ( ( ( y + 1 ) + 1 ) ... N ) -> ( ( y + 1 ) + 1 ) <_ ( ( 2nd ` T ) + 1 ) )
364	362 363	nsyl	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> -. ( ( 2nd ` T ) + 1 ) e. ( ( ( y + 1 ) + 1 ) ... N ) )
365		disjsn	|- ( ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( ( 2nd ` T ) + 1 ) } ) = (/) <-> -. ( ( 2nd ` T ) + 1 ) e. ( ( ( y + 1 ) + 1 ) ... N ) )
366	364 365	sylibr	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( ( 2nd ` T ) + 1 ) } ) = (/) )
367	358 366	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. (/) ) )
368	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 ) } ) )
369		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 ) } ) )
370	368 369	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 ) } )
371	367 370 144	3eqtr3g	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( ( y + 1 ) + 1 ) ... N ) i^i { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) = (/) )
372	340 371	eqtrid	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } i^i ( ( ( y + 1 ) + 1 ) ... N ) ) = (/) )
373		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 ) ) = (/) )
374	339 372 373	syl2anc	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( { <. ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) >. , <. ( ( 2nd ` T ) + 1 ) , ( 2nd ` T ) >. } " ( ( ( y + 1 ) + 1 ) ... N ) ) = (/) )
375	342 226	eleqtrdi	|- ( y e. ( 0 ... ( N - 1 ) ) -> ( ( y + 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
376		fzss1	|- ( ( ( y + 1 ) + 1 ) e. ( ZZ>= ` 1 ) -> ( ( ( y + 1 ) + 1 ) ... N ) C_ ( 1 ... N ) )
377		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 ) } ) ) )
378	375 376 377	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 ) } ) ) )
379	378	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 ) } ) ) )
380	371 379	mpbid	|- ( ( ( ph /\ y e. ( 0 ... ( N - 1 ) ) ) /\ ( 2nd ` T ) <_ y ) -> ( ( ( y + 1 ) + 1 ) ... N ) C_ ( ( 1 ... N ) \ { ( 2nd ` T ) , ( ( 2nd ` T ) + 1 ) } ) )
381		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 ) )
382	380 381	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 ) )
383	374 382	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 ) ) )
384		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 ) ) )
385		uncom	|- ( (/) u. ( ( ( y + 1 ) + 1 ) ... N ) ) = ( ( ( ( y + 1 ) + 1 ) ... N ) u. (/) )
386		un0	|- ( ( ( ( y + 1 ) + 1 ) ... N ) u. (/) ) = ( ( ( y + 1 ) + 1 ) ... N )
387	385 386	eqtr2i	|- ( ( ( y + 1 ) + 1 ) ... N ) = ( (/) u. ( ( ( y + 1 ) + 1 ) ... N ) )
388	383 384 387	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 ) )
389	388	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 ) ) )
390	338 389	eqtrid	|- ( ( ( 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 ) ) )
391	390	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 } ) )
392	337 391	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 } ) ) )
393	277 392	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 } ) ) )
394	393	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 } ) ) ) )
395		iffalse	|- ( -. y < ( 2nd ` T ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = ( y + 1 ) )
396	395	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 } ) ) ) )
397		ovex	|- ( y + 1 ) e. _V
398		oveq2	|- ( j = ( y + 1 ) -> ( 1 ... j ) = ( 1 ... ( y + 1 ) ) )
399	398	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 ) ) ) )
400	399	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 } ) )
401		oveq1	|- ( j = ( y + 1 ) -> ( j + 1 ) = ( ( y + 1 ) + 1 ) )
402	401	oveq1d	|- ( j = ( y + 1 ) -> ( ( j + 1 ) ... N ) = ( ( ( y + 1 ) + 1 ) ... N ) )
403	402	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 ) ) )
404	403	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 } ) )
405	400 404	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 } ) ) )
406	405	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 } ) ) ) )
407	397 406	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 } ) ) )
408	396 407	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 } ) ) ) )
409	408	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 } ) ) ) )
410	395	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 } ) ) ) )
411	398	imaeq2d	|- ( j = ( y + 1 ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) )
412	411	xpeq1d	|- ( j = ( y + 1 ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( y + 1 ) ) ) X. { 1 } ) )
413	402	imaeq2d	|- ( j = ( y + 1 ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) )
414	413	xpeq1d	|- ( j = ( y + 1 ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( ( y + 1 ) + 1 ) ... N ) ) X. { 0 } ) )
415	412 414	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 } ) ) )
416	415	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 } ) ) ) )
417	397 416	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 } ) ) )
418	410 417	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 } ) ) ) )
419	418	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 } ) ) ) )
420	394 409 419	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 } ) ) ) )
421	274 420	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 } ) ) ) )
422	421	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 } ) ) ) ) )
423	109 422	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 } ) ) ) ) )
424		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
425	424 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 ) } ) ) ) ) >. )
426	424 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 ) )
427		breq2	|- ( ( 2nd ` t ) = ( 2nd ` T ) -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` T ) ) )
428	427	ifbid	|- ( ( 2nd ` t ) = ( 2nd ` T ) -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) )
429	428	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 } ) ) ) )
430		fvex	|- ( 1st ` ( 1st ` T ) ) e. _V
431	430 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 ) ) )
432	430 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 ) } ) ) ) ) )
433		id	|- ( ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) )
434		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 ) ) )
435	434	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 } ) )
436		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 ) ) )
437	436	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 } ) )
438	435 437	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 } ) ) )
439	433 438	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 } ) ) ) )
440	431 432 439	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 } ) ) ) )
441	440	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 } ) ) ) )
442	429 441	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 } ) ) ) )
443	425 426 442	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 } ) ) ) )
444	443	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 } ) ) ) ) )
445	444	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 } ) ) ) ) ) )
446	445 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 } ) ) ) ) ) )
447	90 423 446	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 )