Theorem poimirlem7

Description: Lemma for poimir , similar to poimirlem6 , but for vertices after the opposite vertex. (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 } ) ) ) ) }
	poimirlem9.1	|- ( ph -> T e. S )
	poimirlem9.2	|- ( ph -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
	poimirlem7.3	|- ( ph -> M e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) )
Assertion	poimirlem7	|- ( ph -> ( iota_ n e. ( 1 ... N ) ( ( F ` ( M - 2 ) ) ` n ) =/= ( ( F ` ( M - 1 ) ) ` n ) ) = ( ( 2nd ` ( 1st ` T ) ) ` M ) )

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		poimirlem9.1	|- ( ph -> T e. S )
4		poimirlem9.2	|- ( ph -> ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) )
5		poimirlem7.3	|- ( ph -> M e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) )
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	3 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	8 9	syl	|- ( ph -> ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
11		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 ) } )
12	10 11	syl	|- ( ph -> ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
13		fvex	|- ( 2nd ` ( 1st ` T ) ) e. _V
14		f1oeq1	|- ( f = ( 2nd ` ( 1st ` T ) ) -> ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
15	13 14	elab	|- ( ( 2nd ` ( 1st ` T ) ) e. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } <-> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
16	12 15	sylib	|- ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
17		f1of	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 1 ... N ) )
18	16 17	syl	|- ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 1 ... N ) )
19		elfznn	|- ( ( 2nd ` T ) e. ( 1 ... ( N - 1 ) ) -> ( 2nd ` T ) e. NN )
20	4 19	syl	|- ( ph -> ( 2nd ` T ) e. NN )
21	20	peano2nnd	|- ( ph -> ( ( 2nd ` T ) + 1 ) e. NN )
22	21	peano2nnd	|- ( ph -> ( ( ( 2nd ` T ) + 1 ) + 1 ) e. NN )
23		nnuz	|- NN = ( ZZ>= ` 1 )
24	22 23	eleqtrdi	|- ( ph -> ( ( ( 2nd ` T ) + 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
25		fzss1	|- ( ( ( ( 2nd ` T ) + 1 ) + 1 ) e. ( ZZ>= ` 1 ) -> ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) C_ ( 1 ... N ) )
26	24 25	syl	|- ( ph -> ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) C_ ( 1 ... N ) )
27	26 5	sseldd	|- ( ph -> M e. ( 1 ... N ) )
28	18 27	ffvelrnd	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( 1 ... N ) )
29		xp1st	|- ( ( 1st ` T ) e. ( ( ( 0 ..^ K ) ^m ( 1 ... N ) ) X. { f | f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) -> ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
30	10 29	syl	|- ( ph -> ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) )
31		elmapfn	|- ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
32	30 31	syl	|- ( ph -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
33	32	adantr	|- ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) -> ( 1st ` ( 1st ` T ) ) Fn ( 1 ... N ) )
34		1ex	|- 1 e. _V
35		fnconstg	|- ( 1 e. _V -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) )
36	34 35	ax-mp	|- ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) )
37		c0ex	|- 0 e. _V
38		fnconstg	|- ( 0 e. _V -> ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) )
39	37 38	ax-mp	|- ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) )
40	36 39	pm3.2i	|- ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) )
41		dff1o3	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) <-> ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) /\ Fun `' ( 2nd ` ( 1st ` T ) ) ) )
42	41	simprbi	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> Fun `' ( 2nd ` ( 1st ` T ) ) )
43	16 42	syl	|- ( ph -> Fun `' ( 2nd ` ( 1st ` T ) ) )
44		imain	|- ( Fun `' ( 2nd ` ( 1st ` T ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) i^i ( M ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) )
45	43 44	syl	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) i^i ( M ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) )
46		elfzelz	|- ( M e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) -> M e. ZZ )
47	5 46	syl	|- ( ph -> M e. ZZ )
48	47	zred	|- ( ph -> M e. RR )
49	48	ltm1d	|- ( ph -> ( M - 1 ) < M )
50		fzdisj	|- ( ( M - 1 ) < M -> ( ( 1 ... ( M - 1 ) ) i^i ( M ... N ) ) = (/) )
51	49 50	syl	|- ( ph -> ( ( 1 ... ( M - 1 ) ) i^i ( M ... N ) ) = (/) )
52	51	imaeq2d	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) i^i ( M ... N ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " (/) ) )
53		ima0	|- ( ( 2nd ` ( 1st ` T ) ) " (/) ) = (/)
54	52 53	eqtrdi	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) i^i ( M ... N ) ) ) = (/) )
55	45 54	eqtr3d	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) = (/) )
56		fnun	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) = (/) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) )
57	40 55 56	sylancr	|- ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) )
58	47	zcnd	|- ( ph -> M e. CC )
59		npcan1	|- ( M e. CC -> ( ( M - 1 ) + 1 ) = M )
60	58 59	syl	|- ( ph -> ( ( M - 1 ) + 1 ) = M )
61		1red	|- ( ph -> 1 e. RR )
62	22	nnred	|- ( ph -> ( ( ( 2nd ` T ) + 1 ) + 1 ) e. RR )
63	21	nnred	|- ( ph -> ( ( 2nd ` T ) + 1 ) e. RR )
64	21	nnge1d	|- ( ph -> 1 <_ ( ( 2nd ` T ) + 1 ) )
65	63	ltp1d	|- ( ph -> ( ( 2nd ` T ) + 1 ) < ( ( ( 2nd ` T ) + 1 ) + 1 ) )
66	61 63 62 64 65	lelttrd	|- ( ph -> 1 < ( ( ( 2nd ` T ) + 1 ) + 1 ) )
67		elfzle1	|- ( M e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) -> ( ( ( 2nd ` T ) + 1 ) + 1 ) <_ M )
68	5 67	syl	|- ( ph -> ( ( ( 2nd ` T ) + 1 ) + 1 ) <_ M )
69	61 62 48 66 68	ltletrd	|- ( ph -> 1 < M )
70	61 48 69	ltled	|- ( ph -> 1 <_ M )
71		elnnz1	|- ( M e. NN <-> ( M e. ZZ /\ 1 <_ M ) )
72	47 70 71	sylanbrc	|- ( ph -> M e. NN )
73	72 23	eleqtrdi	|- ( ph -> M e. ( ZZ>= ` 1 ) )
74	60 73	eqeltrd	|- ( ph -> ( ( M - 1 ) + 1 ) e. ( ZZ>= ` 1 ) )
75		peano2zm	|- ( M e. ZZ -> ( M - 1 ) e. ZZ )
76	47 75	syl	|- ( ph -> ( M - 1 ) e. ZZ )
77		uzid	|- ( ( M - 1 ) e. ZZ -> ( M - 1 ) e. ( ZZ>= ` ( M - 1 ) ) )
78		peano2uz	|- ( ( M - 1 ) e. ( ZZ>= ` ( M - 1 ) ) -> ( ( M - 1 ) + 1 ) e. ( ZZ>= ` ( M - 1 ) ) )
79	76 77 78	3syl	|- ( ph -> ( ( M - 1 ) + 1 ) e. ( ZZ>= ` ( M - 1 ) ) )
80	60 79	eqeltrrd	|- ( ph -> M e. ( ZZ>= ` ( M - 1 ) ) )
81		uzss	|- ( M e. ( ZZ>= ` ( M - 1 ) ) -> ( ZZ>= ` M ) C_ ( ZZ>= ` ( M - 1 ) ) )
82	80 81	syl	|- ( ph -> ( ZZ>= ` M ) C_ ( ZZ>= ` ( M - 1 ) ) )
83		elfzuz3	|- ( M e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) -> N e. ( ZZ>= ` M ) )
84	5 83	syl	|- ( ph -> N e. ( ZZ>= ` M ) )
85	82 84	sseldd	|- ( ph -> N e. ( ZZ>= ` ( M - 1 ) ) )
86		fzsplit2	|- ( ( ( ( M - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ( ZZ>= ` ( M - 1 ) ) ) -> ( 1 ... N ) = ( ( 1 ... ( M - 1 ) ) u. ( ( ( M - 1 ) + 1 ) ... N ) ) )
87	74 85 86	syl2anc	|- ( ph -> ( 1 ... N ) = ( ( 1 ... ( M - 1 ) ) u. ( ( ( M - 1 ) + 1 ) ... N ) ) )
88	60	oveq1d	|- ( ph -> ( ( ( M - 1 ) + 1 ) ... N ) = ( M ... N ) )
89	88	uneq2d	|- ( ph -> ( ( 1 ... ( M - 1 ) ) u. ( ( ( M - 1 ) + 1 ) ... N ) ) = ( ( 1 ... ( M - 1 ) ) u. ( M ... N ) ) )
90	87 89	eqtrd	|- ( ph -> ( 1 ... N ) = ( ( 1 ... ( M - 1 ) ) u. ( M ... N ) ) )
91	90	imaeq2d	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) u. ( M ... N ) ) ) )
92		imaundi	|- ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) u. ( M ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) )
93	91 92	eqtrdi	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) )
94		f1ofo	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
95	16 94	syl	|- ( ph -> ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
96		foima	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
97	95 96	syl	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( 1 ... N ) )
98	93 97	eqtr3d	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) = ( 1 ... N ) )
99	98	fneq2d	|- ( ph -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) <-> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) ) )
100	57 99	mpbid	|- ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
101	100	adantr	|- ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
102		ovexd	|- ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) -> ( 1 ... N ) e. _V )
103		inidm	|- ( ( 1 ... N ) i^i ( 1 ... N ) ) = ( 1 ... N )
104		eqidd	|- ( ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) /\ n e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` n ) = ( ( 1st ` ( 1st ` T ) ) ` n ) )
105		imaundi	|- ( ( 2nd ` ( 1st ` T ) ) " ( { M } u. ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " { M } ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) )
106		fzpred	|- ( N e. ( ZZ>= ` M ) -> ( M ... N ) = ( { M } u. ( ( M + 1 ) ... N ) ) )
107	84 106	syl	|- ( ph -> ( M ... N ) = ( { M } u. ( ( M + 1 ) ... N ) ) )
108	107	imaeq2d	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( { M } u. ( ( M + 1 ) ... N ) ) ) )
109		f1ofn	|- ( ( 2nd ` ( 1st ` T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
110	16 109	syl	|- ( ph -> ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) )
111		fnsnfv	|- ( ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) /\ M e. ( 1 ... N ) ) -> { ( ( 2nd ` ( 1st ` T ) ) ` M ) } = ( ( 2nd ` ( 1st ` T ) ) " { M } ) )
112	110 27 111	syl2anc	|- ( ph -> { ( ( 2nd ` ( 1st ` T ) ) ` M ) } = ( ( 2nd ` ( 1st ` T ) ) " { M } ) )
113	112	uneq1d	|- ( ph -> ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " { M } ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
114	105 108 113	3eqtr4a	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) = ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
115	114	xpeq1d	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) = ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) X. { 0 } ) )
116		xpundir	|- ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) X. { 0 } ) = ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) )
117	115 116	eqtrdi	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) = ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) )
118	117	uneq2d	|- ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
119		un12	|- ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) = ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) )
120	118 119	eqtrdi	|- ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) = ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
121	120	fveq1d	|- ( ph -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
122	121	ad2antrr	|- ( ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
123		fnconstg	|- ( 0 e. _V -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) )
124	37 123	ax-mp	|- ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) )
125	36 124	pm3.2i	|- ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) )
126		imain	|- ( Fun `' ( 2nd ` ( 1st ` T ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) i^i ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
127	43 126	syl	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) i^i ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
128	76	zred	|- ( ph -> ( M - 1 ) e. RR )
129		peano2re	|- ( M e. RR -> ( M + 1 ) e. RR )
130	48 129	syl	|- ( ph -> ( M + 1 ) e. RR )
131	48	ltp1d	|- ( ph -> M < ( M + 1 ) )
132	128 48 130 49 131	lttrd	|- ( ph -> ( M - 1 ) < ( M + 1 ) )
133		fzdisj	|- ( ( M - 1 ) < ( M + 1 ) -> ( ( 1 ... ( M - 1 ) ) i^i ( ( M + 1 ) ... N ) ) = (/) )
134	132 133	syl	|- ( ph -> ( ( 1 ... ( M - 1 ) ) i^i ( ( M + 1 ) ... N ) ) = (/) )
135	134	imaeq2d	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) i^i ( ( M + 1 ) ... N ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " (/) ) )
136	135 53	eqtrdi	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) i^i ( ( M + 1 ) ... N ) ) ) = (/) )
137	127 136	eqtr3d	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = (/) )
138		fnun	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = (/) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
139	125 137 138	sylancr	|- ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
140		imaundi	|- ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) u. ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) )
141		imadif	|- ( Fun `' ( 2nd ` ( 1st ` T ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { M } ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` T ) ) " { M } ) ) )
142	43 141	syl	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { M } ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` T ) ) " { M } ) ) )
143		fzsplit	|- ( M e. ( 1 ... N ) -> ( 1 ... N ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) )
144	27 143	syl	|- ( ph -> ( 1 ... N ) = ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) )
145	144	difeq1d	|- ( ph -> ( ( 1 ... N ) \ { M } ) = ( ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) \ { M } ) )
146		difundir	|- ( ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) \ { M } ) = ( ( ( 1 ... M ) \ { M } ) u. ( ( ( M + 1 ) ... N ) \ { M } ) )
147		fzsplit2	|- ( ( ( ( M - 1 ) + 1 ) e. ( ZZ>= ` 1 ) /\ M e. ( ZZ>= ` ( M - 1 ) ) ) -> ( 1 ... M ) = ( ( 1 ... ( M - 1 ) ) u. ( ( ( M - 1 ) + 1 ) ... M ) ) )
148	74 80 147	syl2anc	|- ( ph -> ( 1 ... M ) = ( ( 1 ... ( M - 1 ) ) u. ( ( ( M - 1 ) + 1 ) ... M ) ) )
149	60	oveq1d	|- ( ph -> ( ( ( M - 1 ) + 1 ) ... M ) = ( M ... M ) )
150		fzsn	|- ( M e. ZZ -> ( M ... M ) = { M } )
151	47 150	syl	|- ( ph -> ( M ... M ) = { M } )
152	149 151	eqtrd	|- ( ph -> ( ( ( M - 1 ) + 1 ) ... M ) = { M } )
153	152	uneq2d	|- ( ph -> ( ( 1 ... ( M - 1 ) ) u. ( ( ( M - 1 ) + 1 ) ... M ) ) = ( ( 1 ... ( M - 1 ) ) u. { M } ) )
154	148 153	eqtrd	|- ( ph -> ( 1 ... M ) = ( ( 1 ... ( M - 1 ) ) u. { M } ) )
155	154	difeq1d	|- ( ph -> ( ( 1 ... M ) \ { M } ) = ( ( ( 1 ... ( M - 1 ) ) u. { M } ) \ { M } ) )
156		difun2	|- ( ( ( 1 ... ( M - 1 ) ) u. { M } ) \ { M } ) = ( ( 1 ... ( M - 1 ) ) \ { M } )
157	128 48	ltnled	|- ( ph -> ( ( M - 1 ) < M <-> -. M <_ ( M - 1 ) ) )
158	49 157	mpbid	|- ( ph -> -. M <_ ( M - 1 ) )
159		elfzle2	|- ( M e. ( 1 ... ( M - 1 ) ) -> M <_ ( M - 1 ) )
160	158 159	nsyl	|- ( ph -> -. M e. ( 1 ... ( M - 1 ) ) )
161		difsn	|- ( -. M e. ( 1 ... ( M - 1 ) ) -> ( ( 1 ... ( M - 1 ) ) \ { M } ) = ( 1 ... ( M - 1 ) ) )
162	160 161	syl	|- ( ph -> ( ( 1 ... ( M - 1 ) ) \ { M } ) = ( 1 ... ( M - 1 ) ) )
163	156 162	syl5eq	|- ( ph -> ( ( ( 1 ... ( M - 1 ) ) u. { M } ) \ { M } ) = ( 1 ... ( M - 1 ) ) )
164	155 163	eqtrd	|- ( ph -> ( ( 1 ... M ) \ { M } ) = ( 1 ... ( M - 1 ) ) )
165	48 130	ltnled	|- ( ph -> ( M < ( M + 1 ) <-> -. ( M + 1 ) <_ M ) )
166	131 165	mpbid	|- ( ph -> -. ( M + 1 ) <_ M )
167		elfzle1	|- ( M e. ( ( M + 1 ) ... N ) -> ( M + 1 ) <_ M )
168	166 167	nsyl	|- ( ph -> -. M e. ( ( M + 1 ) ... N ) )
169		difsn	|- ( -. M e. ( ( M + 1 ) ... N ) -> ( ( ( M + 1 ) ... N ) \ { M } ) = ( ( M + 1 ) ... N ) )
170	168 169	syl	|- ( ph -> ( ( ( M + 1 ) ... N ) \ { M } ) = ( ( M + 1 ) ... N ) )
171	164 170	uneq12d	|- ( ph -> ( ( ( 1 ... M ) \ { M } ) u. ( ( ( M + 1 ) ... N ) \ { M } ) ) = ( ( 1 ... ( M - 1 ) ) u. ( ( M + 1 ) ... N ) ) )
172	146 171	syl5eq	|- ( ph -> ( ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) \ { M } ) = ( ( 1 ... ( M - 1 ) ) u. ( ( M + 1 ) ... N ) ) )
173	145 172	eqtrd	|- ( ph -> ( ( 1 ... N ) \ { M } ) = ( ( 1 ... ( M - 1 ) ) u. ( ( M + 1 ) ... N ) ) )
174	173	imaeq2d	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... N ) \ { M } ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) u. ( ( M + 1 ) ... N ) ) ) )
175	112	eqcomd	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " { M } ) = { ( ( 2nd ` ( 1st ` T ) ) ` M ) } )
176	97 175	difeq12d	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) \ ( ( 2nd ` ( 1st ` T ) ) " { M } ) ) = ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) )
177	142 174 176	3eqtr3d	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) u. ( ( M + 1 ) ... N ) ) ) = ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) )
178	140 177	eqtr3id	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) )
179	178	fneq2d	|- ( ph -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) <-> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) ) )
180	139 179	mpbid	|- ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) )
181		eldifsn	|- ( n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) <-> ( n e. ( 1 ... N ) /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
182	181	biimpri	|- ( ( n e. ( 1 ... N ) /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) -> n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) )
183	182	ancoms	|- ( ( n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) /\ n e. ( 1 ... N ) ) -> n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) )
184		disjdif	|- ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } i^i ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) ) = (/)
185		fnconstg	|- ( 0 e. _V -> ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) Fn { ( ( 2nd ` ( 1st ` T ) ) ` M ) } )
186	37 185	ax-mp	|- ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) Fn { ( ( 2nd ` ( 1st ` T ) ) ` M ) }
187		fvun2	|- ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) Fn { ( ( 2nd ` ( 1st ` T ) ) ` M ) } /\ ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) /\ ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } i^i ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) ) = (/) /\ n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) ) ) -> ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
188	186 187	mp3an1	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) /\ ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } i^i ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) ) = (/) /\ n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) ) ) -> ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
189	184 188	mpanr1	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) /\ n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) ) -> ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
190	180 183 189	syl2an	|- ( ( ph /\ ( n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) /\ n e. ( 1 ... N ) ) ) -> ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
191	190	anassrs	|- ( ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 0 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
192	122 191	eqtrd	|- ( ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
193	33 101 102 102 103 104 192	ofval	|- ( ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( 1st ` ( 1st ` T ) ) ` n ) + ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) )
194		fnconstg	|- ( 1 e. _V -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) )
195	34 194	ax-mp	|- ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) )
196	195 124	pm3.2i	|- ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) )
197		imain	|- ( Fun `' ( 2nd ` ( 1st ` T ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
198	43 197	syl	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
199		fzdisj	|- ( M < ( M + 1 ) -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) = (/) )
200	131 199	syl	|- ( ph -> ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) = (/) )
201	200	imaeq2d	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) ) = ( ( 2nd ` ( 1st ` T ) ) " (/) ) )
202	201 53	eqtrdi	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... M ) i^i ( ( M + 1 ) ... N ) ) ) = (/) )
203	198 202	eqtr3d	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = (/) )
204		fnun	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = (/) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
205	196 203 204	sylancr	|- ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
206	144	imaeq2d	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) ) )
207		imaundi	|- ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... M ) u. ( ( M + 1 ) ... N ) ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) )
208	206 207	eqtrdi	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... N ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) )
209	208 97	eqtr3d	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = ( 1 ... N ) )
210	209	fneq2d	|- ( ph -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) u. ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) <-> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) ) )
211	205 210	mpbid	|- ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
212	211	adantr	|- ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( 1 ... N ) )
213		imaundi	|- ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) u. { M } ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " { M } ) )
214	154	imaeq2d	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( 1 ... ( M - 1 ) ) u. { M } ) ) )
215	112	uneq2d	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. ( ( 2nd ` ( 1st ` T ) ) " { M } ) ) )
216	213 214 215	3eqtr4a	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) )
217	216	xpeq1d	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) X. { 1 } ) )
218		xpundir	|- ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) u. { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) X. { 1 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) )
219	217 218	eqtrdi	|- ( ph -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) ) )
220	219	uneq1d	|- ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) )
221		un23	|- ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) )
222	221	equncomi	|- ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) = ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) )
223	220 222	eqtrdi	|- ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) = ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
224	223	fveq1d	|- ( ph -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
225	224	ad2antrr	|- ( ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
226		fnconstg	|- ( 1 e. _V -> ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) Fn { ( ( 2nd ` ( 1st ` T ) ) ` M ) } )
227	34 226	ax-mp	|- ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) Fn { ( ( 2nd ` ( 1st ` T ) ) ` M ) }
228		fvun2	|- ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) Fn { ( ( 2nd ` ( 1st ` T ) ) ` M ) } /\ ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) /\ ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } i^i ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) ) = (/) /\ n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) ) ) -> ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
229	227 228	mp3an1	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) /\ ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } i^i ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) ) = (/) /\ n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) ) ) -> ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
230	184 229	mpanr1	|- ( ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) Fn ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) /\ n e. ( ( 1 ... N ) \ { ( ( 2nd ` ( 1st ` T ) ) ` M ) } ) ) -> ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
231	180 183 230	syl2an	|- ( ( ph /\ ( n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) /\ n e. ( 1 ... N ) ) ) -> ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
232	231	anassrs	|- ( ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( { ( ( 2nd ` ( 1st ` T ) ) ` M ) } X. { 1 } ) u. ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
233	225 232	eqtrd	|- ( ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) = ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) )
234	33 212 102 102 103 104 233	ofval	|- ( ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( 1st ` ( 1st ` T ) ) ` n ) + ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` n ) ) )
235	193 234	eqtr4d	|- ( ( ( ph /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) /\ n e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
236	235	an32s	|- ( ( ( ph /\ n e. ( 1 ... N ) ) /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
237	236	anasss	|- ( ( ph /\ ( n e. ( 1 ... N ) /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) ) -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) ` n ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
238		fveq2	|- ( t = T -> ( 2nd ` t ) = ( 2nd ` T ) )
239	238	breq2d	|- ( t = T -> ( y < ( 2nd ` t ) <-> y < ( 2nd ` T ) ) )
240	239	ifbid	|- ( t = T -> if ( y < ( 2nd ` t ) , y , ( y + 1 ) ) = if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) )
241	240	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 } ) ) ) )
242		2fveq3	|- ( t = T -> ( 1st ` ( 1st ` t ) ) = ( 1st ` ( 1st ` T ) ) )
243		2fveq3	|- ( t = T -> ( 2nd ` ( 1st ` t ) ) = ( 2nd ` ( 1st ` T ) ) )
244	243	imaeq1d	|- ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) )
245	244	xpeq1d	|- ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) )
246	243	imaeq1d	|- ( t = T -> ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) )
247	246	xpeq1d	|- ( t = T -> ( ( ( 2nd ` ( 1st ` t ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) )
248	245 247	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 } ) ) )
249	242 248	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 } ) ) ) )
250	249	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 } ) ) ) )
251	241 250	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 } ) ) ) )
252	251	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 } ) ) ) ) )
253	252	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 } ) ) ) ) ) )
254	253 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 } ) ) ) ) ) )
255	254	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 } ) ) ) ) )
256	3 255	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 } ) ) ) ) )
257		breq1	|- ( y = ( M - 2 ) -> ( y < ( 2nd ` T ) <-> ( M - 2 ) < ( 2nd ` T ) ) )
258	257	adantl	|- ( ( ph /\ y = ( M - 2 ) ) -> ( y < ( 2nd ` T ) <-> ( M - 2 ) < ( 2nd ` T ) ) )
259		oveq1	|- ( y = ( M - 2 ) -> ( y + 1 ) = ( ( M - 2 ) + 1 ) )
260		sub1m1	|- ( M e. CC -> ( ( M - 1 ) - 1 ) = ( M - 2 ) )
261	58 260	syl	|- ( ph -> ( ( M - 1 ) - 1 ) = ( M - 2 ) )
262	261	oveq1d	|- ( ph -> ( ( ( M - 1 ) - 1 ) + 1 ) = ( ( M - 2 ) + 1 ) )
263	76	zcnd	|- ( ph -> ( M - 1 ) e. CC )
264		npcan1	|- ( ( M - 1 ) e. CC -> ( ( ( M - 1 ) - 1 ) + 1 ) = ( M - 1 ) )
265	263 264	syl	|- ( ph -> ( ( ( M - 1 ) - 1 ) + 1 ) = ( M - 1 ) )
266	262 265	eqtr3d	|- ( ph -> ( ( M - 2 ) + 1 ) = ( M - 1 ) )
267	259 266	sylan9eqr	|- ( ( ph /\ y = ( M - 2 ) ) -> ( y + 1 ) = ( M - 1 ) )
268	258 267	ifbieq2d	|- ( ( ph /\ y = ( M - 2 ) ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = if ( ( M - 2 ) < ( 2nd ` T ) , y , ( M - 1 ) ) )
269	20	nncnd	|- ( ph -> ( 2nd ` T ) e. CC )
270		add1p1	|- ( ( 2nd ` T ) e. CC -> ( ( ( 2nd ` T ) + 1 ) + 1 ) = ( ( 2nd ` T ) + 2 ) )
271	269 270	syl	|- ( ph -> ( ( ( 2nd ` T ) + 1 ) + 1 ) = ( ( 2nd ` T ) + 2 ) )
272	271 68	eqbrtrrd	|- ( ph -> ( ( 2nd ` T ) + 2 ) <_ M )
273	20	nnred	|- ( ph -> ( 2nd ` T ) e. RR )
274		2re	|- 2 e. RR
275		leaddsub	|- ( ( ( 2nd ` T ) e. RR /\ 2 e. RR /\ M e. RR ) -> ( ( ( 2nd ` T ) + 2 ) <_ M <-> ( 2nd ` T ) <_ ( M - 2 ) ) )
276	274 275	mp3an2	|- ( ( ( 2nd ` T ) e. RR /\ M e. RR ) -> ( ( ( 2nd ` T ) + 2 ) <_ M <-> ( 2nd ` T ) <_ ( M - 2 ) ) )
277	273 48 276	syl2anc	|- ( ph -> ( ( ( 2nd ` T ) + 2 ) <_ M <-> ( 2nd ` T ) <_ ( M - 2 ) ) )
278	61 48	posdifd	|- ( ph -> ( 1 < M <-> 0 < ( M - 1 ) ) )
279	69 278	mpbid	|- ( ph -> 0 < ( M - 1 ) )
280		elnnz	|- ( ( M - 1 ) e. NN <-> ( ( M - 1 ) e. ZZ /\ 0 < ( M - 1 ) ) )
281	76 279 280	sylanbrc	|- ( ph -> ( M - 1 ) e. NN )
282		nnm1nn0	|- ( ( M - 1 ) e. NN -> ( ( M - 1 ) - 1 ) e. NN0 )
283	281 282	syl	|- ( ph -> ( ( M - 1 ) - 1 ) e. NN0 )
284	261 283	eqeltrrd	|- ( ph -> ( M - 2 ) e. NN0 )
285	284	nn0red	|- ( ph -> ( M - 2 ) e. RR )
286	273 285	lenltd	|- ( ph -> ( ( 2nd ` T ) <_ ( M - 2 ) <-> -. ( M - 2 ) < ( 2nd ` T ) ) )
287	277 286	bitrd	|- ( ph -> ( ( ( 2nd ` T ) + 2 ) <_ M <-> -. ( M - 2 ) < ( 2nd ` T ) ) )
288	272 287	mpbid	|- ( ph -> -. ( M - 2 ) < ( 2nd ` T ) )
289	288	iffalsed	|- ( ph -> if ( ( M - 2 ) < ( 2nd ` T ) , y , ( M - 1 ) ) = ( M - 1 ) )
290	289	adantr	|- ( ( ph /\ y = ( M - 2 ) ) -> if ( ( M - 2 ) < ( 2nd ` T ) , y , ( M - 1 ) ) = ( M - 1 ) )
291	268 290	eqtrd	|- ( ( ph /\ y = ( M - 2 ) ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = ( M - 1 ) )
292	291	csbeq1d	|- ( ( ph /\ y = ( M - 2 ) ) -> [_ 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 } ) ) ) = [_ ( M - 1 ) / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
293		oveq2	|- ( j = ( M - 1 ) -> ( 1 ... j ) = ( 1 ... ( M - 1 ) ) )
294	293	imaeq2d	|- ( j = ( M - 1 ) -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) )
295	294	xpeq1d	|- ( j = ( M - 1 ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) )
296	295	adantl	|- ( ( ph /\ j = ( M - 1 ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) )
297		oveq1	|- ( j = ( M - 1 ) -> ( j + 1 ) = ( ( M - 1 ) + 1 ) )
298	297 60	sylan9eqr	|- ( ( ph /\ j = ( M - 1 ) ) -> ( j + 1 ) = M )
299	298	oveq1d	|- ( ( ph /\ j = ( M - 1 ) ) -> ( ( j + 1 ) ... N ) = ( M ... N ) )
300	299	imaeq2d	|- ( ( ph /\ j = ( M - 1 ) ) -> ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) )
301	300	xpeq1d	|- ( ( ph /\ j = ( M - 1 ) ) -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) )
302	296 301	uneq12d	|- ( ( ph /\ j = ( M - 1 ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) )
303	302	oveq2d	|- ( ( ph /\ j = ( M - 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 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) )
304	76 303	csbied	|- ( ph -> [_ ( M - 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 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) )
305	304	adantr	|- ( ( ph /\ y = ( M - 2 ) ) -> [_ ( M - 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 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) )
306	292 305	eqtrd	|- ( ( ph /\ y = ( M - 2 ) ) -> [_ 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 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) )
307		nnm1nn0	|- ( N e. NN -> ( N - 1 ) e. NN0 )
308	1 307	syl	|- ( ph -> ( N - 1 ) e. NN0 )
309	1	nnred	|- ( ph -> N e. RR )
310	48	lem1d	|- ( ph -> ( M - 1 ) <_ M )
311		elfzle2	|- ( M e. ( ( ( ( 2nd ` T ) + 1 ) + 1 ) ... N ) -> M <_ N )
312	5 311	syl	|- ( ph -> M <_ N )
313	128 48 309 310 312	letrd	|- ( ph -> ( M - 1 ) <_ N )
314	128 309 61 313	lesub1dd	|- ( ph -> ( ( M - 1 ) - 1 ) <_ ( N - 1 ) )
315	261 314	eqbrtrrd	|- ( ph -> ( M - 2 ) <_ ( N - 1 ) )
316		elfz2nn0	|- ( ( M - 2 ) e. ( 0 ... ( N - 1 ) ) <-> ( ( M - 2 ) e. NN0 /\ ( N - 1 ) e. NN0 /\ ( M - 2 ) <_ ( N - 1 ) ) )
317	284 308 315 316	syl3anbrc	|- ( ph -> ( M - 2 ) e. ( 0 ... ( N - 1 ) ) )
318		ovexd	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) e. _V )
319	256 306 317 318	fvmptd	|- ( ph -> ( F ` ( M - 2 ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) )
320	319	fveq1d	|- ( ph -> ( ( F ` ( M - 2 ) ) ` n ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) ` n ) )
321	320	adantr	|- ( ( ph /\ ( n e. ( 1 ... N ) /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) ) -> ( ( F ` ( M - 2 ) ) ` n ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) ` n ) )
322		breq1	|- ( y = ( M - 1 ) -> ( y < ( 2nd ` T ) <-> ( M - 1 ) < ( 2nd ` T ) ) )
323	322	adantl	|- ( ( ph /\ y = ( M - 1 ) ) -> ( y < ( 2nd ` T ) <-> ( M - 1 ) < ( 2nd ` T ) ) )
324		oveq1	|- ( y = ( M - 1 ) -> ( y + 1 ) = ( ( M - 1 ) + 1 ) )
325	324 60	sylan9eqr	|- ( ( ph /\ y = ( M - 1 ) ) -> ( y + 1 ) = M )
326	323 325	ifbieq2d	|- ( ( ph /\ y = ( M - 1 ) ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = if ( ( M - 1 ) < ( 2nd ` T ) , y , M ) )
327	63	lep1d	|- ( ph -> ( ( 2nd ` T ) + 1 ) <_ ( ( ( 2nd ` T ) + 1 ) + 1 ) )
328	63 62 48 327 68	letrd	|- ( ph -> ( ( 2nd ` T ) + 1 ) <_ M )
329		1re	|- 1 e. RR
330		leaddsub	|- ( ( ( 2nd ` T ) e. RR /\ 1 e. RR /\ M e. RR ) -> ( ( ( 2nd ` T ) + 1 ) <_ M <-> ( 2nd ` T ) <_ ( M - 1 ) ) )
331	329 330	mp3an2	|- ( ( ( 2nd ` T ) e. RR /\ M e. RR ) -> ( ( ( 2nd ` T ) + 1 ) <_ M <-> ( 2nd ` T ) <_ ( M - 1 ) ) )
332	273 48 331	syl2anc	|- ( ph -> ( ( ( 2nd ` T ) + 1 ) <_ M <-> ( 2nd ` T ) <_ ( M - 1 ) ) )
333	273 128	lenltd	|- ( ph -> ( ( 2nd ` T ) <_ ( M - 1 ) <-> -. ( M - 1 ) < ( 2nd ` T ) ) )
334	332 333	bitrd	|- ( ph -> ( ( ( 2nd ` T ) + 1 ) <_ M <-> -. ( M - 1 ) < ( 2nd ` T ) ) )
335	328 334	mpbid	|- ( ph -> -. ( M - 1 ) < ( 2nd ` T ) )
336	335	iffalsed	|- ( ph -> if ( ( M - 1 ) < ( 2nd ` T ) , y , M ) = M )
337	336	adantr	|- ( ( ph /\ y = ( M - 1 ) ) -> if ( ( M - 1 ) < ( 2nd ` T ) , y , M ) = M )
338	326 337	eqtrd	|- ( ( ph /\ y = ( M - 1 ) ) -> if ( y < ( 2nd ` T ) , y , ( y + 1 ) ) = M )
339	338	csbeq1d	|- ( ( ph /\ y = ( M - 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 } ) ) ) = [_ M / j ]_ ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) ) )
340		oveq2	|- ( j = M -> ( 1 ... j ) = ( 1 ... M ) )
341	340	imaeq2d	|- ( j = M -> ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) )
342	341	xpeq1d	|- ( j = M -> ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) )
343		oveq1	|- ( j = M -> ( j + 1 ) = ( M + 1 ) )
344	343	oveq1d	|- ( j = M -> ( ( j + 1 ) ... N ) = ( ( M + 1 ) ... N ) )
345	344	imaeq2d	|- ( j = M -> ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) = ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) )
346	345	xpeq1d	|- ( j = M -> ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) = ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) )
347	342 346	uneq12d	|- ( j = M -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... j ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( j + 1 ) ... N ) ) X. { 0 } ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) )
348	347	oveq2d	|- ( j = M -> ( ( 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 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
349	348	adantl	|- ( ( ph /\ j = M ) -> ( ( 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 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
350	5 349	csbied	|- ( ph -> [_ M / 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 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
351	350	adantr	|- ( ( ph /\ y = ( M - 1 ) ) -> [_ M / 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 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
352	339 351	eqtrd	|- ( ( ph /\ y = ( M - 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 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
353	281	nnnn0d	|- ( ph -> ( M - 1 ) e. NN0 )
354	48 309 61 312	lesub1dd	|- ( ph -> ( M - 1 ) <_ ( N - 1 ) )
355		elfz2nn0	|- ( ( M - 1 ) e. ( 0 ... ( N - 1 ) ) <-> ( ( M - 1 ) e. NN0 /\ ( N - 1 ) e. NN0 /\ ( M - 1 ) <_ ( N - 1 ) ) )
356	353 308 354 355	syl3anbrc	|- ( ph -> ( M - 1 ) e. ( 0 ... ( N - 1 ) ) )
357		ovexd	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) e. _V )
358	256 352 356 357	fvmptd	|- ( ph -> ( F ` ( M - 1 ) ) = ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) )
359	358	fveq1d	|- ( ph -> ( ( F ` ( M - 1 ) ) ` n ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
360	359	adantr	|- ( ( ph /\ ( n e. ( 1 ... N ) /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) ) -> ( ( F ` ( M - 1 ) ) ` n ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` n ) )
361	237 321 360	3eqtr4d	|- ( ( ph /\ ( n e. ( 1 ... N ) /\ n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) ) ) -> ( ( F ` ( M - 2 ) ) ` n ) = ( ( F ` ( M - 1 ) ) ` n ) )
362	361	expr	|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( n =/= ( ( 2nd ` ( 1st ` T ) ) ` M ) -> ( ( F ` ( M - 2 ) ) ` n ) = ( ( F ` ( M - 1 ) ) ` n ) ) )
363	362	necon1d	|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( F ` ( M - 2 ) ) ` n ) =/= ( ( F ` ( M - 1 ) ) ` n ) -> n = ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
364		elmapi	|- ( ( 1st ` ( 1st ` T ) ) e. ( ( 0 ..^ K ) ^m ( 1 ... N ) ) -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
365	30 364	syl	|- ( ph -> ( 1st ` ( 1st ` T ) ) : ( 1 ... N ) --> ( 0 ..^ K ) )
366	365 28	ffvelrnd	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) e. ( 0 ..^ K ) )
367		elfzonn0	|- ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) e. ( 0 ..^ K ) -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) e. NN0 )
368	366 367	syl	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) e. NN0 )
369	368	nn0red	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) e. RR )
370	369	ltp1d	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) < ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) + 1 ) )
371	369 370	ltned	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) =/= ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) + 1 ) )
372	319	fveq1d	|- ( ph -> ( ( F ` ( M - 2 ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
373		ovexd	|- ( ph -> ( 1 ... N ) e. _V )
374		eqidd	|- ( ( ph /\ ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( 1 ... N ) ) -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
375		fzss1	|- ( M e. ( ZZ>= ` 1 ) -> ( M ... N ) C_ ( 1 ... N ) )
376	73 375	syl	|- ( ph -> ( M ... N ) C_ ( 1 ... N ) )
377		eluzfz1	|- ( N e. ( ZZ>= ` M ) -> M e. ( M ... N ) )
378	84 377	syl	|- ( ph -> M e. ( M ... N ) )
379		fnfvima	|- ( ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) /\ ( M ... N ) C_ ( 1 ... N ) /\ M e. ( M ... N ) ) -> ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) )
380	110 376 378 379	syl3anc	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) )
381		fvun2	|- ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) /\ ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) = (/) /\ ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
382	36 39 381	mp3an12	|- ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) = (/) /\ ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
383	55 380 382	syl2anc	|- ( ph -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
384	37	fvconst2	|- ( ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = 0 )
385	380 384	syl	|- ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = 0 )
386	383 385	eqtrd	|- ( ph -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = 0 )
387	386	adantr	|- ( ( ph /\ ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( 1 ... N ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = 0 )
388	32 100 373 373 103 374 387	ofval	|- ( ( ph /\ ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) + 0 ) )
389	28 388	mpdan	|- ( ph -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... ( M - 1 ) ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( M ... N ) ) X. { 0 } ) ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) + 0 ) )
390	368	nn0cnd	|- ( ph -> ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) e. CC )
391	390	addid1d	|- ( ph -> ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) + 0 ) = ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
392	372 389 391	3eqtrd	|- ( ph -> ( ( F ` ( M - 2 ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
393	358	fveq1d	|- ( ph -> ( ( F ` ( M - 1 ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
394		fzss2	|- ( N e. ( ZZ>= ` M ) -> ( 1 ... M ) C_ ( 1 ... N ) )
395	84 394	syl	|- ( ph -> ( 1 ... M ) C_ ( 1 ... N ) )
396		elfz1end	|- ( M e. NN <-> M e. ( 1 ... M ) )
397	72 396	sylib	|- ( ph -> M e. ( 1 ... M ) )
398		fnfvima	|- ( ( ( 2nd ` ( 1st ` T ) ) Fn ( 1 ... N ) /\ ( 1 ... M ) C_ ( 1 ... N ) /\ M e. ( 1 ... M ) ) -> ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) )
399	110 395 397 398	syl3anc	|- ( ph -> ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) )
400		fvun1	|- ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) /\ ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) Fn ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) /\ ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = (/) /\ ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
401	195 124 400	mp3an12	|- ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) i^i ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) ) = (/) /\ ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
402	203 399 401	syl2anc	|- ( ph -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
403	34	fvconst2	|- ( ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = 1 )
404	399 403	syl	|- ( ph -> ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = 1 )
405	402 404	eqtrd	|- ( ph -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = 1 )
406	405	adantr	|- ( ( ph /\ ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( 1 ... N ) ) -> ( ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = 1 )
407	32 211 373 373 103 374 406	ofval	|- ( ( ph /\ ( ( 2nd ` ( 1st ` T ) ) ` M ) e. ( 1 ... N ) ) -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) + 1 ) )
408	28 407	mpdan	|- ( ph -> ( ( ( 1st ` ( 1st ` T ) ) oF + ( ( ( ( 2nd ` ( 1st ` T ) ) " ( 1 ... M ) ) X. { 1 } ) u. ( ( ( 2nd ` ( 1st ` T ) ) " ( ( M + 1 ) ... N ) ) X. { 0 } ) ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) + 1 ) )
409	393 408	eqtrd	|- ( ph -> ( ( F ` ( M - 1 ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) = ( ( ( 1st ` ( 1st ` T ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) + 1 ) )
410	371 392 409	3netr4d	|- ( ph -> ( ( F ` ( M - 2 ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) =/= ( ( F ` ( M - 1 ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
411		fveq2	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` M ) -> ( ( F ` ( M - 2 ) ) ` n ) = ( ( F ` ( M - 2 ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
412		fveq2	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` M ) -> ( ( F ` ( M - 1 ) ) ` n ) = ( ( F ` ( M - 1 ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
413	411 412	neeq12d	|- ( n = ( ( 2nd ` ( 1st ` T ) ) ` M ) -> ( ( ( F ` ( M - 2 ) ) ` n ) =/= ( ( F ` ( M - 1 ) ) ` n ) <-> ( ( F ` ( M - 2 ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) =/= ( ( F ` ( M - 1 ) ) ` ( ( 2nd ` ( 1st ` T ) ) ` M ) ) ) )
414	410 413	syl5ibrcom	|- ( ph -> ( n = ( ( 2nd ` ( 1st ` T ) ) ` M ) -> ( ( F ` ( M - 2 ) ) ` n ) =/= ( ( F ` ( M - 1 ) ) ` n ) ) )
415	414	adantr	|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( n = ( ( 2nd ` ( 1st ` T ) ) ` M ) -> ( ( F ` ( M - 2 ) ) ` n ) =/= ( ( F ` ( M - 1 ) ) ` n ) ) )
416	363 415	impbid	|- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( ( F ` ( M - 2 ) ) ` n ) =/= ( ( F ` ( M - 1 ) ) ` n ) <-> n = ( ( 2nd ` ( 1st ` T ) ) ` M ) ) )
417	28 416	riota5	|- ( ph -> ( iota_ n e. ( 1 ... N ) ( ( F ` ( M - 2 ) ) ` n ) =/= ( ( F ` ( M - 1 ) ) ` n ) ) = ( ( 2nd ` ( 1st ` T ) ) ` M ) )