Theorem poimirlem17

Description: Lemma for poimir establishing existence for poimirlem18 . (Contributed by Brendan Leahy, 21-Aug-2020)

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

Proof

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