Metamath Proof Explorer

Theorem poimirlem6

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