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