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

Theorem poimirlem12 31872
Description: Lemma for poimir 31893 connecting walks that could yield from a given cube a given face opposite the final 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 )
poimirlem12.3  |-  ( ph  ->  ( 2nd `  T
)  =  N )
poimirlem12.4  |-  ( ph  ->  U  e.  S )
poimirlem12.5  |-  ( ph  ->  ( 2nd `  U
)  =  N )
poimirlem12.6  |-  ( ph  ->  M  e.  ( 0 ... ( N  - 
1 ) ) )
Assertion
Ref Expression
poimirlem12  |-  ( 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 poimirlem12
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 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  T  e.  S )
4 elrabi 3227 . . . . . . . . . . . . . . . . 17  |-  ( 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 . . . . . . . . . . . . . . . . 17  |-  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 . . . . . . . . . . . . . . . 16  |-  ( T  e.  S  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) ) )
7 xp1st 6835 . . . . . . . . . . . . . . . 16  |-  ( 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 ) } ) )
83, 6, 73syl 18 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  T
)  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )
9 xp2nd 6836 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) } )
108, 9syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
11 fvex 5889 . . . . . . . . . . . . . . 15  |-  ( 2nd `  ( 1st `  T
) )  e.  _V
12 f1oeq1 5820 . . . . . . . . . . . . . . 15  |-  ( f  =  ( 2nd `  ( 1st `  T ) )  ->  ( f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
1311, 12elab 3219 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  ( 1st `  T ) )  e. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) }  <->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
1410, 13sylib 200 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
15 f1of 5829 . . . . . . . . . . . . 13  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) --> ( 1 ... N
) )
16 frn 5750 . . . . . . . . . . . . 13  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
) --> ( 1 ... N )  ->  ran  ( 2nd `  ( 1st `  T ) )  C_  ( 1 ... N
) )
1714, 15, 163syl 18 . . . . . . . . . . . 12  |-  ( ph  ->  ran  ( 2nd `  ( 1st `  T ) ) 
C_  ( 1 ... N ) )
182, 17syl5ss 3476 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  C_  ( 1 ... N
) )
19 poimirlem12.4 . . . . . . . . . . . . . . 15  |-  ( ph  ->  U  e.  S )
20 elrabi 3227 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) )
2120, 5eleq2s 2531 . . . . . . . . . . . . . . 15  |-  ( U  e.  S  ->  U  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) ) )
22 xp1st 6835 . . . . . . . . . . . . . . 15  |-  ( 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 ) } ) )
2319, 21, 223syl 18 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  U
)  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )
24 xp2nd 6836 . . . . . . . . . . . . . 14  |-  ( ( 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 ) } )
2523, 24syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2nd `  ( 1st `  U ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
26 fvex 5889 . . . . . . . . . . . . . 14  |-  ( 2nd `  ( 1st `  U
) )  e.  _V
27 f1oeq1 5820 . . . . . . . . . . . . . 14  |-  ( f  =  ( 2nd `  ( 1st `  U ) )  ->  ( f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  ( 1st `  U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
2826, 27elab 3219 . . . . . . . . . . . . 13  |-  ( ( 2nd `  ( 1st `  U ) )  e. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) }  <->  ( 2nd `  ( 1st `  U
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
2925, 28sylib 200 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2nd `  ( 1st `  U ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
30 f1ofo 5836 . . . . . . . . . . . 12  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  U
) ) : ( 1 ... N )
-onto-> ( 1 ... N
) )
31 foima 5813 . . . . . . . . . . . 12  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
) -onto-> ( 1 ... N )  ->  (
( 2nd `  ( 1st `  U ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
3229, 30, 313syl 18 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
3318, 32sseqtr4d 3502 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  C_  ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... N ) ) )
3433ssdifd 3602 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) ) 
\  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) ) )  C_  ( (
( 2nd `  ( 1st `  U ) )
" ( 1 ... N ) )  \ 
( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) ) ) )
35 dff1o3 5835 . . . . . . . . . . . 12  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( ( 2nd `  ( 1st `  U
) ) : ( 1 ... N )
-onto-> ( 1 ... N
)  /\  Fun  `' ( 2nd `  ( 1st `  U ) ) ) )
3635simprbi 466 . . . . . . . . . . 11  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  Fun  `' ( 2nd `  ( 1st `  U ) ) )
37 imadif 5674 . . . . . . . . . . 11  |-  ( Fun  `' ( 2nd `  ( 1st `  U ) )  ->  ( ( 2nd `  ( 1st `  U
) ) " (
( 1 ... N
)  \  ( 1 ... M ) ) )  =  ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... N ) )  \ 
( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) ) ) )
3829, 36, 373syl 18 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( ( 1 ... N )  \ 
( 1 ... M
) ) )  =  ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... N ) ) 
\  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) ) ) )
39 difun2 3876 . . . . . . . . . . . 12  |-  ( ( ( ( M  + 
1 ) ... N
)  u.  ( 1 ... M ) ) 
\  ( 1 ... M ) )  =  ( ( ( M  +  1 ) ... N )  \  (
1 ... M ) )
40 poimirlem12.6 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  ( 0 ... ( N  - 
1 ) ) )
41 elfznn0 11889 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  ( 0 ... ( N  -  1 ) )  ->  M  e.  NN0 )
42 nn0p1nn 10911 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  NN0  ->  ( M  +  1 )  e.  NN )
4340, 41, 423syl 18 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( M  +  1 )  e.  NN )
44 nnuz 11196 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
4543, 44syl6eleq 2521 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( M  +  1 )  e.  ( ZZ>= ` 
1 ) )
46 poimir.0 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  NN )
4746nncnd 10627 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  N  e.  CC )
48 npcan1 10046 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
4947, 48syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
50 elfzuz3 11799 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  ( 0 ... ( N  -  1 ) )  ->  ( N  -  1 )  e.  ( ZZ>= `  M
) )
51 peano2uz 11214 . . . . . . . . . . . . . . . . 17  |-  ( ( N  -  1 )  e.  ( ZZ>= `  M
)  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  M )
)
5240, 50, 513syl 18 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  e.  ( ZZ>= `  M ) )
5349, 52eqeltrrd 2512 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  ( ZZ>= `  M ) )
54 fzsplit2 11826 . . . . . . . . . . . . . . 15  |-  ( ( ( M  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ( ZZ>= `  M )
)  ->  ( 1 ... N )  =  ( ( 1 ... M )  u.  (
( M  +  1 ) ... N ) ) )
5545, 53, 54syl2anc 666 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1 ... N
)  =  ( ( 1 ... M )  u.  ( ( M  +  1 ) ... N ) ) )
56 uncom 3611 . . . . . . . . . . . . . 14  |-  ( ( 1 ... M )  u.  ( ( M  +  1 ) ... N ) )  =  ( ( ( M  +  1 ) ... N )  u.  (
1 ... M ) )
5755, 56syl6eq 2480 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 1 ... N
)  =  ( ( ( M  +  1 ) ... N )  u.  ( 1 ... M ) ) )
5857difeq1d 3583 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 1 ... N )  \  (
1 ... M ) )  =  ( ( ( ( M  +  1 ) ... N )  u.  ( 1 ... M ) )  \ 
( 1 ... M
) ) )
59 incom 3656 . . . . . . . . . . . . . 14  |-  ( ( ( M  +  1 ) ... N )  i^i  ( 1 ... M ) )  =  ( ( 1 ... M )  i^i  (
( M  +  1 ) ... N ) )
6040, 41syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  e.  NN0 )
6160nn0red 10928 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  e.  RR )
6261ltp1d 10539 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  <  ( M  +  1 ) )
63 fzdisj 11828 . . . . . . . . . . . . . . 15  |-  ( M  <  ( M  + 
1 )  ->  (
( 1 ... M
)  i^i  ( ( M  +  1 ) ... N ) )  =  (/) )
6462, 63syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1 ... M )  i^i  (
( M  +  1 ) ... N ) )  =  (/) )
6559, 64syl5eq 2476 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( M  +  1 ) ... N )  i^i  (
1 ... M ) )  =  (/) )
66 disj3 3838 . . . . . . . . . . . . 13  |-  ( ( ( ( M  + 
1 ) ... N
)  i^i  ( 1 ... M ) )  =  (/)  <->  ( ( M  +  1 ) ... N )  =  ( ( ( M  + 
1 ) ... N
)  \  ( 1 ... M ) ) )
6765, 66sylib 200 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( M  + 
1 ) ... N
)  =  ( ( ( M  +  1 ) ... N ) 
\  ( 1 ... M ) ) )
6839, 58, 673eqtr4a 2490 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 1 ... N )  \  (
1 ... M ) )  =  ( ( M  +  1 ) ... N ) )
6968imaeq2d 5185 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( ( 1 ... N )  \ 
( 1 ... M
) ) )  =  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )
7038, 69eqtr3d 2466 . . . . . . . . 9  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... N ) ) 
\  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) ) )  =  ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) ) )
7134, 70sseqtrd 3501 . . . . . . . 8  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) ) 
\  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) ) )  C_  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) ) )
7271sselda 3465 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) ) 
\  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) ) ) )  ->  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )
731, 72sylan2br 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 ) ) )
74 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  U  ->  ( 2nd `  t )  =  ( 2nd `  U
) )
7574breq2d 4433 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  U  ->  (
y  <  ( 2nd `  t )  <->  y  <  ( 2nd `  U ) ) )
7675ifbid 3932 . . . . . . . . . . . . . . . . 17  |-  ( t  =  U  ->  if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  =  if ( y  <  ( 2nd `  U
) ,  y ,  ( y  +  1 ) ) )
7776csbeq1d 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 } ) ) ) )
78 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  U  ->  ( 1st `  t )  =  ( 1st `  U
) )
7978fveq2d 5883 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  U  ->  ( 1st `  ( 1st `  t
) )  =  ( 1st `  ( 1st `  U ) ) )
8078fveq2d 5883 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  U  ->  ( 2nd `  ( 1st `  t
) )  =  ( 2nd `  ( 1st `  U ) ) )
8180imaeq1d 5184 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  U  ->  (
( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... j ) ) )
8281xpeq1d 4874 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  U  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  U ) ) "
( 1 ... j
) )  X.  {
1 } ) )
8380imaeq1d 5184 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  U  ->  (
( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) ) )
8483xpeq1d 4874 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  U  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )
8582, 84uneq12d 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 } ) ) )
8679, 85oveq12d 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 } ) ) ) )
8786csbeq2dv 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 } ) ) ) )
8877, 87eqtrd 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 } ) ) ) )
8988mpteq2dv 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 } ) ) ) ) )
9089eqeq2d 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 } ) ) ) ) ) )
9190, 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 } ) ) ) ) ) )
9291simprbi 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 } ) ) ) ) )
9319, 92syl 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 } ) ) ) ) )
94 breq1 4424 . . . . . . . . . . . . . 14  |-  ( y  =  M  ->  (
y  <  ( 2nd `  U )  <->  M  <  ( 2nd `  U ) ) )
95 id 23 . . . . . . . . . . . . . 14  |-  ( y  =  M  ->  y  =  M )
9694, 95ifbieq1d 3933 . . . . . . . . . . . . 13  |-  ( y  =  M  ->  if ( y  <  ( 2nd `  U ) ,  y ,  ( y  +  1 ) )  =  if ( M  <  ( 2nd `  U
) ,  M , 
( y  +  1 ) ) )
9746nnred 10626 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  N  e.  RR )
98 peano2rem 9943 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  RR  ->  ( N  -  1 )  e.  RR )
9997, 98syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  -  1 )  e.  RR )
100 elfzle2 11805 . . . . . . . . . . . . . . . . 17  |-  ( M  e.  ( 0 ... ( N  -  1 ) )  ->  M  <_  ( N  -  1 ) )
10140, 100syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  M  <_  ( N  -  1 ) )
10297ltm1d 10541 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  -  1 )  <  N )
10361, 99, 97, 101, 102lelttrd 9795 . . . . . . . . . . . . . . 15  |-  ( ph  ->  M  <  N )
104 poimirlem12.5 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 2nd `  U
)  =  N )
105103, 104breqtrrd 4448 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  <  ( 2nd `  U ) )
106105iftrued 3918 . . . . . . . . . . . . 13  |-  ( ph  ->  if ( M  < 
( 2nd `  U
) ,  M , 
( y  +  1 ) )  =  M )
10796, 106sylan9eqr 2486 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  =  M )  ->  if ( y  <  ( 2nd `  U ) ,  y ,  ( y  +  1 ) )  =  M )
108107csbeq1d 3403 . . . . . . . . . . 11  |-  ( (
ph  /\  y  =  M )  ->  [_ 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 } ) ) ) )
109 oveq2 6311 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  M  ->  (
1 ... j )  =  ( 1 ... M
) )
110109imaeq2d 5185 . . . . . . . . . . . . . . . . 17  |-  ( j  =  M  ->  (
( 2nd `  ( 1st `  U ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) ) )
111110xpeq1d 4874 . . . . . . . . . . . . . . . 16  |-  ( j  =  M  ->  (
( ( 2nd `  ( 1st `  U ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  U ) ) "
( 1 ... M
) )  X.  {
1 } ) )
112 oveq1 6310 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  M  ->  (
j  +  1 )  =  ( M  + 
1 ) )
113112oveq1d 6318 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  M  ->  (
( j  +  1 ) ... N )  =  ( ( M  +  1 ) ... N ) )
114113imaeq2d 5185 . . . . . . . . . . . . . . . . 17  |-  ( j  =  M  ->  (
( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )
115114xpeq1d 4874 . . . . . . . . . . . . . . . 16  |-  ( j  =  M  ->  (
( ( 2nd `  ( 1st `  U ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) )
116111, 115uneq12d 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 } ) ) )
117116oveq2d 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 } ) ) ) )
118117adantl 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 } ) ) ) )
11940, 118csbied 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 } ) ) ) )
120119adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  y  =  M )  ->  [_ 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 } ) ) ) )
121108, 120eqtrd 2464 . . . . . . . . . 10  |-  ( (
ph  /\  y  =  M )  ->  [_ 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 } ) ) ) )
122 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
123122a1i 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 )
12493, 121, 40, 123fvmptd 5968 . . . . . . . . 9  |-  ( ph  ->  ( F `  M
)  =  ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) ) ) )
125124fveq1d 5881 . . . . . . . 8  |-  ( ph  ->  ( ( F `  M ) `  y
)  =  ( ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  y
) )
126125adantr 467 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( ( F `
 M ) `  y )  =  ( ( ( 1st `  ( 1st `  U ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  y
) )
127 imassrn 5196 . . . . . . . . . 10  |-  ( ( 2nd `  ( 1st `  U ) ) "
( ( M  + 
1 ) ... N
) )  C_  ran  ( 2nd `  ( 1st `  U ) )
128 f1of 5829 . . . . . . . . . . 11  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  U
) ) : ( 1 ... N ) --> ( 1 ... N
) )
129 frn 5750 . . . . . . . . . . 11  |-  ( ( 2nd `  ( 1st `  U ) ) : ( 1 ... N
) --> ( 1 ... N )  ->  ran  ( 2nd `  ( 1st `  U ) )  C_  ( 1 ... N
) )
13029, 128, 1293syl 18 . . . . . . . . . 10  |-  ( ph  ->  ran  ( 2nd `  ( 1st `  U ) ) 
C_  ( 1 ... N ) )
131127, 130syl5ss 3476 . . . . . . . . 9  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  C_  ( 1 ... N
) )
132131sselda 3465 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  y  e.  ( 1 ... N ) )
133 xp1st 6835 . . . . . . . . . . 11  |-  ( ( 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 ) ) )
134 elmapfn 7500 . . . . . . . . . . 11  |-  ( ( 1st `  ( 1st `  U ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) )  ->  ( 1st `  ( 1st `  U ) )  Fn  ( 1 ... N ) )
13523, 133, 1343syl 18 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  ( 1st `  U ) )  Fn  ( 1 ... N ) )
136135adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( 1st `  ( 1st `  U ) )  Fn  ( 1 ... N ) )
137 1ex 9640 . . . . . . . . . . . . . 14  |-  1  e.  _V
138 fnconstg 5786 . . . . . . . . . . . . . 14  |-  ( 1  e.  _V  ->  (
( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) ) )
139137, 138ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )
140 c0ex 9639 . . . . . . . . . . . . . 14  |-  0  e.  _V
141 fnconstg 5786 . . . . . . . . . . . . . 14  |-  ( 0  e.  _V  ->  (
( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) ) )
142140, 141ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) )
143139, 142pm3.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 ) ) )
144 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 ) ) ) )
14529, 36, 1443syl 18 . . . . . . . . . . . . 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 ) ) ) )
14664imaeq2d 5185 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  ( ( 2nd `  ( 1st `  U ) )
" (/) ) )
147 ima0 5200 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  ( 1st `  U ) ) " (/) )  =  (/)
148146, 147syl6eq 2480 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  (/) )
149145, 148eqtr3d 2466 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  i^i  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) ) )  =  (/) )
150 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 ) ) ) )
151143, 149, 150sylancr 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 ) ) ) )
152 imaundi 5265 . . . . . . . . . . . . 13  |-  ( ( 2nd `  ( 1st `  U ) ) "
( ( 1 ... M )  u.  (
( M  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) )  u.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )
15355imaeq2d 5185 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( 1 ... N ) )  =  ( ( 2nd `  ( 1st `  U ) )
" ( ( 1 ... M )  u.  ( ( M  + 
1 ) ... N
) ) ) )
154153, 32eqtr3d 2466 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  ( 1st `  U ) )
" ( ( 1 ... M )  u.  ( ( M  + 
1 ) ... N
) ) )  =  ( 1 ... N
) )
155152, 154syl5eqr 2478 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  U
) ) " (
1 ... M ) )  u.  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
156155fneq2d 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
) ) )
157151, 156mpbid 214 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( 2nd `  ( 1st `  U ) ) "
( 1 ... M
) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  ( 1 ... N
) )
158157adantr 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 ) )
159 ovex 6331 . . . . . . . . . 10  |-  ( 1 ... N )  e. 
_V
160159a1i 11 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( 1 ... N )  e.  _V )
161 inidm 3672 . . . . . . . . 9  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
162 eqidd 2424 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  /\  y  e.  ( 1 ... N ) )  ->  ( ( 1st `  ( 1st `  U
) ) `  y
)  =  ( ( 1st `  ( 1st `  U ) ) `  y ) )
163 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 ) )
164139, 142, 163mp3an12 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 ) )
165149, 164sylan 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 ) )
166140fvconst2 6133 . . . . . . . . . . . 12  |-  ( y  e.  ( ( 2nd `  ( 1st `  U
) ) " (
( M  +  1 ) ... N ) )  ->  ( (
( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) `
 y )  =  0 )
167166adantl 468 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( ( ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) `
 y )  =  0 )
168165, 167eqtrd 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 )
169168adantr 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 )
170136, 158, 160, 160, 161, 162, 169ofval 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 ) )
171132, 170mpdan 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 ) )
172 elmapi 7499 . . . . . . . . . . . . 13  |-  ( ( 1st `  ( 1st `  U ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) )  ->  ( 1st `  ( 1st `  U ) ) : ( 1 ... N ) --> ( 0..^ K ) )
17323, 133, 1723syl 18 . . . . . . . . . . . 12  |-  ( ph  ->  ( 1st `  ( 1st `  U ) ) : ( 1 ... N ) --> ( 0..^ K ) )
174173ffvelrnda 6035 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( 1 ... N
) )  ->  (
( 1st `  ( 1st `  U ) ) `
 y )  e.  ( 0..^ K ) )
175 elfzonn0 11962 . . . . . . . . . . 11  |-  ( ( ( 1st `  ( 1st `  U ) ) `
 y )  e.  ( 0..^ K )  ->  ( ( 1st `  ( 1st `  U
) ) `  y
)  e.  NN0 )
176174, 175syl 17 . . . . . . . . . 10  |-  ( (
ph  /\  y  e.  ( 1 ... N
) )  ->  (
( 1st `  ( 1st `  U ) ) `
 y )  e. 
NN0 )
177176nn0cnd 10929 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( 1 ... N
) )  ->  (
( 1st `  ( 1st `  U ) ) `
 y )  e.  CC )
178177addid1d 9835 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( 1 ... N
) )  ->  (
( ( 1st `  ( 1st `  U ) ) `
 y )  +  0 )  =  ( ( 1st `  ( 1st `  U ) ) `
 y ) )
179132, 178syldan 473 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( ( ( 1st `  ( 1st `  U ) ) `  y )  +  0 )  =  ( ( 1st `  ( 1st `  U ) ) `  y ) )
180126, 171, 1793eqtrd 2468 . . . . . 6  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  U ) )
" ( ( M  +  1 ) ... N ) ) )  ->  ( ( F `
 M ) `  y )  =  ( ( 1st `  ( 1st `  U ) ) `
 y ) )
18173, 180syldan 473 . . . . 5  |-  ( (
ph  /\  ( y  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  /\  -.  y  e.  (
( 2nd `  ( 1st `  U ) )
" ( 1 ... M ) ) ) )  ->  ( ( F `  M ) `  y )  =  ( ( 1st `  ( 1st `  U ) ) `
 y ) )
182 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  ( 2nd `  t )  =  ( 2nd `  T
) )
183182breq2d 4433 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  T  ->  (
y  <  ( 2nd `  t )  <->  y  <  ( 2nd `  T ) ) )
184183ifbid 3932 . . . . . . . . . . . . . . . . 17  |-  ( t  =  T  ->  if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  =  if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) ) )
185184csbeq1d 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 } ) ) ) )
186 fveq2 5879 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  ( 1st `  t )  =  ( 1st `  T
) )
187186fveq2d 5883 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  T  ->  ( 1st `  ( 1st `  t
) )  =  ( 1st `  ( 1st `  T ) ) )
188186fveq2d 5883 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  T  ->  ( 2nd `  ( 1st `  t
) )  =  ( 2nd `  ( 1st `  T ) ) )
189188imaeq1d 5184 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) ) )
190189xpeq1d 4874 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... j
) )  X.  {
1 } ) )
191188imaeq1d 5184 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) ) )
192191xpeq1d 4874 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )
193190, 192uneq12d 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 } ) ) )
194187, 193oveq12d 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 } ) ) ) )
195194csbeq2dv 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 } ) ) ) )
196185, 195eqtrd 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 } ) ) ) )
197196mpteq2dv 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 } ) ) ) ) )
198197eqeq2d 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 } ) ) ) ) ) )
199198, 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 } ) ) ) ) ) )
200199simprbi 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 } ) ) ) ) )
2013, 200syl 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 } ) ) ) ) )
202 breq1 4424 . . . . . . . . . . . . . 14  |-  ( y  =  M  ->  (
y  <  ( 2nd `  T )  <->  M  <  ( 2nd `  T ) ) )
203202, 95ifbieq1d 3933 . . . . . . . . . . . . 13  |-  ( y  =  M  ->  if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  =  if ( M  <  ( 2nd `  T
) ,  M , 
( y  +  1 ) ) )
204 poimirlem12.3 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 2nd `  T
)  =  N )
205103, 204breqtrrd 4448 . . . . . . . . . . . . . 14  |-  ( ph  ->  M  <  ( 2nd `  T ) )
206205iftrued 3918 . . . . . . . . . . . . 13  |-  ( ph  ->  if ( M  < 
( 2nd `  T
) ,  M , 
( y  +  1 ) )  =  M )
207203, 206sylan9eqr 2486 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  =  M )  ->  if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  =  M )
208207csbeq1d 3403 . . . . . . . . . . 11  |-  ( (
ph  /\  y  =  M )  ->  [_ if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  [_ M  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
209109imaeq2d 5185 . . . . . . . . . . . . . . . . 17  |-  ( j  =  M  ->  (
( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) ) )
210209xpeq1d 4874 . . . . . . . . . . . . . . . 16  |-  ( j  =  M  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... M
) )  X.  {
1 } ) )
211113imaeq2d 5185 . . . . . . . . . . . . . . . . 17  |-  ( j  =  M  ->  (
( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )
212211xpeq1d 4874 . . . . . . . . . . . . . . . 16  |-  ( j  =  M  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) )
213210, 212uneq12d 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 } ) ) )
214213oveq2d 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 } ) ) ) )
215214adantl 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 } ) ) ) )
21640, 215csbied 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 } ) ) ) )
217216adantr 467 . . . . . . . . . . 11  |-  ( (
ph  /\  y  =  M )  ->  [_ M  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
218208, 217eqtrd 2464 . . . . . . . . . 10  |-  ( (
ph  /\  y  =  M )  ->  [_ if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
219 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
220219a1i 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 )
221201, 218, 40, 220fvmptd 5968 . . . . . . . . 9  |-  ( ph  ->  ( F `  M
)  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( M  + 
1 ) ... N
) )  X.  {
0 } ) ) ) )
222221fveq1d 5881 . . . . . . . 8  |-  ( ph  ->  ( ( F `  M ) `  y
)  =  ( ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  y
) )
223222adantr 467 . . . . . . 7  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) ) )  ->  ( ( F `
 M ) `  y )  =  ( ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  y
) )
22418sselda 3465 . . . . . . . 8  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) ) )  ->  y  e.  ( 1 ... N ) )
225 xp1st 6835 . . . . . . . . . . 11  |-  ( ( 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 ) ) )
226 elmapfn 7500 . . . . . . . . . . 11  |-  ( ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) )  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
2278, 225, 2263syl 18 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
228227adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) ) )  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
229 fnconstg 5786 . . . . . . . . . . . . . 14  |-  ( 1  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) ) )
230137, 229ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )
231 fnconstg 5786 . . . . . . . . . . . . . 14  |-  ( 0  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )
232140, 231ax-mp 5 . . . . . . . . . . . . 13  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )
233230, 232pm3.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 ) ) )
234 dff1o3 5835 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( ( 2nd `  ( 1st `  T
) ) : ( 1 ... N )
-onto-> ( 1 ... N
)  /\  Fun  `' ( 2nd `  ( 1st `  T ) ) ) )
235234simprbi 466 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  Fun  `' ( 2nd `  ( 1st `  T ) ) )
236 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 ) ) ) )
23714, 235, 2363syl 18 . . . . . . . . . . . . 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 ) ) ) )
23864imaeq2d 5185 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  ( ( 2nd `  ( 1st `  T ) )
" (/) ) )
239 ima0 5200 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  ( 1st `  T ) ) " (/) )  =  (/)
240238, 239syl6eq 2480 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  i^i  ( ( M  + 
1 ) ... N
) ) )  =  (/) )
241237, 240eqtr3d 2466 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )  =  (/) )
242 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 ) ) ) )
243233, 241, 242sylancr 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 ) ) ) )
244 imaundi 5265 . . . . . . . . . . . . 13  |-  ( ( 2nd `  ( 1st `  T ) ) "
( ( 1 ... M )  u.  (
( M  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... M ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( M  +  1 ) ... N ) ) )
24555imaeq2d 5185 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  u.  ( ( M  + 
1 ) ... N
) ) ) )
246 f1ofo 5836 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N )
-onto-> ( 1 ... N
) )
247 foima 5813 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
) -onto-> ( 1 ... N )  ->  (
( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
24814, 246, 2473syl 18 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
249245, 248eqtr3d 2466 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... M )  u.  ( ( M  + 
1 ) ... N
) ) )  =  ( 1 ... N
) )
250244, 249syl5eqr 2478 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... M ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
251250fneq2d 5683 . . . . . . . . . . 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 ) ) )  <-> 
( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... M
) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  ( 1 ... N
) ) )
252243, 251mpbid 214 . . . . . . . . . 10  |-  ( ph  ->  ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... M
) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( M  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  ( 1 ... N
) )
253252adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  y  e.  ( ( 2nd `  ( 1st `  T )