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

Theorem poimirlem6 31860
Description: Lemma for poimir 31887 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.)
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 ) ) )
poimirlem6.3  |-  ( ph  ->  M  e.  ( 1 ... ( ( 2nd `  T )  -  1 ) ) )
Assertion
Ref Expression
poimirlem6  |-  ( ph  ->  ( iota_ n  e.  ( 1 ... N ) ( ( F `  ( M  -  1
) ) `  n
)  =/=  ( ( F `  M ) `
 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 poimirlem6
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 )
1918nnzd 11040 . . . . . . 7  |-  ( ph  ->  ( 2nd `  T
)  e.  ZZ )
20 peano2zm 10981 . . . . . . 7  |-  ( ( 2nd `  T )  e.  ZZ  ->  (
( 2nd `  T
)  -  1 )  e.  ZZ )
2119, 20syl 17 . . . . . 6  |-  ( ph  ->  ( ( 2nd `  T
)  -  1 )  e.  ZZ )
22 poimir.0 . . . . . . 7  |-  ( ph  ->  N  e.  NN )
2322nnzd 11040 . . . . . 6  |-  ( ph  ->  N  e.  ZZ )
2421zred 11041 . . . . . . 7  |-  ( ph  ->  ( ( 2nd `  T
)  -  1 )  e.  RR )
2518nnred 10625 . . . . . . 7  |-  ( ph  ->  ( 2nd `  T
)  e.  RR )
2622nnred 10625 . . . . . . 7  |-  ( ph  ->  N  e.  RR )
2725lem1d 10541 . . . . . . 7  |-  ( ph  ->  ( ( 2nd `  T
)  -  1 )  <_  ( 2nd `  T
) )
28 nnm1nn0 10912 . . . . . . . . . 10  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  NN0 )
2922, 28syl 17 . . . . . . . . 9  |-  ( ph  ->  ( N  -  1 )  e.  NN0 )
3029nn0red 10927 . . . . . . . 8  |-  ( ph  ->  ( N  -  1 )  e.  RR )
31 elfzle2 11804 . . . . . . . . 9  |-  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  ->  ( 2nd `  T )  <_ 
( N  -  1 ) )
3216, 31syl 17 . . . . . . . 8  |-  ( ph  ->  ( 2nd `  T
)  <_  ( N  -  1 ) )
3326lem1d 10541 . . . . . . . 8  |-  ( ph  ->  ( N  -  1 )  <_  N )
3425, 30, 26, 32, 33letrd 9793 . . . . . . 7  |-  ( ph  ->  ( 2nd `  T
)  <_  N )
3524, 25, 26, 27, 34letrd 9793 . . . . . 6  |-  ( ph  ->  ( ( 2nd `  T
)  -  1 )  <_  N )
36 eluz2 11166 . . . . . 6  |-  ( N  e.  ( ZZ>= `  (
( 2nd `  T
)  -  1 ) )  <->  ( ( ( 2nd `  T )  -  1 )  e.  ZZ  /\  N  e.  ZZ  /\  ( ( 2nd `  T )  -  1 )  <_  N ) )
3721, 23, 35, 36syl3anbrc 1189 . . . . 5  |-  ( ph  ->  N  e.  ( ZZ>= `  ( ( 2nd `  T
)  -  1 ) ) )
38 fzss2 11839 . . . . 5  |-  ( N  e.  ( ZZ>= `  (
( 2nd `  T
)  -  1 ) )  ->  ( 1 ... ( ( 2nd `  T )  -  1 ) )  C_  (
1 ... N ) )
3937, 38syl 17 . . . 4  |-  ( ph  ->  ( 1 ... (
( 2nd `  T
)  -  1 ) )  C_  ( 1 ... N ) )
40 poimirlem6.3 . . . 4  |-  ( ph  ->  M  e.  ( 1 ... ( ( 2nd `  T )  -  1 ) ) )
4139, 40sseldd 3465 . . 3  |-  ( ph  ->  M  e.  ( 1 ... N ) )
4215, 41ffvelrnd 6035 . 2  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) ) `
 M )  e.  ( 1 ... N
) )
43 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 ) ) )
447, 43syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  (
1 ... N ) ) )
45 elmapfn 7499 . . . . . . . . . . . 12  |-  ( ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) )  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
4644, 45syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
4746adantr 466 . . . . . . . . . 10  |-  ( (
ph  /\  n  =/=  ( ( 2nd `  ( 1st `  T ) ) `
 M ) )  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
48 1ex 9639 . . . . . . . . . . . . . . 15  |-  1  e.  _V
49 fnconstg 5785 . . . . . . . . . . . . . . 15  |-  ( 1  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( M  -  1 ) ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) ) )
5048, 49ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( M  -  1 ) ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )
51 c0ex 9638 . . . . . . . . . . . . . . 15  |-  0  e.  _V
52 fnconstg 5785 . . . . . . . . . . . . . . 15  |-  ( 0  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( M ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) ) )
5351, 52ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( M ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) )
5450, 53pm3.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 ) ) )
55 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 ) ) ) )
5655simprbi 465 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  Fun  `' ( 2nd `  ( 1st `  T ) ) )
5713, 56syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  Fun  `' ( 2nd `  ( 1st `  T
) ) )
58 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 ) ) ) )
5957, 58syl 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 ) ) ) )
60 elfznn 11829 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  ( 1 ... ( ( 2nd `  T
)  -  1 ) )  ->  M  e.  NN )
6140, 60syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  M  e.  NN )
6261nnred 10625 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  M  e.  RR )
6362ltm1d 10540 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( M  -  1 )  <  M )
64 fzdisj 11827 . . . . . . . . . . . . . . . . 17  |-  ( ( M  -  1 )  <  M  ->  (
( 1 ... ( M  -  1 ) )  i^i  ( M ... N ) )  =  (/) )
6563, 64syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1 ... ( M  -  1 ) )  i^i  ( M ... N ) )  =  (/) )
6665imaeq2d 5184 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  i^i  ( M ... N
) ) )  =  ( ( 2nd `  ( 1st `  T ) )
" (/) ) )
67 ima0 5199 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  ( 1st `  T ) ) " (/) )  =  (/)
6866, 67syl6eq 2479 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  i^i  ( M ... N
) ) )  =  (/) )
6959, 68eqtr3d 2465 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) ) )  =  (/) )
70 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 ) ) ) )
7154, 69, 70sylancr 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 ) ) ) )
7261nncnd 10626 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  CC )
73 npcan1 10045 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  CC  ->  (
( M  -  1 )  +  1 )  =  M )
7472, 73syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( M  - 
1 )  +  1 )  =  M )
75 nnuz 11195 . . . . . . . . . . . . . . . . . . . 20  |-  NN  =  ( ZZ>= `  1 )
7661, 75syl6eleq 2520 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  M  e.  ( ZZ>= ` 
1 ) )
7774, 76eqeltrd 2510 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( M  - 
1 )  +  1 )  e.  ( ZZ>= ` 
1 ) )
78 nnm1nn0 10912 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  e.  NN  ->  ( M  -  1 )  e.  NN0 )
7961, 78syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( M  -  1 )  e.  NN0 )
8079nn0zd 11039 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( M  -  1 )  e.  ZZ )
81 uzid 11174 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( M  -  1 )  e.  ZZ  ->  ( M  -  1 )  e.  ( ZZ>= `  ( M  -  1 ) ) )
8280, 81syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( M  -  1 )  e.  ( ZZ>= `  ( M  -  1
) ) )
83 peano2uz 11213 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( M  -  1 )  e.  ( ZZ>= `  ( M  -  1 ) )  ->  ( ( M  -  1 )  +  1 )  e.  ( ZZ>= `  ( M  -  1 ) ) )
8482, 83syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( M  - 
1 )  +  1 )  e.  ( ZZ>= `  ( M  -  1
) ) )
8574, 84eqeltrrd 2511 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  ( ZZ>= `  ( M  -  1
) ) )
86 uzss 11180 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  ( ZZ>= `  ( M  -  1 ) )  ->  ( ZZ>= `  M )  C_  ( ZZ>=
`  ( M  - 
1 ) ) )
8785, 86syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ZZ>= `  M )  C_  ( ZZ>= `  ( M  -  1 ) ) )
8861nnzd 11040 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  ZZ )
89 elfzle2 11804 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( M  e.  ( 1 ... ( ( 2nd `  T
)  -  1 ) )  ->  M  <_  ( ( 2nd `  T
)  -  1 ) )
9040, 89syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  M  <_  ( ( 2nd `  T )  - 
1 ) )
9162, 24, 26, 90, 35letrd 9793 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  <_  N )
92 eluz2 11166 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ( ZZ>= `  M
)  <->  ( M  e.  ZZ  /\  N  e.  ZZ  /\  M  <_  N ) )
9388, 23, 91, 92syl3anbrc 1189 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
9487, 93sseldd 3465 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  -  1
) ) )
95 fzsplit2 11825 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( M  - 
1 )  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ( ZZ>= `  ( M  -  1 ) ) )  ->  ( 1 ... N )  =  ( ( 1 ... ( M  -  1 ) )  u.  (
( ( M  - 
1 )  +  1 ) ... N ) ) )
9677, 94, 95syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1 ... N
)  =  ( ( 1 ... ( M  -  1 ) )  u.  ( ( ( M  -  1 )  +  1 ) ... N ) ) )
9774oveq1d 6317 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( M  -  1 )  +  1 ) ... N
)  =  ( M ... N ) )
9897uneq2d 3620 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 1 ... ( M  -  1 ) )  u.  (
( ( M  - 
1 )  +  1 ) ... N ) )  =  ( ( 1 ... ( M  -  1 ) )  u.  ( M ... N ) ) )
9996, 98eqtrd 2463 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1 ... N
)  =  ( ( 1 ... ( M  -  1 ) )  u.  ( M ... N ) ) )
10099imaeq2d 5184 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  u.  ( M ... N
) ) ) )
101 imaundi 5264 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  ( 1st `  T ) ) "
( ( 1 ... ( M  -  1 ) )  u.  ( M ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( M  -  1 ) ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( M ... N ) ) )
102100, 101syl6eq 2479 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) ) ) )
103 f1ofo 5835 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N )
-onto-> ( 1 ... N
) )
10413, 103syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
105 foima 5812 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
) -onto-> ( 1 ... N )  ->  (
( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
106104, 105syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
107102, 106eqtr3d 2465 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) ) )  =  ( 1 ... N ) )
108107fneq2d 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 ) ) )
10971, 108mpbid 213 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... ( M  -  1 ) ) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) )  X.  { 0 } ) )  Fn  (
1 ... N ) )
110109adantr 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 ) )
111 ovex 6330 . . . . . . . . . . 11  |-  ( 1 ... N )  e. 
_V
112111a1i 11 . . . . . . . . . 10  |-  ( (
ph  /\  n  =/=  ( ( 2nd `  ( 1st `  T ) ) `
 M ) )  ->  ( 1 ... N )  e.  _V )
113 inidm 3671 . . . . . . . . . 10  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
114 eqidd 2423 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  =/=  ( ( 2nd `  ( 1st `  T ) ) `
 M ) )  /\  n  e.  ( 1 ... N ) )  ->  ( ( 1st `  ( 1st `  T
) ) `  n
)  =  ( ( 1st `  ( 1st `  T ) ) `  n ) )
115 imaundi 5264 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  ( 1st `  T ) ) "
( { M }  u.  ( ( M  + 
1 ) ... N
) ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " { M } )  u.  (
( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )
116 fzpred 11845 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  ( ZZ>= `  M
)  ->  ( M ... N )  =  ( { M }  u.  ( ( M  + 
1 ) ... N
) ) )
11793, 116syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( M ... N
)  =  ( { M }  u.  (
( M  +  1 ) ... N ) ) )
118117imaeq2d 5184 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( M ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( { M }  u.  ( ( M  +  1 ) ... N ) ) ) )
119 f1ofn 5829 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) )  Fn  (
1 ... N ) )
12013, 119syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
121 fnsnfv 5938 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 2nd `  ( 1st `  T ) )  Fn  ( 1 ... N )  /\  M  e.  ( 1 ... N
) )  ->  { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }  =  ( ( 2nd `  ( 1st `  T
) ) " { M } ) )
122120, 41, 121syl2anc 665 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  { ( ( 2nd `  ( 1st `  T
) ) `  M
) }  =  ( ( 2nd `  ( 1st `  T ) )
" { M }
) )
123122uneq1d 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 ) ) ) )
124115, 118, 1233eqtr4a 2489 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( M ... N ) )  =  ( { ( ( 2nd `  ( 1st `  T ) ) `  M ) }  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) ) )
125124xpeq1d 4873 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " ( M ... N ) )  X.  { 0 } )  =  ( ( { ( ( 2nd `  ( 1st `  T
) ) `  M
) }  u.  (
( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )  X.  { 0 } ) )
126 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 } ) )
127125, 126syl6eq 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 } ) ) )
128127uneq2d 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 } ) ) ) )
129 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 } ) ) )
130128, 129syl6eq 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 } ) ) ) )
131130fveq1d 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 ) )
132131ad2antrr 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 ) )
133 fnconstg 5785 . . . . . . . . . . . . . . . . 17  |-  ( 0  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )
13451, 133ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )
13550, 134pm3.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 ) ) )
136 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 ) ) ) )
13757, 136syl 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 ) ) ) )
13879nn0red 10927 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( M  -  1 )  e.  RR )
139 peano2re 9807 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M  e.  RR  ->  ( M  +  1 )  e.  RR )
14062, 139syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( M  +  1 )  e.  RR )
14162ltp1d 10538 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  <  ( M  +  1 ) )
142138, 62, 140, 63, 141lttrd 9797 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( M  -  1 )  <  ( M  +  1 ) )
143 fzdisj 11827 . . . . . . . . . . . . . . . . . . 19  |-  ( ( M  -  1 )  <  ( M  + 
1 )  ->  (
( 1 ... ( M  -  1 ) )  i^i  ( ( M  +  1 ) ... N ) )  =  (/) )
144142, 143syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 1 ... ( M  -  1 ) )  i^i  (
( M  +  1 ) ... N ) )  =  (/) )
145144imaeq2d 5184 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  ( ( 2nd `  ( 1st `  T ) )
" (/) ) )
146145, 67syl6eq 2479 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  (/) )
147137, 146eqtr3d 2465 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )  =  (/) )
148 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 ) ) ) )
149135, 147, 148sylancr 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 ) ) ) )
150 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 ) ) )
151 imadif 5673 . . . . . . . . . . . . . . . . . 18  |-  ( Fun  `' ( 2nd `  ( 1st `  T ) )  ->  ( ( 2nd `  ( 1st `  T
) ) " (
( 1 ... N
)  \  { M } ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... N ) ) 
\  ( ( 2nd `  ( 1st `  T
) ) " { M } ) ) )
15257, 151syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... N )  \  { M } ) )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... N
) )  \  (
( 2nd `  ( 1st `  T ) )
" { M }
) ) )
153 fzsplit 11826 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M  e.  ( 1 ... N )  ->  (
1 ... N )  =  ( ( 1 ... M )  u.  (
( M  +  1 ) ... N ) ) )
15441, 153syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1 ... N
)  =  ( ( 1 ... M )  u.  ( ( M  +  1 ) ... N ) ) )
155154difeq1d 3582 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1 ... N )  \  { M } )  =  ( ( ( 1 ... M )  u.  (
( M  +  1 ) ... N ) )  \  { M } ) )
156 difundir 3726 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1 ... M
)  u.  ( ( M  +  1 ) ... N ) ) 
\  { M }
)  =  ( ( ( 1 ... M
)  \  { M } )  u.  (
( ( M  + 
1 ) ... N
)  \  { M } ) )
157 fzsplit2 11825 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( M  - 
1 )  +  1 )  e.  ( ZZ>= ` 
1 )  /\  M  e.  ( ZZ>= `  ( M  -  1 ) ) )  ->  ( 1 ... M )  =  ( ( 1 ... ( M  -  1 ) )  u.  (
( ( M  - 
1 )  +  1 ) ... M ) ) )
15877, 85, 157syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( 1 ... M
)  =  ( ( 1 ... ( M  -  1 ) )  u.  ( ( ( M  -  1 )  +  1 ) ... M ) ) )
15974oveq1d 6317 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( ( M  -  1 )  +  1 ) ... M
)  =  ( M ... M ) )
160 fzsn 11841 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( M  e.  ZZ  ->  ( M ... M )  =  { M } )
16188, 160syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( M ... M
)  =  { M } )
162159, 161eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( ( M  -  1 )  +  1 ) ... M
)  =  { M } )
163162uneq2d 3620 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( 1 ... ( M  -  1 ) )  u.  (
( ( M  - 
1 )  +  1 ) ... M ) )  =  ( ( 1 ... ( M  -  1 ) )  u.  { M }
) )
164158, 163eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( 1 ... M
)  =  ( ( 1 ... ( M  -  1 ) )  u.  { M }
) )
165164difeq1d 3582 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 1 ... M )  \  { M } )  =  ( ( ( 1 ... ( M  -  1 ) )  u.  { M } )  \  { M } ) )
166 difun2 3875 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 1 ... ( M  -  1 ) )  u.  { M } )  \  { M } )  =  ( ( 1 ... ( M  -  1 ) )  \  { M } )
167138, 62ltnled 9783 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( ( M  - 
1 )  <  M  <->  -.  M  <_  ( M  -  1 ) ) )
16863, 167mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  -.  M  <_  ( M  -  1 ) )
169 elfzle2 11804 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  e.  ( 1 ... ( M  -  1 ) )  ->  M  <_  ( M  -  1 ) )
170168, 169nsyl 124 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  -.  M  e.  ( 1 ... ( M  -  1 ) ) )
171 difsn 4131 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( -.  M  e.  ( 1 ... ( M  - 
1 ) )  -> 
( ( 1 ... ( M  -  1 ) )  \  { M } )  =  ( 1 ... ( M  -  1 ) ) )
172170, 171syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( 1 ... ( M  -  1 ) )  \  { M } )  =  ( 1 ... ( M  -  1 ) ) )
173166, 172syl5eq 2475 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( 1 ... ( M  - 
1 ) )  u. 
{ M } ) 
\  { M }
)  =  ( 1 ... ( M  - 
1 ) ) )
174165, 173eqtrd 2463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( 1 ... M )  \  { M } )  =  ( 1 ... ( M  -  1 ) ) )
17562, 140ltnled 9783 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( M  <  ( M  +  1 )  <->  -.  ( M  +  1 )  <_  M )
)
176141, 175mpbid 213 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  -.  ( M  + 
1 )  <_  M
)
177 elfzle1 11803 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( M  e.  ( ( M  +  1 ) ... N )  ->  ( M  +  1 )  <_  M )
178176, 177nsyl 124 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  -.  M  e.  ( ( M  +  1 ) ... N ) )
179 difsn 4131 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( -.  M  e.  ( ( M  +  1 ) ... N )  -> 
( ( ( M  +  1 ) ... N )  \  { M } )  =  ( ( M  +  1 ) ... N ) )
180178, 179syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( ( M  +  1 ) ... N )  \  { M } )  =  ( ( M  +  1 ) ... N ) )
181174, 180uneq12d 3621 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( ( 1 ... M )  \  { M } )  u.  ( ( ( M  +  1 ) ... N )  \  { M } ) )  =  ( ( 1 ... ( M  -  1 ) )  u.  (
( M  +  1 ) ... N ) ) )
182156, 181syl5eq 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( ( 1 ... M )  u.  ( ( M  + 
1 ) ... N
) )  \  { M } )  =  ( ( 1 ... ( M  -  1 ) )  u.  ( ( M  +  1 ) ... N ) ) )
183155, 182eqtrd 2463 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 1 ... N )  \  { M } )  =  ( ( 1 ... ( M  -  1 ) )  u.  ( ( M  +  1 ) ... N ) ) )
184183imaeq2d 5184 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... N )  \  { M } ) )  =  ( ( 2nd `  ( 1st `  T
) ) " (
( 1 ... ( M  -  1 ) )  u.  ( ( M  +  1 ) ... N ) ) ) )
185122eqcomd 2430 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" { M }
)  =  { ( ( 2nd `  ( 1st `  T ) ) `
 M ) } )
186106, 185difeq12d 3584 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... N ) ) 
\  ( ( 2nd `  ( 1st `  T
) ) " { M } ) )  =  ( ( 1 ... N )  \  {
( ( 2nd `  ( 1st `  T ) ) `
 M ) } ) )
187152, 184, 1863eqtr3d 2471 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  u.  ( ( M  + 
1 ) ... N
) ) )  =  ( ( 1 ... N )  \  {
( ( 2nd `  ( 1st `  T ) ) `
 M ) } ) )
188150, 187syl5eqr 2477 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )  =  ( ( 1 ... N
)  \  { (
( 2nd `  ( 1st `  T ) ) `
 M ) } ) )
189188fneq2d 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 ) } ) ) )
190149, 189mpbid 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 ) } ) )
191 eldifsn 4122 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( ( 1 ... N )  \  { ( ( 2nd `  ( 1st `  T
) ) `  M
) } )  <->  ( n  e.  ( 1 ... N
)  /\  n  =/=  ( ( 2nd `  ( 1st `  T ) ) `
 M ) ) )
192191biimpri 209 . . . . . . . . . . . . . 14  |-  ( ( n  e.  ( 1 ... N )  /\  n  =/=  ( ( 2nd `  ( 1st `  T
) ) `  M
) )  ->  n  e.  ( ( 1 ... N )  \  {
( ( 2nd `  ( 1st `  T ) ) `
 M ) } ) )
193192ancoms 454 . . . . . . . . . . . . 13  |-  ( ( n  =/=  ( ( 2nd `  ( 1st `  T ) ) `  M )  /\  n  e.  ( 1 ... N
) )  ->  n  e.  ( ( 1 ... N )  \  {
( ( 2nd `  ( 1st `  T ) ) `
 M ) } ) )
194 disjdif 3867 . . . . . . . . . . . . . 14  |-  ( { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }  i^i  ( ( 1 ... N )  \  { ( ( 2nd `  ( 1st `  T
) ) `  M
) } ) )  =  (/)
195 fnconstg 5785 . . . . . . . . . . . . . . . 16  |-  ( 0  e.  _V  ->  ( { ( ( 2nd `  ( 1st `  T
) ) `  M
) }  X.  {
0 } )  Fn 
{ ( ( 2nd `  ( 1st `  T
) ) `  M
) } )
19651, 195ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }  X.  { 0 } )  Fn  { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }
197 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 ) )
198196, 197mp3an1 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 ) )
199194, 198mpanr1 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 ) )
200190, 193, 199syl2an 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 ) )
201200anassrs 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 ) )
202132, 201eqtrd 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 ) )
20347, 110, 112, 112, 113, 114, 202ofval 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 ) ) )
204 fnconstg 5785 . . . . . . . . . . . . . . 15  |-  ( 1  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) ) )
20548, 204ax-mp 5 . . . . . . . . . . . . . 14  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )
206205, 134pm3.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 ) ) )
207 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 ) ) ) )
20857, 207syl 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 ) ) ) )
209 fzdisj 11827 . . . . . . . . . . . . . . . . 17  |-  ( M  <  ( M  + 
1 )  ->  (
( 1 ... M
)  i^i  ( ( M  +  1 ) ... N ) )  =  (/) )
210141, 209syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1 ... M )  i^i  (
( M  +  1 ) ... N ) )  =  (/) )
211210imaeq2d 5184 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  ( ( 2nd `  ( 1st `  T ) )
" (/) ) )
212211, 67syl6eq 2479 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  (/) )
213208, 212eqtr3d 2465 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )  =  (/) )
214 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 ) ) ) )
215206, 213, 214sylancr 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 ) ) ) )
216154imaeq2d 5184 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  u.  ( ( M  + 
1 ) ... N
) ) ) )
217 imaundi 5264 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  ( 1st `  T ) ) "
( ( 1 ... M )  u.  (
( M  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )
218216, 217syl6eq 2479 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) ) )
219218, 106eqtr3d 2465 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
220219fneq2d 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
) ) )
221215, 220mpbid 213 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... M
) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  ( 1 ... N
) )
222221adantr 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 ) )
223 imaundi 5264 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  ( 1st `  T ) ) "
( ( 1 ... ( M  -  1 ) )  u.  { M } ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " { M } ) )
224164imaeq2d 5184 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( M  - 
1 ) )  u. 
{ M } ) ) )
225122uneq2d 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 }
) ) )
226223, 224, 2253eqtr4a 2489 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( M  - 
1 ) ) )  u.  { ( ( 2nd `  ( 1st `  T ) ) `  M ) } ) )
227226xpeq1d 4873 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  =  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( M  -  1 ) ) )  u. 
{ ( ( 2nd `  ( 1st `  T
) ) `  M
) } )  X. 
{ 1 } ) )
228 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 } ) )
229227, 228syl6eq 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 } ) ) )
230229uneq1d 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 } ) ) )
231 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 } ) )
232231equncomi 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 } ) ) )
233230, 232syl6eq 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 } ) ) ) )
234233fveq1d 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 ) )
235234ad2antrr 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 ) )
236 fnconstg 5785 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  _V  ->  ( { ( ( 2nd `  ( 1st `  T
) ) `  M
) }  X.  {
1 } )  Fn 
{ ( ( 2nd `  ( 1st `  T
) ) `  M
) } )
23748, 236ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }  X.  { 1 } )  Fn  { ( ( 2nd `  ( 1st `  T ) ) `
 M ) }
238 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 ) )
239237, 238mp3an1 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 ) )
240194, 239mpanr1 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 ) )
241190, 193, 240syl2an 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 ) )
242241anassrs 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 ) )
243235, 242eqtrd 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 ) )
24447, 222, 112, 112, 113, 114, 243ofval 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 ) ) )
245203, 244eqtr4d 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
) )
246245an32s 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 ) )
247246anasss 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
) )
248 fveq2 5878 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  T  ->  ( 2nd `  t )  =  ( 2nd `  T
) )
249248breq2d 4432 . . . . . . . . . . . . . . . . 17  |-  ( t  =  T  ->  (
y  <  ( 2nd `  t )  <->  y  <  ( 2nd `  T ) ) )
250249ifbid 3931 . . . . . . . . . . . . . . . 16  |-  ( t  =  T  ->  if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  =  if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) ) )
251250csbeq1d 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 } ) ) ) )
252 fveq2 5878 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  T  ->  ( 1st `  t )  =  ( 1st `  T
) )
253252fveq2d 5882 . . . . . . . . . . . . . . . . 17  |-  ( t  =  T  ->  ( 1st `  ( 1st `  t
) )  =  ( 1st `  ( 1st `  T ) ) )
254252fveq2d 5882 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  T  ->  ( 2nd `  ( 1st `  t
) )  =  ( 2nd `  ( 1st `  T ) ) )
255254imaeq1d 5183 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) ) )
256255xpeq1d 4873 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... j
) )  X.  {
1 } ) )
257254imaeq1d 5183 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) ) )
258257xpeq1d 4873 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )
259256, 258uneq12d 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 } ) ) )
260253, 259oveq12d 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 } )