Users' Mathboxes Mathbox for Brendan Leahy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  poimirlem7 Structured version   Unicode version

Theorem poimirlem7 31861
Description: Lemma for poimir 31887, similar to poimirlem6 31860, but for vertices after the opposite vertex. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
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
Ref Expression
poimirlem7  |-  ( ph  ->  ( iota_ n  e.  ( 1 ... N ) ( ( F `  ( M  -  2
) ) `  n
)  =/=  ( ( F `  ( M  -  1 ) ) `
 n ) )  =  ( ( 2nd `  ( 1st `  T
) ) `  M
) )
Distinct variable groups:    f, j, n, t, y    ph, j, n, y    j, F, n, y    j, M, n, y    j, N, n, y    T, j, n, y    ph, t    f, K, j, n, t    f, M, t    f, N, t    T, f    f, F, t   
t, T    S, j, n, t, y
Allowed substitution hints:    ph( f)    S( f)    K( y)

Proof of Theorem poimirlem7
StepHypRef Expression
1 poimirlem9.1 . . . . . . . 8  |-  ( ph  ->  T  e.  S )
2 elrabi 3226 . . . . . . . . 9  |-  ( 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 ) ) )
3 poimirlem22.s . . . . . . . . 9  |-  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 } ) ) ) ) }
42, 3eleq2s 2530 . . . . . . . 8  |-  ( T  e.  S  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) ) )
51, 4syl 17 . . . . . . 7  |-  ( ph  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )
6 xp1st 6834 . . . . . . 7  |-  ( 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 ) } ) )
75, 6syl 17 . . . . . 6  |-  ( ph  ->  ( 1st `  T
)  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )
8 xp2nd 6835 . . . . . 6  |-  ( ( 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 ) } )
97, 8syl 17 . . . . 5  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
10 fvex 5888 . . . . . 6  |-  ( 2nd `  ( 1st `  T
) )  e.  _V
11 f1oeq1 5819 . . . . . 6  |-  ( f  =  ( 2nd `  ( 1st `  T ) )  ->  ( f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
1210, 11elab 3218 . . . . 5  |-  ( ( 2nd `  ( 1st `  T ) )  e. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) }  <->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
139, 12sylib 199 . . . 4  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
14 f1of 5828 . . . 4  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) --> ( 1 ... N
) )
1513, 14syl 17 . . 3  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) --> ( 1 ... N ) )
16 poimirlem9.2 . . . . . . . . 9  |-  ( ph  ->  ( 2nd `  T
)  e.  ( 1 ... ( N  - 
1 ) ) )
17 elfznn 11829 . . . . . . . . 9  |-  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  ->  ( 2nd `  T )  e.  NN )
1816, 17syl 17 . . . . . . . 8  |-  ( ph  ->  ( 2nd `  T
)  e.  NN )
1918peano2nnd 10627 . . . . . . 7  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  e.  NN )
2019peano2nnd 10627 . . . . . 6  |-  ( ph  ->  ( ( ( 2nd `  T )  +  1 )  +  1 )  e.  NN )
21 nnuz 11195 . . . . . 6  |-  NN  =  ( ZZ>= `  1 )
2220, 21syl6eleq 2520 . . . . 5  |-  ( ph  ->  ( ( ( 2nd `  T )  +  1 )  +  1 )  e.  ( ZZ>= `  1
) )
23 fzss1 11838 . . . . 5  |-  ( ( ( ( 2nd `  T
)  +  1 )  +  1 )  e.  ( ZZ>= `  1 )  ->  ( ( ( ( 2nd `  T )  +  1 )  +  1 ) ... N
)  C_  ( 1 ... N ) )
2422, 23syl 17 . . . 4  |-  ( ph  ->  ( ( ( ( 2nd `  T )  +  1 )  +  1 ) ... N
)  C_  ( 1 ... N ) )
25 poimirlem7.3 . . . 4  |-  ( ph  ->  M  e.  ( ( ( ( 2nd `  T
)  +  1 )  +  1 ) ... N ) )
2624, 25sseldd 3465 . . 3  |-  ( ph  ->  M  e.  ( 1 ... N ) )
2715, 26ffvelrnd 6035 . 2  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) ) `
 M )  e.  ( 1 ... N
) )
28 xp1st 6834 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) )
297, 28syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  (
1 ... N ) ) )
30 elmapfn 7499 . . . . . . . . . . . 12  |-  ( ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) )  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
3129, 30syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
3231adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  n  =/=  ( ( 2nd `  ( 1st `  T ) ) `
 M ) )  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
33 1ex 9639 . . . . . . . . . . . . . . 15  |-  1  e.  _V
34 fnconstg 5785 . . . . . . . . . . . . . . 15  |-  ( 1  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( M  -  1 ) ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) ) )
3533, 34ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( M  -  1 ) ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )
36 c0ex 9638 . . . . . . . . . . . . . . 15  |-  0  e.  _V
37 fnconstg 5785 . . . . . . . . . . . . . . 15  |-  ( 0  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( M ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) ) )
3836, 37ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( M ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) )
3935, 38pm3.2i 456 . . . . . . . . . . . . 13  |-  ( ( ( ( 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 ) ) )
40 dff1o3 5834 . . . . . . . . . . . . . . . . 17  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( ( 2nd `  ( 1st `  T
) ) : ( 1 ... N )
-onto-> ( 1 ... N
)  /\  Fun  `' ( 2nd `  ( 1st `  T ) ) ) )
4140simprbi 465 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  Fun  `' ( 2nd `  ( 1st `  T ) ) )
4213, 41syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Fun  `' ( 2nd `  ( 1st `  T
) ) )
43 imain 5674 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) )
4442, 43syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  i^i  ( M ... N
) ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) ) ) )
45 elfzelz 11801 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  ( ( ( ( 2nd `  T
)  +  1 )  +  1 ) ... N )  ->  M  e.  ZZ )
4625, 45syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  M  e.  ZZ )
4746zred 11041 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  M  e.  RR )
4847ltm1d 10540 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( M  -  1 )  <  M )
49 fzdisj 11827 . . . . . . . . . . . . . . . . 17  |-  ( ( M  -  1 )  <  M  ->  (
( 1 ... ( M  -  1 ) )  i^i  ( M ... N ) )  =  (/) )
5048, 49syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1 ... ( M  -  1 ) )  i^i  ( M ... N ) )  =  (/) )
5150imaeq2d 5184 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  i^i  ( M ... N
) ) )  =  ( ( 2nd `  ( 1st `  T ) )
" (/) ) )
52 ima0 5199 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  ( 1st `  T ) ) " (/) )  =  (/)
5351, 52syl6eq 2479 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  i^i  ( M ... N
) ) )  =  (/) )
5444, 53eqtr3d 2465 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) ) )  =  (/) )
55 fnun 5697 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( 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 ) ) ) )
5639, 54, 55sylancr 667 . . . . . . . . . . . 12  |-  ( 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 ) ) ) )
5746zcnd 11042 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  CC )
58 npcan1 10045 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  CC  ->  (
( M  -  1 )  +  1 )  =  M )
5957, 58syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( M  - 
1 )  +  1 )  =  M )
60 1red 9659 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  1  e.  RR )
6120nnred 10625 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( 2nd `  T )  +  1 )  +  1 )  e.  RR )
6219nnred 10625 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  e.  RR )
6319nnge1d 10653 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  1  <_  ( ( 2nd `  T )  +  1 ) )
6462ltp1d 10538 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  <  ( ( ( 2nd `  T )  +  1 )  +  1 ) )
6560, 62, 61, 63, 64lelttrd 9794 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  1  <  ( ( ( 2nd `  T
)  +  1 )  +  1 ) )
66 elfzle1 11803 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( M  e.  ( ( ( ( 2nd `  T
)  +  1 )  +  1 ) ... N )  ->  (
( ( 2nd `  T
)  +  1 )  +  1 )  <_  M )
6725, 66syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( 2nd `  T )  +  1 )  +  1 )  <_  M )
6860, 61, 47, 65, 67ltletrd 9796 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  1  <  M )
6960, 47, 68ltled 9784 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  1  <_  M )
70 elnnz1 10964 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M  e.  NN  <->  ( M  e.  ZZ  /\  1  <_  M ) )
7146, 69, 70sylanbrc 668 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  NN )
7271, 21syl6eleq 2520 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
7359, 72eqeltrd 2510 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( M  - 
1 )  +  1 )  e.  ( ZZ>= ` 
1 ) )
74 peano2zm 10981 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( M  e.  ZZ  ->  ( M  -  1 )  e.  ZZ )
7546, 74syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( M  -  1 )  e.  ZZ )
76 uzid 11174 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( M  -  1 )  e.  ZZ  ->  ( M  -  1 )  e.  ( ZZ>= `  ( M  -  1 ) ) )
77 peano2uz 11213 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( M  -  1 )  e.  ( ZZ>= `  ( M  -  1 ) )  ->  ( ( M  -  1 )  +  1 )  e.  ( ZZ>= `  ( M  -  1 ) ) )
7875, 76, 773syl 18 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( M  - 
1 )  +  1 )  e.  ( ZZ>= `  ( M  -  1
) ) )
7959, 78eqeltrrd 2511 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  ( ZZ>= `  ( M  -  1
) ) )
80 uzss 11180 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  ( ZZ>= `  ( M  -  1 ) )  ->  ( ZZ>= `  M )  C_  ( ZZ>=
`  ( M  - 
1 ) ) )
8179, 80syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ZZ>= `  M )  C_  ( ZZ>= `  ( M  -  1 ) ) )
82 elfzuz3 11798 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  ( ( ( ( 2nd `  T
)  +  1 )  +  1 ) ... N )  ->  N  e.  ( ZZ>= `  M )
)
8325, 82syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
8481, 83sseldd 3465 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  -  1
) ) )
85 fzsplit2 11825 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( M  - 
1 )  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ( ZZ>= `  ( M  -  1 ) ) )  ->  ( 1 ... N )  =  ( ( 1 ... ( M  -  1 ) )  u.  (
( ( M  - 
1 )  +  1 ) ... N ) ) )
8673, 84, 85syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1 ... N
)  =  ( ( 1 ... ( M  -  1 ) )  u.  ( ( ( M  -  1 )  +  1 ) ... N ) ) )
8759oveq1d 6317 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( M  -  1 )  +  1 ) ... N
)  =  ( M ... N ) )
8887uneq2d 3620 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 1 ... ( M  -  1 ) )  u.  (
( ( M  - 
1 )  +  1 ) ... N ) )  =  ( ( 1 ... ( M  -  1 ) )  u.  ( M ... N ) ) )
8986, 88eqtrd 2463 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1 ... N
)  =  ( ( 1 ... ( M  -  1 ) )  u.  ( M ... N ) ) )
9089imaeq2d 5184 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  u.  ( M ... N
) ) ) )
91 imaundi 5264 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  ( 1st `  T ) ) "
( ( 1 ... ( M  -  1 ) )  u.  ( M ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( M  -  1 ) ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( M ... N ) ) )
9290, 91syl6eq 2479 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) ) ) )
93 f1ofo 5835 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N )
-onto-> ( 1 ... N
) )
9413, 93syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
95 foima 5812 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
) -onto-> ( 1 ... N )  ->  (
( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
9694, 95syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
9792, 96eqtr3d 2465 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) ) )  =  ( 1 ... N ) )
9897fneq2d 5682 . . . . . . . . . . . 12  |-  ( 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 ) ) )
9956, 98mpbid 213 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... ( M  -  1 ) ) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) )  X.  { 0 } ) )  Fn  (
1 ... N ) )
10099adantr 466 . . . . . . . . . 10  |-  ( (
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 ovex 6330 . . . . . . . . . . 11  |-  ( 1 ... N )  e. 
_V
102101a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  n  =/=  ( ( 2nd `  ( 1st `  T ) ) `
 M ) )  ->  ( 1 ... N )  e.  _V )
103 inidm 3671 . . . . . . . . . 10  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
104 eqidd 2423 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  =/=  ( ( 2nd `  ( 1st `  T ) ) `
 M ) )  /\  n  e.  ( 1 ... N ) )  ->  ( ( 1st `  ( 1st `  T
) ) `  n
)  =  ( ( 1st `  ( 1st `  T ) ) `  n ) )
105 imaundi 5264 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  ( 1st `  T ) ) "
( { M }  u.  ( ( M  + 
1 ) ... N
) ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " { M } )  u.  (
( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )
106 fzpred 11845 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( M ... N )  =  ( { M }  u.  ( ( M  + 
1 ) ... N
) ) )
10783, 106syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( M ... N
)  =  ( { M }  u.  (
( M  +  1 ) ... N ) ) )
108107imaeq2d 5184 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( M ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( { M }  u.  ( ( M  +  1 ) ... N ) ) ) )
109 f1ofn 5829 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) )  Fn  (
1 ... N ) )
11013, 109syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
111 fnsnfv 5938 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 2nd `  ( 1st `  T ) )  Fn  ( 1 ... N )  /\  M  e.  ( 1 ... N
) )  ->  { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }  =  ( ( 2nd `  ( 1st `  T
) ) " { M } ) )
112110, 26, 111syl2anc 665 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  { ( ( 2nd `  ( 1st `  T
) ) `  M
) }  =  ( ( 2nd `  ( 1st `  T ) )
" { M }
) )
113112uneq1d 3619 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( { ( ( 2nd `  ( 1st `  T ) ) `  M ) }  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  T ) ) " { M } )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) ) )
114105, 108, 1133eqtr4a 2489 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( M ... N ) )  =  ( { ( ( 2nd `  ( 1st `  T ) ) `  M ) }  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) ) )
115114xpeq1d 4873 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) )  X.  { 0 } )  =  ( ( { ( ( 2nd `  ( 1st `  T
) ) `  M
) }  u.  (
( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )  X.  { 0 } ) )
116 xpundir 4904 . . . . . . . . . . . . . . . 16  |-  ( ( { ( ( 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 } ) )
117115, 116syl6eq 2479 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) )  X.  { 0 } )  =  ( ( { ( ( 2nd `  ( 1st `  T
) ) `  M
) }  X.  {
0 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) ) )
118117uneq2d 3620 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... ( M  -  1 ) ) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) )  X.  { 0 } ) )  =  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  X.  { 1 } )  u.  ( ( { ( ( 2nd `  ( 1st `  T
) ) `  M
) }  X.  {
0 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
119 un12 3624 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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 } ) ) )
120118, 119syl6eq 2479 . . . . . . . . . . . . 13  |-  ( 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 } ) ) ) )
121120fveq1d 5880 . . . . . . . . . . . 12  |-  ( 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 ) )
122121ad2antrr 730 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  =/=  ( ( 2nd `  ( 1st `  T ) ) `
 M ) )  /\  n  e.  ( 1 ... N ) )  ->  ( (
( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( M ... N ) )  X. 
{ 0 } ) ) `  n )  =  ( ( ( { ( ( 2nd `  ( 1st `  T
) ) `  M
) }  X.  {
0 } )  u.  ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... ( M  -  1 ) ) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) ) ) `
 n ) )
123 fnconstg 5785 . . . . . . . . . . . . . . . . 17  |-  ( 0  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )
12436, 123ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )
12535, 124pm3.2i 456 . . . . . . . . . . . . . . 15  |-  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( M  -  1 ) ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  /\  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } )  Fn  ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )
126 imain 5674 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) ) )
12742, 126syl 17 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) ) )
12875zred 11041 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( M  -  1 )  e.  RR )
129 peano2re 9807 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M  e.  RR  ->  ( M  +  1 )  e.  RR )
13047, 129syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( M  +  1 )  e.  RR )
13147ltp1d 10538 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  <  ( M  +  1 ) )
132128, 47, 130, 48, 131lttrd 9797 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( M  -  1 )  <  ( M  +  1 ) )
133 fzdisj 11827 . . . . . . . . . . . . . . . . . . 19  |-  ( ( M  -  1 )  <  ( M  + 
1 )  ->  (
( 1 ... ( M  -  1 ) )  i^i  ( ( M  +  1 ) ... N ) )  =  (/) )
134132, 133syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 1 ... ( M  -  1 ) )  i^i  (
( M  +  1 ) ... N ) )  =  (/) )
135134imaeq2d 5184 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  ( ( 2nd `  ( 1st `  T ) )
" (/) ) )
136135, 52syl6eq 2479 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  (/) )
137127, 136eqtr3d 2465 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )  =  (/) )
138 fnun 5697 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( 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 ) ) ) )
139125, 137, 138sylancr 667 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... ( M  -  1 ) ) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) ) )
140 imaundi 5264 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  ( 1st `  T ) ) "
( ( 1 ... ( M  -  1 ) )  u.  (
( M  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( M  -  1 ) ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )
141 imadif 5673 . . . . . . . . . . . . . . . . . 18  |-  ( Fun  `' ( 2nd `  ( 1st `  T ) )  ->  ( ( 2nd `  ( 1st `  T
) ) " (
( 1 ... N
)  \  { M } ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... N ) ) 
\  ( ( 2nd `  ( 1st `  T
) ) " { M } ) ) )
14242, 141syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... N )  \  { M } ) )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... N
) )  \  (
( 2nd `  ( 1st `  T ) )
" { M }
) ) )
143 fzsplit 11826 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M  e.  ( 1 ... N )  ->  (
1 ... N )  =  ( ( 1 ... M )  u.  (
( M  +  1 ) ... N ) ) )
14426, 143syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1 ... N
)  =  ( ( 1 ... M )  u.  ( ( M  +  1 ) ... N ) ) )
145144difeq1d 3582 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1 ... N )  \  { M } )  =  ( ( ( 1 ... M )  u.  (
( M  +  1 ) ... N ) )  \  { M } ) )
146 difundir 3726 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1 ... M
)  u.  ( ( M  +  1 ) ... N ) ) 
\  { M }
)  =  ( ( ( 1 ... M
)  \  { M } )  u.  (
( ( M  + 
1 ) ... N
)  \  { M } ) )
147 fzsplit2 11825 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( M  - 
1 )  +  1 )  e.  ( ZZ>= ` 
1 )  /\  M  e.  ( ZZ>= `  ( M  -  1 ) ) )  ->  ( 1 ... M )  =  ( ( 1 ... ( M  -  1 ) )  u.  (
( ( M  - 
1 )  +  1 ) ... M ) ) )
14873, 79, 147syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( 1 ... M
)  =  ( ( 1 ... ( M  -  1 ) )  u.  ( ( ( M  -  1 )  +  1 ) ... M ) ) )
14959oveq1d 6317 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( ( M  -  1 )  +  1 ) ... M
)  =  ( M ... M ) )
150 fzsn 11841 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( M  e.  ZZ  ->  ( M ... M )  =  { M } )
15146, 150syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( M ... M
)  =  { M } )
152149, 151eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( ( M  -  1 )  +  1 ) ... M
)  =  { M } )
153152uneq2d 3620 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( 1 ... ( M  -  1 ) )  u.  (
( ( M  - 
1 )  +  1 ) ... M ) )  =  ( ( 1 ... ( M  -  1 ) )  u.  { M }
) )
154148, 153eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 1 ... M
)  =  ( ( 1 ... ( M  -  1 ) )  u.  { M }
) )
155154difeq1d 3582 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 1 ... M )  \  { M } )  =  ( ( ( 1 ... ( M  -  1 ) )  u.  { M } )  \  { M } ) )
156 difun2 3875 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 1 ... ( M  -  1 ) )  u.  { M } )  \  { M } )  =  ( ( 1 ... ( M  -  1 ) )  \  { M } )
157128, 47ltnled 9783 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( M  - 
1 )  <  M  <->  -.  M  <_  ( M  -  1 ) ) )
15848, 157mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  -.  M  <_  ( M  -  1 ) )
159 elfzle2 11804 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  e.  ( 1 ... ( M  -  1 ) )  ->  M  <_  ( M  -  1 ) )
160158, 159nsyl 124 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  -.  M  e.  ( 1 ... ( M  -  1 ) ) )
161 difsn 4131 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  M  e.  ( 1 ... ( M  - 
1 ) )  -> 
( ( 1 ... ( M  -  1 ) )  \  { M } )  =  ( 1 ... ( M  -  1 ) ) )
162160, 161syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( 1 ... ( M  -  1 ) )  \  { M } )  =  ( 1 ... ( M  -  1 ) ) )
163156, 162syl5eq 2475 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( 1 ... ( M  - 
1 ) )  u. 
{ M } ) 
\  { M }
)  =  ( 1 ... ( M  - 
1 ) ) )
164155, 163eqtrd 2463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( 1 ... M )  \  { M } )  =  ( 1 ... ( M  -  1 ) ) )
16547, 130ltnled 9783 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( M  <  ( M  +  1 )  <->  -.  ( M  +  1 )  <_  M )
)
166131, 165mpbid 213 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  -.  ( M  + 
1 )  <_  M
)
167 elfzle1 11803 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( M  e.  ( ( M  +  1 ) ... N )  ->  ( M  +  1 )  <_  M )
168166, 167nsyl 124 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  M  e.  ( ( M  +  1 ) ... N ) )
169 difsn 4131 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  M  e.  ( ( M  +  1 ) ... N )  -> 
( ( ( M  +  1 ) ... N )  \  { M } )  =  ( ( M  +  1 ) ... N ) )
170168, 169syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( ( M  +  1 ) ... N )  \  { M } )  =  ( ( M  +  1 ) ... N ) )
171164, 170uneq12d 3621 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( 1 ... M )  \  { M } )  u.  ( ( ( M  +  1 ) ... N )  \  { M } ) )  =  ( ( 1 ... ( M  -  1 ) )  u.  (
( M  +  1 ) ... N ) ) )
172146, 171syl5eq 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( 1 ... M )  u.  ( ( M  + 
1 ) ... N
) )  \  { M } )  =  ( ( 1 ... ( M  -  1 ) )  u.  ( ( M  +  1 ) ... N ) ) )
173145, 172eqtrd 2463 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 1 ... N )  \  { M } )  =  ( ( 1 ... ( M  -  1 ) )  u.  ( ( M  +  1 ) ... N ) ) )
174173imaeq2d 5184 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... N )  \  { M } ) )  =  ( ( 2nd `  ( 1st `  T
) ) " (
( 1 ... ( M  -  1 ) )  u.  ( ( M  +  1 ) ... N ) ) ) )
175112eqcomd 2430 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" { M }
)  =  { ( ( 2nd `  ( 1st `  T ) ) `
 M ) } )
17696, 175difeq12d 3584 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... N ) ) 
\  ( ( 2nd `  ( 1st `  T
) ) " { M } ) )  =  ( ( 1 ... N )  \  {
( ( 2nd `  ( 1st `  T ) ) `
 M ) } ) )
177142, 174, 1763eqtr3d 2471 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  u.  ( ( M  + 
1 ) ... N
) ) )  =  ( ( 1 ... N )  \  {
( ( 2nd `  ( 1st `  T ) ) `
 M ) } ) )
178140, 177syl5eqr 2477 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )  =  ( ( 1 ... N
)  \  { (
( 2nd `  ( 1st `  T ) ) `
 M ) } ) )
179178fneq2d 5682 . . . . . . . . . . . . . 14  |-  ( 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 ) } ) ) )
180139, 179mpbid 213 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... ( M  -  1 ) ) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  ( ( 1 ... N )  \  {
( ( 2nd `  ( 1st `  T ) ) `
 M ) } ) )
181 eldifsn 4122 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( ( 1 ... N )  \  { ( ( 2nd `  ( 1st `  T
) ) `  M
) } )  <->  ( n  e.  ( 1 ... N
)  /\  n  =/=  ( ( 2nd `  ( 1st `  T ) ) `
 M ) ) )
182181biimpri 209 . . . . . . . . . . . . . 14  |-  ( ( n  e.  ( 1 ... N )  /\  n  =/=  ( ( 2nd `  ( 1st `  T
) ) `  M
) )  ->  n  e.  ( ( 1 ... N )  \  {
( ( 2nd `  ( 1st `  T ) ) `
 M ) } ) )
183182ancoms 454 . . . . . . . . . . . . 13  |-  ( ( n  =/=  ( ( 2nd `  ( 1st `  T ) ) `  M )  /\  n  e.  ( 1 ... N
) )  ->  n  e.  ( ( 1 ... N )  \  {
( ( 2nd `  ( 1st `  T ) ) `
 M ) } ) )
184 disjdif 3867 . . . . . . . . . . . . . 14  |-  ( { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }  i^i  ( ( 1 ... N )  \  { ( ( 2nd `  ( 1st `  T
) ) `  M
) } ) )  =  (/)
185 fnconstg 5785 . . . . . . . . . . . . . . . 16  |-  ( 0  e.  _V  ->  ( { ( ( 2nd `  ( 1st `  T
) ) `  M
) }  X.  {
0 } )  Fn 
{ ( ( 2nd `  ( 1st `  T
) ) `  M
) } )
18636, 185ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }  X.  { 0 } )  Fn  { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }
187 fvun2 5950 . . . . . . . . . . . . . . 15  |-  ( ( ( { ( ( 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 ) )
188186, 187mp3an1 1347 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( 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 ) )
189184, 188mpanr1 687 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( 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 ) )
190180, 183, 189syl2an 479 . . . . . . . . . . . 12  |-  ( (
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 ) )
191190anassrs 652 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
192122, 191eqtrd 2463 . . . . . . . . . 10  |-  ( ( ( 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 ) )
19332, 100, 102, 102, 103, 104, 192ofval 6551 . . . . . . . . 9  |-  ( ( ( ph  /\  n  =/=  ( ( 2nd `  ( 1st `  T ) ) `
 M ) )  /\  n  e.  ( 1 ... N ) )  ->  ( (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( M ... N ) )  X. 
{ 0 } ) ) ) `  n
)  =  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  +  ( ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( M  -  1 ) ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) ) `
 n ) ) )
194 fnconstg 5785 . . . . . . . . . . . . . . 15  |-  ( 1  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) ) )
19533, 194ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )
196195, 124pm3.2i 456 . . . . . . . . . . . . 13  |-  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  /\  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } )  Fn  ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )
197 imain 5674 . . . . . . . . . . . . . . 15  |-  ( 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 ) ) ) )
19842, 197syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) ) )
199 fzdisj 11827 . . . . . . . . . . . . . . . . 17  |-  ( M  <  ( M  + 
1 )  ->  (
( 1 ... M
)  i^i  ( ( M  +  1 ) ... N ) )  =  (/) )
200131, 199syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1 ... M )  i^i  (
( M  +  1 ) ... N ) )  =  (/) )
201200imaeq2d 5184 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  ( ( 2nd `  ( 1st `  T ) )
" (/) ) )
202201, 52syl6eq 2479 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  (/) )
203198, 202eqtr3d 2465 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )  =  (/) )
204 fnun 5697 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( 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 ) ) ) )
205196, 203, 204sylancr 667 . . . . . . . . . . . 12  |-  ( 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 ) ) ) )
206144imaeq2d 5184 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  u.  ( ( M  + 
1 ) ... N
) ) ) )
207 imaundi 5264 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  ( 1st `  T ) ) "
( ( 1 ... M )  u.  (
( M  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )
208206, 207syl6eq 2479 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) ) )
209208, 96eqtr3d 2465 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
210209fneq2d 5682 . . . . . . . . . . . 12  |-  ( 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
) ) )
211205, 210mpbid 213 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... M
) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  ( 1 ... N
) )
212211adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  n  =/=  ( ( 2nd `  ( 1st `  T ) ) `
 M ) )  ->  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) )  Fn  ( 1 ... N ) )
213 imaundi 5264 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  ( 1st `  T ) ) "
( ( 1 ... ( M  -  1 ) )  u.  { M } ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " { M } ) )
214154imaeq2d 5184 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  u. 
{ M } ) ) )
215112uneq2d 3620 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  u.  { ( ( 2nd `  ( 1st `  T ) ) `  M ) } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... ( M  -  1 ) ) )  u.  (
( 2nd `  ( 1st `  T ) )
" { M }
) ) )
216213, 214, 2153eqtr4a 2489 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  u.  { ( ( 2nd `  ( 1st `  T ) ) `  M ) } ) )
217216xpeq1d 4873 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  =  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( M  -  1 ) ) )  u. 
{ ( ( 2nd `  ( 1st `  T
) ) `  M
) } )  X. 
{ 1 } ) )
218 xpundir 4904 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( 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 } ) )
219217, 218syl6eq 2479 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  =  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( M  -  1 ) ) )  X. 
{ 1 } )  u.  ( { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }  X.  { 1 } ) ) )
220219uneq1d 3619 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... M
) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) )  =  ( ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( M  -  1 ) ) )  X. 
{ 1 } )  u.  ( { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }  X.  { 1 } ) )  u.  (
( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) )
221 un23 3625 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( 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 } ) )
222221equncomi 3612 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( 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 } ) ) )
223220, 222syl6eq 2479 . . . . . . . . . . . . 13  |-  ( 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 } ) ) ) )
224223fveq1d 5880 . . . . . . . . . . . 12  |-  ( 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 ) )
225224ad2antrr 730 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  =/=  ( ( 2nd `  ( 1st `  T ) ) `
 M ) )  /\  n  e.  ( 1 ... N ) )  ->  ( (
( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  n )  =  ( ( ( { ( ( 2nd `  ( 1st `  T
) ) `  M
) }  X.  {
1 } )  u.  ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... ( M  -  1 ) ) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) ) ) `
 n ) )
226 fnconstg 5785 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  _V  ->  ( { ( ( 2nd `  ( 1st `  T
) ) `  M
) }  X.  {
1 } )  Fn 
{ ( ( 2nd `  ( 1st `  T
) ) `  M
) } )
22733, 226ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }  X.  { 1 } )  Fn  { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }
228 fvun2 5950 . . . . . . . . . . . . . . 15  |-  ( ( ( { ( ( 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 ) )
229227, 228mp3an1 1347 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( ( 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 ) )
230184, 229mpanr1 687 . . . . . . . . . . . . 13  |-  ( ( ( ( ( ( 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 ) )
231180, 183, 230syl2an 479 . . . . . . . . . . . 12  |-  ( (
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 ) )
232231anassrs 652 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
233225, 232eqtrd 2463 . . . . . . . . . 10  |-  ( ( ( 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 ) )
23432, 212, 102, 102, 103, 104, 233ofval 6551 . . . . . . . . 9  |-  ( ( ( 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 ) ) )
235193, 234eqtr4d 2466 . . . . . . . 8  |-  ( ( ( 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
) )
236235an32s 811 . . . . . . 7  |-  ( ( ( 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 ) )
237236anasss 651 . . . . . 6  |-  ( (
ph  /\  ( n  e.  ( 1 ... N
)  /\  n  =/=  ( ( 2nd `  ( 1st `  T ) ) `
 M ) ) )  ->  ( (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( M ... N ) )  X. 
{ 0 } ) ) ) `  n
)  =  ( ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  n
) )
238 fveq2 5878 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  T  ->  ( 2nd `  t )  =  ( 2nd `  T
) )
239238breq2d 4432 . . . . . . . . . . . . . . . . 17  |-  ( t  =  T  ->  (
y  <  ( 2nd `  t )  <->  y  <  ( 2nd `  T ) ) )
240239ifbid 3931 . . . . . . . . . . . . . . . 16  |-  ( t  =  T  ->  if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  =  if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) ) )
241240csbeq1d 3402 . . . . . . . . . . . . . . 15  |-  ( t  =  T  ->  [_ if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  [_ if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
242 fveq2 5878 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  T  ->  ( 1st `  t )  =  ( 1st `  T
) )
243242fveq2d 5882 . . . . . . . . . . . . . . . . 17  |-  ( t  =  T  ->  ( 1st `  ( 1st `  t
) )  =  ( 1st `  ( 1st `  T ) ) )
244242fveq2d 5882 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  T  ->  ( 2nd `  ( 1st `  t
) )  =  ( 2nd `  ( 1st `  T ) ) )
245244imaeq1d 5183 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) ) )
246245xpeq1d 4873 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... j
) )  X.  {
1 } ) )
247244imaeq1d 5183 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) ) )
248247xpeq1d 4873 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )
249246, 248uneq12d 3621 . . . . . . . . . . . . . . . . 17  |-  ( 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 } ) ) )
250243, 249oveq12d 6320 . . . . . . . . . . . . . . . 16  |-  ( 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 } ) ) ) )
251250csbeq2dv 3809 . . . . . . . . . . . . . . 15  |-  ( 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.  ( (