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

Theorem poimirlem11 31871
Description: Lemma for poimir 31893 connecting walks that could yield from a given cube a given face opposite the first vertex of the walk. (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 } ) ) ) ) }
poimirlem22.1  |-  ( ph  ->  F : ( 0 ... ( N  - 
1 ) ) --> ( ( 0 ... K
)  ^m  ( 1 ... N ) ) )
poimirlem12.2  |-  ( ph  ->  T  e.  S )
poimirlem11.3  |-  ( ph  ->  ( 2nd `  T
)  =  0 )
poimirlem11.4  |-  ( ph  ->  U  e.  S )
poimirlem11.5  |-  ( ph  ->  ( 2nd `  U
)  =  0 )
poimirlem11.6  |-  ( ph  ->  M  e.  ( 1 ... N ) )
Assertion
Ref Expression
poimirlem11  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  C_  ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) ) )
Distinct variable groups:    f, j,
t, y    ph, j, y   
j, F, y    j, M, y    j, N, y    T, j, y    U, j, y    ph, t    f, K, j, t    f, M, t    f, N, t    T, f    U, f    f, F, t    t, T    t, U    S, j, t, y
Allowed substitution hints:    ph( f)    S( f)    K( y)

Proof of Theorem poimirlem11
StepHypRef Expression
1 eldif 3447 . . . . . . 7  |-  ( y  e.  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... M
) )  \  (
( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) ) )  <-> 
( y  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  /\  -.  y  e.  (
( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) ) ) )
2 imassrn 5196 . . . . . . . . . . . 12  |-  ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... M
) )  C_  ran  ( 2nd `  ( 1st `  T ) )
3 poimirlem12.2 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  T  e.  S )
4 elrabi 3227 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) )
5 poimirlem22.s . . . . . . . . . . . . . . . . . . 19  |-  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 } ) ) ) ) }
64, 5eleq2s 2531 . . . . . . . . . . . . . . . . . 18  |-  ( T  e.  S  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) ) )
73, 6syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )
8 xp1st 6835 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) } ) )
97, 8syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1st `  T
)  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )
10 xp2nd 6836 . . . . . . . . . . . . . . . 16  |-  ( ( 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 ) } )
119, 10syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
12 fvex 5889 . . . . . . . . . . . . . . . 16  |-  ( 2nd `  ( 1st `  T
) )  e.  _V
13 f1oeq1 5820 . . . . . . . . . . . . . . . 16  |-  ( f  =  ( 2nd `  ( 1st `  T ) )  ->  ( f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
1412, 13elab 3219 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  ( 1st `  T ) )  e. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) }  <->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
1511, 14sylib 200 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
16 f1of 5829 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) --> ( 1 ... N
) )
1715, 16syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) --> ( 1 ... N ) )
18 frn 5750 . . . . . . . . . . . . 13  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
) --> ( 1 ... N )  ->  ran  ( 2nd `  ( 1st `  T ) )  C_  ( 1 ... N
) )
1917, 18syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ran  ( 2nd `  ( 1st `  T ) ) 
C_  ( 1 ... N ) )
202, 19syl5ss 3476 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  C_  ( 1 ... N
) )
21 poimirlem11.4 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  U  e.  S )
22 elrabi 3227 . . . . . . . . . . . . . . . . . 18  |-  ( U  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 } ) ) ) ) }  ->  U  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )
2322, 5eleq2s 2531 . . . . . . . . . . . . . . . . 17  |-  ( U  e.  S  ->  U  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) ) )
2421, 23syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  U  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )
25 xp1st 6835 . . . . . . . . . . . . . . . 16  |-  ( U  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  ->  ( 1st `  U )  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
2624, 25syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  U
)  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )
27 xp2nd 6836 . . . . . . . . . . . . . . 15  |-  ( ( 1st `  U )  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 2nd `  ( 1st `  U ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
2826, 27syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 2nd `  ( 1st `  U ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
29 fvex 5889 . . . . . . . . . . . . . . 15  |-  ( 2nd `  ( 1st `  U
) )  e.  _V
30 f1oeq1 5820 . . . . . . . . . . . . . . 15  |-  ( f  =  ( 2nd `  ( 1st `  U ) )  ->  ( f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  ( 1st `  U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
3129, 30elab 3219 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  ( 1st `  U ) )  e. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) }  <->  ( 2nd `  ( 1st `  U
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
3228, 31sylib 200 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2nd `  ( 1st `  U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
33 f1ofo 5836 . . . . . . . . . . . . 13  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  U
) ) : ( 1 ... N )
-onto-> ( 1 ... N
) )
3432, 33syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2nd `  ( 1st `  U ) ) : ( 1 ... N ) -onto-> ( 1 ... N ) )
35 foima 5813 . . . . . . . . . . . 12  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
) -onto-> ( 1 ... N )  ->  (
( 2nd `  ( 1st `  U ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
3634, 35syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
3720, 36sseqtr4d 3502 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  C_  ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... N ) ) )
3837ssdifd 3602 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) ) 
\  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) ) )  C_  ( (
( 2nd `  ( 1st `  U ) )
" ( 1 ... N ) )  \ 
( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) ) ) )
39 dff1o3 5835 . . . . . . . . . . . . 13  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( ( 2nd `  ( 1st `  U
) ) : ( 1 ... N )
-onto-> ( 1 ... N
)  /\  Fun  `' ( 2nd `  ( 1st `  U ) ) ) )
4039simprbi 466 . . . . . . . . . . . 12  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  Fun  `' ( 2nd `  ( 1st `  U ) ) )
4132, 40syl 17 . . . . . . . . . . 11  |-  ( ph  ->  Fun  `' ( 2nd `  ( 1st `  U
) ) )
42 imadif 5674 . . . . . . . . . . 11  |-  ( Fun  `' ( 2nd `  ( 1st `  U ) )  ->  ( ( 2nd `  ( 1st `  U
) ) " (
( 1 ... N
)  \  ( 1 ... M ) ) )  =  ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... N ) )  \ 
( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) ) ) )
4341, 42syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( ( 1 ... N )  \ 
( 1 ... M
) ) )  =  ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... N ) ) 
\  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) ) ) )
44 difun2 3876 . . . . . . . . . . . 12  |-  ( ( ( ( M  + 
1 ) ... N
)  u.  ( 1 ... M ) ) 
\  ( 1 ... M ) )  =  ( ( ( M  +  1 ) ... N )  \  (
1 ... M ) )
45 poimirlem11.6 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  e.  ( 1 ... N ) )
46 fzsplit 11827 . . . . . . . . . . . . . . 15  |-  ( M  e.  ( 1 ... N )  ->  (
1 ... N )  =  ( ( 1 ... M )  u.  (
( M  +  1 ) ... N ) ) )
4745, 46syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1 ... N
)  =  ( ( 1 ... M )  u.  ( ( M  +  1 ) ... N ) ) )
48 uncom 3611 . . . . . . . . . . . . . 14  |-  ( ( 1 ... M )  u.  ( ( M  +  1 ) ... N ) )  =  ( ( ( M  +  1 ) ... N )  u.  (
1 ... M ) )
4947, 48syl6eq 2480 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... N
)  =  ( ( ( M  +  1 ) ... N )  u.  ( 1 ... M ) ) )
5049difeq1d 3583 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1 ... N )  \  (
1 ... M ) )  =  ( ( ( ( M  +  1 ) ... N )  u.  ( 1 ... M ) )  \ 
( 1 ... M
) ) )
51 incom 3656 . . . . . . . . . . . . . 14  |-  ( ( ( M  +  1 ) ... N )  i^i  ( 1 ... M ) )  =  ( ( 1 ... M )  i^i  (
( M  +  1 ) ... N ) )
52 elfznn 11830 . . . . . . . . . . . . . . . . . 18  |-  ( M  e.  ( 1 ... N )  ->  M  e.  NN )
5345, 52syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  NN )
5453nnred 10626 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  RR )
5554ltp1d 10539 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  <  ( M  +  1 ) )
56 fzdisj 11828 . . . . . . . . . . . . . . 15  |-  ( M  <  ( M  + 
1 )  ->  (
( 1 ... M
)  i^i  ( ( M  +  1 ) ... N ) )  =  (/) )
5755, 56syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1 ... M )  i^i  (
( M  +  1 ) ... N ) )  =  (/) )
5851, 57syl5eq 2476 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( M  +  1 ) ... N )  i^i  (
1 ... M ) )  =  (/) )
59 disj3 3838 . . . . . . . . . . . . 13  |-  ( ( ( ( M  + 
1 ) ... N
)  i^i  ( 1 ... M ) )  =  (/)  <->  ( ( M  +  1 ) ... N )  =  ( ( ( M  + 
1 ) ... N
)  \  ( 1 ... M ) ) )
6058, 59sylib 200 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( M  + 
1 ) ... N
)  =  ( ( ( M  +  1 ) ... N ) 
\  ( 1 ... M ) ) )
6144, 50, 603eqtr4a 2490 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1 ... N )  \  (
1 ... M ) )  =  ( ( M  +  1 ) ... N ) )
6261imaeq2d 5185 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( ( 1 ... N )  \ 
( 1 ... M
) ) )  =  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )
6343, 62eqtr3d 2466 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... N ) ) 
\  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) ) )  =  ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) ) )
6438, 63sseqtrd 3501 . . . . . . . 8  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) ) 
\  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) ) )  C_  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) ) )
6564sselda 3465 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) ) 
\  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) ) ) )  ->  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )
661, 65sylan2br 479 . . . . . 6  |-  ( (
ph  /\  ( y  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  /\  -.  y  e.  (
( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) ) ) )  ->  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )
67 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  U  ->  ( 2nd `  t )  =  ( 2nd `  U
) )
6867breq2d 4433 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  U  ->  (
y  <  ( 2nd `  t )  <->  y  <  ( 2nd `  U ) ) )
6968ifbid 3932 . . . . . . . . . . . . . . . . 17  |-  ( t  =  U  ->  if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  =  if ( y  <  ( 2nd `  U
) ,  y ,  ( y  +  1 ) ) )
7069csbeq1d 3403 . . . . . . . . . . . . . . . 16  |-  ( t  =  U  ->  [_ 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 `  U ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
71 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  U  ->  ( 1st `  t )  =  ( 1st `  U
) )
7271fveq2d 5883 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  U  ->  ( 1st `  ( 1st `  t
) )  =  ( 1st `  ( 1st `  U ) ) )
7371fveq2d 5883 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  U  ->  ( 2nd `  ( 1st `  t
) )  =  ( 2nd `  ( 1st `  U ) ) )
7473imaeq1d 5184 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  U  ->  (
( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... j ) ) )
7574xpeq1d 4874 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  U  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  U ) ) "
( 1 ... j
) )  X.  {
1 } ) )
7673imaeq1d 5184 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  U  ->  (
( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) ) )
7776xpeq1d 4874 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  U  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )
7875, 77uneq12d 3622 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  U  ->  (
( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) )  =  ( ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )
7972, 78oveq12d 6321 . . . . . . . . . . . . . . . . 17  |-  ( t  =  U  ->  (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
8079csbeq2dv 3810 . . . . . . . . . . . . . . . 16  |-  ( t  =  U  ->  [_ if ( y  <  ( 2nd `  U ) ,  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 `  U ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
8170, 80eqtrd 2464 . . . . . . . . . . . . . . 15  |-  ( t  =  U  ->  [_ 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 `  U ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
8281mpteq2dv 4509 . . . . . . . . . . . . . 14  |-  ( t  =  U  ->  (
y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )  =  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  ( 2nd `  U
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
8382eqeq2d 2437 . . . . . . . . . . . . 13  |-  ( t  =  U  ->  ( F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  t
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )  <->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  ( 2nd `  U
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) ) )
8483, 5elrab2 3232 . . . . . . . . . . . 12  |-  ( U  e.  S  <->  ( U  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 `  U
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) ) )
8584simprbi 466 . . . . . . . . . . 11  |-  ( U  e.  S  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  U
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
8621, 85syl 17 . . . . . . . . . 10  |-  ( ph  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  U ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
87 poimirlem11.5 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 2nd `  U
)  =  0 )
88 breq12 4426 . . . . . . . . . . . . . . . 16  |-  ( ( y  =  ( M  -  1 )  /\  ( 2nd `  U )  =  0 )  -> 
( y  <  ( 2nd `  U )  <->  ( M  -  1 )  <  0 ) )
8987, 88sylan2 477 . . . . . . . . . . . . . . 15  |-  ( ( y  =  ( M  -  1 )  /\  ph )  ->  ( y  <  ( 2nd `  U
)  <->  ( M  - 
1 )  <  0
) )
9089ancoms 455 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  (
y  <  ( 2nd `  U )  <->  ( M  -  1 )  <  0 ) )
91 oveq1 6310 . . . . . . . . . . . . . . 15  |-  ( y  =  ( M  - 
1 )  ->  (
y  +  1 )  =  ( ( M  -  1 )  +  1 ) )
9253nncnd 10627 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  CC )
93 npcan1 10046 . . . . . . . . . . . . . . . 16  |-  ( M  e.  CC  ->  (
( M  -  1 )  +  1 )  =  M )
9492, 93syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( M  - 
1 )  +  1 )  =  M )
9591, 94sylan9eqr 2486 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  (
y  +  1 )  =  M )
9690, 95ifbieq2d 3935 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  if ( y  <  ( 2nd `  U ) ,  y ,  ( y  +  1 ) )  =  if ( ( M  -  1 )  <  0 ,  y ,  M ) )
9753nnzd 11041 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  M  e.  ZZ )
98 poimir.0 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  N  e.  NN )
9998nnzd 11041 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  ZZ )
100 elfzm1b 11874 . . . . . . . . . . . . . . . . . . 19  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  e.  ( 1 ... N )  <-> 
( M  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) ) )
10197, 99, 100syl2anc 666 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( M  e.  ( 1 ... N )  <-> 
( M  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) ) )
10245, 101mpbid 214 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( M  -  1 )  e.  ( 0 ... ( N  - 
1 ) ) )
103 elfzle1 11804 . . . . . . . . . . . . . . . . 17  |-  ( ( M  -  1 )  e.  ( 0 ... ( N  -  1 ) )  ->  0  <_  ( M  -  1 ) )
104102, 103syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  0  <_  ( M  -  1 ) )
105 0red 9646 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  0  e.  RR )
106 nnm1nn0 10913 . . . . . . . . . . . . . . . . . . 19  |-  ( M  e.  NN  ->  ( M  -  1 )  e.  NN0 )
10753, 106syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( M  -  1 )  e.  NN0 )
108107nn0red 10928 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( M  -  1 )  e.  RR )
109105, 108lenltd 9783 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 0  <_  ( M  -  1 )  <->  -.  ( M  -  1 )  <  0 ) )
110104, 109mpbid 214 . . . . . . . . . . . . . . 15  |-  ( ph  ->  -.  ( M  - 
1 )  <  0
)
111110iffalsed 3921 . . . . . . . . . . . . . 14  |-  ( ph  ->  if ( ( M  -  1 )  <  0 ,  y ,  M )  =  M )
112111adantr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  if ( ( M  - 
1 )  <  0 ,  y ,  M
)  =  M )
11396, 112eqtrd 2464 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  if ( y  <  ( 2nd `  U ) ,  y ,  ( y  +  1 ) )  =  M )
114113csbeq1d 3403 . . . . . . . . . . 11  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  [_ if ( y  <  ( 2nd `  U ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  [_ M  /  j ]_ (
( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
115 oveq2 6311 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  M  ->  (
1 ... j )  =  ( 1 ... M
) )
116115imaeq2d 5185 . . . . . . . . . . . . . . . . 17  |-  ( j  =  M  ->  (
( 2nd `  ( 1st `  U ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) ) )
117116xpeq1d 4874 . . . . . . . . . . . . . . . 16  |-  ( j  =  M  ->  (
( ( 2nd `  ( 1st `  U ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  U ) ) "
( 1 ... M
) )  X.  {
1 } ) )
118 oveq1 6310 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  M  ->  (
j  +  1 )  =  ( M  + 
1 ) )
119118oveq1d 6318 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  M  ->  (
( j  +  1 ) ... N )  =  ( ( M  +  1 ) ... N ) )
120119imaeq2d 5185 . . . . . . . . . . . . . . . . 17  |-  ( j  =  M  ->  (
( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )
121120xpeq1d 4874 . . . . . . . . . . . . . . . 16  |-  ( j  =  M  ->  (
( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) )
122117, 121uneq12d 3622 . . . . . . . . . . . . . . 15  |-  ( j  =  M  ->  (
( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) )  =  ( ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) ) )
123122oveq2d 6319 . . . . . . . . . . . . . 14  |-  ( j  =  M  ->  (
( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
124123adantl 468 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  =  M )  ->  (
( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
12545, 124csbied 3423 . . . . . . . . . . . 12  |-  ( ph  ->  [_ M  /  j ]_ ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
126125adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  [_ M  /  j ]_ (
( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
127114, 126eqtrd 2464 . . . . . . . . . 10  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  [_ if ( y  <  ( 2nd `  U ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
128 ovex 6331 . . . . . . . . . . 11  |-  ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) ) )  e.  _V
129128a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  e.  _V )
13086, 127, 102, 129fvmptd 5968 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( M  -  1 ) )  =  ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) ) ) )
131130fveq1d 5881 . . . . . . . 8  |-  ( ph  ->  ( ( F `  ( M  -  1
) ) `  y
)  =  ( ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  y
) )
132131adantr 467 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( ( F `
 ( M  - 
1 ) ) `  y )  =  ( ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  y
) )
133 imassrn 5196 . . . . . . . . . 10  |-  ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  C_  ran  ( 2nd `  ( 1st `  U ) )
134 f1of 5829 . . . . . . . . . . . 12  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  U
) ) : ( 1 ... N ) --> ( 1 ... N
) )
13532, 134syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( 2nd `  ( 1st `  U ) ) : ( 1 ... N ) --> ( 1 ... N ) )
136 frn 5750 . . . . . . . . . . 11  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
) --> ( 1 ... N )  ->  ran  ( 2nd `  ( 1st `  U ) )  C_  ( 1 ... N
) )
137135, 136syl 17 . . . . . . . . . 10  |-  ( ph  ->  ran  ( 2nd `  ( 1st `  U ) ) 
C_  ( 1 ... N ) )
138133, 137syl5ss 3476 . . . . . . . . 9  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  C_  ( 1 ... N
) )
139138sselda 3465 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  y  e.  ( 1 ... N ) )
140 xp1st 6835 . . . . . . . . . . . 12  |-  ( ( 1st `  U )  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 1st `  ( 1st `  U ) )  e.  ( ( 0..^ K )  ^m  (
1 ... N ) ) )
14126, 140syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( 1st `  ( 1st `  U ) )  e.  ( ( 0..^ K )  ^m  (
1 ... N ) ) )
142 elmapfn 7500 . . . . . . . . . . 11  |-  ( ( 1st `  ( 1st `  U ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) )  ->  ( 1st `  ( 1st `  U ) )  Fn  ( 1 ... N ) )
143141, 142syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  ( 1st `  U ) )  Fn  ( 1 ... N ) )
144143adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( 1st `  ( 1st `  U ) )  Fn  ( 1 ... N ) )
145 1ex 9640 . . . . . . . . . . . . . 14  |-  1  e.  _V
146 fnconstg 5786 . . . . . . . . . . . . . 14  |-  ( 1  e.  _V  ->  (
( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) ) )
147145, 146ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )
148 c0ex 9639 . . . . . . . . . . . . . 14  |-  0  e.  _V
149 fnconstg 5786 . . . . . . . . . . . . . 14  |-  ( 0  e.  _V  ->  (
( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) ) )
150148, 149ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) )
151147, 150pm3.2i 457 . . . . . . . . . . . 12  |-  ( ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  /\  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } )  Fn  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )
152 imain 5675 . . . . . . . . . . . . . 14  |-  ( Fun  `' ( 2nd `  ( 1st `  U ) )  ->  ( ( 2nd `  ( 1st `  U
) ) " (
( 1 ... M
)  i^i  ( ( M  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  i^i  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) ) )
15341, 152syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  i^i  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) ) ) )
15457imaeq2d 5185 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  ( ( 2nd `  ( 1st `  U ) )
" (/) ) )
155 ima0 5200 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  ( 1st `  U ) ) " (/) )  =  (/)
156154, 155syl6eq 2480 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  (/) )
157153, 156eqtr3d 2466 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  i^i  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) ) )  =  (/) )
158 fnun 5698 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( 2nd `  ( 1st `  U ) ) "
( 1 ... M
) )  X.  {
1 } )  Fn  ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  /\  ( ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } )  Fn  (
( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  /\  ( ( ( 2nd `  ( 1st `  U ) ) "
( 1 ... M
) )  i^i  (
( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  =  (/) )  ->  (
( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  u.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) ) )
159151, 157, 158sylancr 668 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( 2nd `  ( 1st `  U ) ) "
( 1 ... M
) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  u.  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) ) ) )
160 imaundi 5265 . . . . . . . . . . . . 13  |-  ( ( 2nd `  ( 1st `  U ) ) "
( ( 1 ... M )  u.  (
( M  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  u.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )
16147imaeq2d 5185 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... N ) )  =  ( ( 2nd `  ( 1st `  U ) )
" ( ( 1 ... M )  u.  ( ( M  + 
1 ) ... N
) ) ) )
162161, 36eqtr3d 2466 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( ( 1 ... M )  u.  ( ( M  + 
1 ) ... N
) ) )  =  ( 1 ... N
) )
163160, 162syl5eqr 2478 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  u.  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
164163fneq2d 5683 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) )  Fn  ( ( ( 2nd `  ( 1st `  U ) ) "
( 1 ... M
) )  u.  (
( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  <-> 
( ( ( ( 2nd `  ( 1st `  U ) ) "
( 1 ... M
) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  ( 1 ... N
) ) )
165159, 164mpbid 214 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( 2nd `  ( 1st `  U ) ) "
( 1 ... M
) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  ( 1 ... N
) )
166165adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) )  Fn  ( 1 ... N ) )
167 ovex 6331 . . . . . . . . . 10  |-  ( 1 ... N )  e. 
_V
168167a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( 1 ... N )  e.  _V )
169 inidm 3672 . . . . . . . . 9  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
170 eqidd 2424 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  /\  y  e.  ( 1 ... N ) )  ->  ( ( 1st `  ( 1st `  U
) ) `  y
)  =  ( ( 1st `  ( 1st `  U ) ) `  y ) )
171 fvun2 5951 . . . . . . . . . . . . 13  |-  ( ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  Fn  ( ( 2nd `  ( 1st `  U ) ) "
( 1 ... M
) )  /\  (
( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) )  /\  ( ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  i^i  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  =  (/)  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) ) )  ->  ( (
( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  y )  =  ( ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) `
 y ) )
172147, 150, 171mp3an12 1351 . . . . . . . . . . . 12  |-  ( ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  i^i  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) ) )  =  (/)  /\  y  e.  ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) ) )  -> 
( ( ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) ) `
 y )  =  ( ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) `  y ) )
173157, 172sylan 474 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( ( ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) ) `
 y )  =  ( ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) `  y ) )
174148fvconst2 6133 . . . . . . . . . . . 12  |-  ( y  e.  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) )  ->  ( (
( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) `
 y )  =  0 )
175174adantl 468 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) `
 y )  =  0 )
176173, 175eqtrd 2464 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( ( ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) ) `
 y )  =  0 )
177176adantr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  /\  y  e.  ( 1 ... N ) )  ->  ( (
( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  y )  =  0 )
178144, 166, 168, 168, 169, 170, 177ofval 6552 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  /\  y  e.  ( 1 ... N ) )  ->  ( (
( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  y
)  =  ( ( ( 1st `  ( 1st `  U ) ) `
 y )  +  0 ) )
179139, 178mpdan 673 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) ) ) `  y )  =  ( ( ( 1st `  ( 1st `  U ) ) `  y )  +  0 ) )
180 elmapi 7499 . . . . . . . . . . . . 13  |-  ( ( 1st `  ( 1st `  U ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) )  ->  ( 1st `  ( 1st `  U ) ) : ( 1 ... N ) --> ( 0..^ K ) )
181141, 180syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1st `  ( 1st `  U ) ) : ( 1 ... N ) --> ( 0..^ K ) )
182181ffvelrnda 6035 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( 1 ... N
) )  ->  (
( 1st `  ( 1st `  U ) ) `
 y )  e.  ( 0..^ K ) )
183 elfzonn0 11962 . . . . . . . . . . 11  |-  ( ( ( 1st `  ( 1st `  U ) ) `
 y )  e.  ( 0..^ K )  ->  ( ( 1st `  ( 1st `  U
) ) `  y
)  e.  NN0 )
184182, 183syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( 1 ... N
) )  ->  (
( 1st `  ( 1st `  U ) ) `
 y )  e. 
NN0 )
185184nn0cnd 10929 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 1 ... N
) )  ->  (
( 1st `  ( 1st `  U ) ) `
 y )  e.  CC )
186139, 185syldan 473 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( ( 1st `  ( 1st `  U
) ) `  y
)  e.  CC )
187186addid1d 9835 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( ( ( 1st `  ( 1st `  U ) ) `  y )  +  0 )  =  ( ( 1st `  ( 1st `  U ) ) `  y ) )
188132, 179, 1873eqtrd 2468 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( ( F `
 ( M  - 
1 ) ) `  y )  =  ( ( 1st `  ( 1st `  U ) ) `
 y ) )
18966, 188syldan 473 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  /\  -.  y  e.  (
( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) ) ) )  ->  ( ( F `  ( M  -  1 ) ) `
 y )  =  ( ( 1st `  ( 1st `  U ) ) `
 y ) )
190 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  ( 2nd `  t )  =  ( 2nd `  T
) )
191190breq2d 4433 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  T  ->  (
y  <  ( 2nd `  t )  <->  y  <  ( 2nd `  T ) ) )
192191ifbid 3932 . . . . . . . . . . . . . . . . 17  |-  ( t  =  T  ->  if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  =  if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) ) )
193192csbeq1d 3403 . . . . . . . . . . . . . . . 16  |-  ( 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 } ) ) ) )
194 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  ( 1st `  t )  =  ( 1st `  T
) )
195194fveq2d 5883 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  T  ->  ( 1st `  ( 1st `  t
) )  =  ( 1st `  ( 1st `  T ) ) )
196194fveq2d 5883 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  T  ->  ( 2nd `  ( 1st `  t
) )  =  ( 2nd `  ( 1st `  T ) ) )
197196imaeq1d 5184 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) ) )
198197xpeq1d 4874 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... j
) )  X.  {
1 } ) )
199196imaeq1d 5184 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) ) )
200199xpeq1d 4874 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )
201198, 200uneq12d 3622 . . . . . . . . . . . . . . . . . 18  |-  ( 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 } ) ) )
202195, 201oveq12d 6321 . . . . . . . . . . . . . . . . 17  |-  ( 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 } ) ) ) )
203202csbeq2dv 3810 . . . . . . . . . . . . . . . 16  |-  ( 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 } ) ) ) )
204193, 203eqtrd 2464 . . . . . . . . . . . . . . 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 } ) ) ) )
205204mpteq2dv 4509 . . . . . . . . . . . . . 14  |-  ( t  =  T  ->  (
y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )  =  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
206205eqeq2d 2437 . . . . . . . . . . . . 13  |-  ( t  =  T  ->  ( F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  t
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )  <->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) ) )
207206, 5elrab2 3232 . . . . . . . . . . . 12  |-  ( T  e.  S  <->  ( T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  /\  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) ) )
208207simprbi 466 . . . . . . . . . . 11  |-  ( T  e.  S  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
2093, 208syl 17 . . . . . . . . . 10  |-  ( ph  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
210 poimirlem11.3 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 2nd `  T
)  =  0 )
211 breq12 4426 . . . . . . . . . . . . . . . 16  |-  ( ( y  =  ( M  -  1 )  /\  ( 2nd `  T )  =  0 )  -> 
( y  <  ( 2nd `  T )  <->  ( M  -  1 )  <  0 ) )
212210, 211sylan2 477 . . . . . . . . . . . . . . 15  |-  ( ( y  =  ( M  -  1 )  /\  ph )  ->  ( y  <  ( 2nd `  T
)  <->  ( M  - 
1 )  <  0
) )
213212ancoms 455 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  (
y  <  ( 2nd `  T )  <->  ( M  -  1 )  <  0 ) )
214213, 95ifbieq2d 3935 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  =  if ( ( M  -  1 )  <  0 ,  y ,  M ) )
215214, 112eqtrd 2464 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  =  M )
216215csbeq1d 3403 . . . . . . . . . . 11  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  [_ if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  [_ M  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
217115imaeq2d 5185 . . . . . . . . . . . . . . . . 17  |-  ( j  =  M  ->  (
( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) ) )
218217xpeq1d 4874 . . . . . . . . . . . . . . . 16  |-  ( j  =  M  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... M
) )  X.  {
1 } ) )
219119imaeq2d 5185 . . . . . . . . . . . . . . . . 17  |-  ( j  =  M  ->  (
( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )
220219xpeq1d 4874 . . . . . . . . . . . . . . . 16  |-  ( j  =  M  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) )
221218, 220uneq12d 3622 . . . . . . . . . . . . . . 15  |-  ( j  =  M  ->  (
( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) )  =  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) ) )
222221oveq2d 6319 . . . . . . . . . . . . . 14  |-  ( j  =  M  ->  (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
223222adantl 468 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  =  M )  ->  (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
22445, 223csbied 3423 . . . . . . . . . . . 12  |-  ( ph  ->  [_ M  /  j ]_ ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
225224adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  [_ M  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
226216, 225eqtrd 2464 . . . . . . . . . 10  |-  ( (
ph  /\  y  =  ( M  -  1
) )  ->  [_ if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
227 ovex 6331 . . . . . . . . . . 11  |-  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) ) )  e.  _V
228227a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  e.  _V )
229209, 226, 102, 228fvmptd 5968 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( M  -  1 ) )  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) ) ) )
230229fveq1d 5881 . . . . . . . 8  |-  ( ph  ->  ( ( F `  ( M  -  1
) ) `  y
)  =  ( ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  y
) )
231230adantr 467 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) ) )  ->  ( ( F `
 ( M  - 
1 ) ) `  y )  =  ( ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  y
) )
23220sselda 3465 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) ) )  ->  y  e.  ( 1 ... N ) )
233 xp1st 6835 . . . . . . . . . . . 12  |-  ( ( 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 ) ) )
2349, 233syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  (
1 ... N ) ) )
235 elmapfn 7500 . . . . . . . . . . 11  |-  ( ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) )  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
236234, 235syl 17 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
237236adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) ) )  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
238 fnconstg 5786 . . . . . . . . . . . . . 14  |-  ( 1  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) ) )
239145, 238ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )
240 fnconstg 5786 . . . . . . . . . . . . . 14  |-  ( 0  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )
241148, 240ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )
242239, 241pm3.2i 457 . . . . . . . . . . . 12  |-  ( ( ( ( 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 ) ) )
243 dff1o3 5835 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( ( 2nd `  ( 1st `  T
) ) : ( 1 ... N )
-onto-> ( 1 ... N
)  /\  Fun  `' ( 2nd `  ( 1st `  T ) ) ) )
244243simprbi 466 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  Fun  `' ( 2nd `  ( 1st `  T ) ) )
24515, 244syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  Fun  `' ( 2nd `  ( 1st `  T
) ) )
246 imain 5675 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) )
247245, 246syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) ) )
24857imaeq2d 5185 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  ( ( 2nd `  ( 1st `  T ) )
" (/) ) )
249 ima0 5200 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  ( 1st `  T ) ) " (/) )  =  (/)
250248, 249syl6eq 2480 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  (/) )
251247, 250eqtr3d 2466 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )  =  (/) )
252 fnun 5698 . . . . . . . . . . . 12  |-  ( ( ( ( ( ( 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 ) ) ) )
253242, 251, 252sylancr 668 . . . . . . . . . . 11  |-  ( 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 ) ) ) )
254 imaundi 5265 . . . . . . . . . . . . 13  |-  ( ( 2nd `  ( 1st `  T ) ) "
( ( 1 ... M )  u.  (
( M  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )
25547imaeq2d 5185 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( ( 2nd `