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

Theorem poimirlem4 31858
Description: Lemma for poimir 31887 connecting the admissible faces on the back face of the  ( M  + 
1 )-cube to admissible simplices in the  M-cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0  |-  ( ph  ->  N  e.  NN )
poimirlem4.1  |-  ( ph  ->  K  e.  NN )
poimirlem4.2  |-  ( ph  ->  M  e.  NN0 )
poimirlem4.3  |-  ( ph  ->  M  <  N )
Assertion
Ref Expression
poimirlem4  |-  ( ph  ->  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } )  |  A. i  e.  ( 0 ... M
) E. j  e.  ( 0 ... M
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B }  ~~  { s  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } )  |  ( A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  /\  (
( 1st `  s
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  s
) `  ( M  +  1 ) )  =  ( M  + 
1 ) ) } )
Distinct variable groups:    f, i,
j, p, s    ph, j    j, M    j, N    ph, i, p, s    B, f, i, j, s    f, K, i, j, p, s   
f, M, i, p, s    f, N, i, p, s
Allowed substitution hints:    ph( f)    B( p)

Proof of Theorem poimirlem4
Dummy variables  k  n  t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poimir.0 . . . . . . . 8  |-  ( ph  ->  N  e.  NN )
21adantr 466 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( ( ( 0..^ K )  ^m  (
1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )  ->  N  e.  NN )
3 poimirlem4.1 . . . . . . . 8  |-  ( ph  ->  K  e.  NN )
43adantr 466 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( ( ( 0..^ K )  ^m  (
1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )  ->  K  e.  NN )
5 poimirlem4.2 . . . . . . . 8  |-  ( ph  ->  M  e.  NN0 )
65adantr 466 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( ( ( 0..^ K )  ^m  (
1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )  ->  M  e.  NN0 )
7 poimirlem4.3 . . . . . . . 8  |-  ( ph  ->  M  <  N )
87adantr 466 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( ( ( 0..^ K )  ^m  (
1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )  ->  M  <  N )
9 xp1st 6834 . . . . . . . . 9  |-  ( t  e.  ( ( ( 0..^ K )  ^m  ( 1 ... M
) )  X.  {
f  |  f : ( 1 ... M
)
-1-1-onto-> ( 1 ... M
) } )  -> 
( 1st `  t
)  e.  ( ( 0..^ K )  ^m  ( 1 ... M
) ) )
10 elmapi 7498 . . . . . . . . 9  |-  ( ( 1st `  t )  e.  ( ( 0..^ K )  ^m  (
1 ... M ) )  ->  ( 1st `  t
) : ( 1 ... M ) --> ( 0..^ K ) )
119, 10syl 17 . . . . . . . 8  |-  ( t  e.  ( ( ( 0..^ K )  ^m  ( 1 ... M
) )  X.  {
f  |  f : ( 1 ... M
)
-1-1-onto-> ( 1 ... M
) } )  -> 
( 1st `  t
) : ( 1 ... M ) --> ( 0..^ K ) )
1211adantl 467 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( ( ( 0..^ K )  ^m  (
1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )  ->  ( 1st `  t ) : ( 1 ... M
) --> ( 0..^ K ) )
13 xp2nd 6835 . . . . . . . . 9  |-  ( t  e.  ( ( ( 0..^ K )  ^m  ( 1 ... M
) )  X.  {
f  |  f : ( 1 ... M
)
-1-1-onto-> ( 1 ... M
) } )  -> 
( 2nd `  t
)  e.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } )
14 fvex 5888 . . . . . . . . . 10  |-  ( 2nd `  t )  e.  _V
15 f1oeq1 5819 . . . . . . . . . 10  |-  ( f  =  ( 2nd `  t
)  ->  ( f : ( 1 ... M ) -1-1-onto-> ( 1 ... M
)  <->  ( 2nd `  t
) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) ) )
1614, 15elab 3218 . . . . . . . . 9  |-  ( ( 2nd `  t )  e.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) }  <-> 
( 2nd `  t
) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
1713, 16sylib 199 . . . . . . . 8  |-  ( t  e.  ( ( ( 0..^ K )  ^m  ( 1 ... M
) )  X.  {
f  |  f : ( 1 ... M
)
-1-1-onto-> ( 1 ... M
) } )  -> 
( 2nd `  t
) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
1817adantl 467 . . . . . . 7  |-  ( (
ph  /\  t  e.  ( ( ( 0..^ K )  ^m  (
1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )  ->  ( 2nd `  t ) : ( 1 ... M
)
-1-1-onto-> ( 1 ... M
) )
192, 4, 6, 8, 12, 18poimirlem3 31857 . . . . . 6  |-  ( (
ph  /\  t  e.  ( ( ( 0..^ K )  ^m  (
1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )  ->  ( A. i  e.  (
0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( 1st `  t
)  oF  +  ( ( ( ( 2nd `  t )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  t )
" ( ( j  +  1 ) ... M ) )  X. 
{ 0 } ) ) )  u.  (
( ( M  + 
1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  ->  ( <. ( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) >.  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } )  /\  ( A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } )  oF  +  ( ( ( ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  /\  (
( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 ( M  + 
1 ) )  =  0  /\  ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) `
 ( M  + 
1 ) )  =  ( M  +  1 ) ) ) ) )
20 fvex 5888 . . . . . . . . . . . . . . . 16  |-  ( 1st `  t )  e.  _V
21 snex 4659 . . . . . . . . . . . . . . . 16  |-  { <. ( M  +  1 ) ,  0 >. }  e.  _V
2220, 21unex 6600 . . . . . . . . . . . . . . 15  |-  ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } )  e.  _V
23 snex 4659 . . . . . . . . . . . . . . . 16  |-  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. }  e.  _V
2414, 23unex 6600 . . . . . . . . . . . . . . 15  |-  ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )  e.  _V
2522, 24op1std 6814 . . . . . . . . . . . . . 14  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( 1st `  s
)  =  ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) )
2622, 24op2ndd 6815 . . . . . . . . . . . . . . . . 17  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( 2nd `  s
)  =  ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) )
2726imaeq1d 5183 . . . . . . . . . . . . . . . 16  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( ( 2nd `  s ) " (
1 ... j ) )  =  ( ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) ) )
2827xpeq1d 4873 . . . . . . . . . . . . . . 15  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } ) )
2926imaeq1d 5183 . . . . . . . . . . . . . . . 16  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( ( 2nd `  s ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  =  ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) ) )
3029xpeq1d 4873 . . . . . . . . . . . . . . 15  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } )  =  ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) )
3128, 30uneq12d 3621 . . . . . . . . . . . . . 14  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) )  =  ( ( ( ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )
3225, 31oveq12d 6320 . . . . . . . . . . . . 13  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) )  =  ( ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } )  oF  +  ( ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) ) )
3332uneq1d 3619 . . . . . . . . . . . 12  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  =  ( ( ( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } )  oF  +  ( ( ( ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) ) )
3433csbeq1d 3402 . . . . . . . . . . 11  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B  =  [_ ( ( ( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } )  oF  +  ( ( ( ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B )
3534eqeq2d 2436 . . . . . . . . . 10  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( i  = 
[_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B  <->  i  =  [_ ( ( ( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } )  oF  +  ( ( ( ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B ) )
3635rexbidv 2939 . . . . . . . . 9  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( E. j  e.  ( 0 ... M
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B  <->  E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } )  oF  +  ( ( ( ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B ) )
3736ralbidv 2864 . . . . . . . 8  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( A. i  e.  ( 0 ... M
) E. j  e.  ( 0 ... M
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B  <->  A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } )  oF  +  ( ( ( ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B ) )
3825fveq1d 5880 . . . . . . . . 9  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( ( 1st `  s ) `  ( M  +  1 ) )  =  ( ( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 ( M  + 
1 ) ) )
3938eqeq1d 2424 . . . . . . . 8  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( ( ( 1st `  s ) `
 ( M  + 
1 ) )  =  0  <->  ( ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 ( M  + 
1 ) )  =  0 ) )
4026fveq1d 5880 . . . . . . . . 9  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( ( 2nd `  s ) `  ( M  +  1 ) )  =  ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) `
 ( M  + 
1 ) ) )
4140eqeq1d 2424 . . . . . . . 8  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( ( ( 2nd `  s ) `
 ( M  + 
1 ) )  =  ( M  +  1 )  <->  ( ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) `
 ( M  + 
1 ) )  =  ( M  +  1 ) ) )
4237, 39, 413anbi123d 1335 . . . . . . 7  |-  ( s  =  <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  ->  ( ( A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  /\  (
( 1st `  s
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  s
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  <->  ( A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } )  oF  +  ( ( ( ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  /\  (
( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 ( M  + 
1 ) )  =  0  /\  ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) `
 ( M  + 
1 ) )  =  ( M  +  1 ) ) ) )
4342elrab 3229 . . . . . 6  |-  ( <.
( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) >.  e.  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X. 
{ f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  |  ( A. i  e.  ( 0 ... M
) E. j  e.  ( 0 ... M
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B  /\  ( ( 1st `  s
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  s
) `  ( M  +  1 ) )  =  ( M  + 
1 ) ) }  <-> 
( <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X.  {
f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  /\  ( A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ (
( ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } )  oF  +  ( ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  /\  (
( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 ( M  + 
1 ) )  =  0  /\  ( ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) `
 ( M  + 
1 ) )  =  ( M  +  1 ) ) ) )
4419, 43syl6ibr 230 . . . . 5  |-  ( (
ph  /\  t  e.  ( ( ( 0..^ K )  ^m  (
1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )  ->  ( A. i  e.  (
0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( 1st `  t
)  oF  +  ( ( ( ( 2nd `  t )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  t )
" ( ( j  +  1 ) ... M ) )  X. 
{ 0 } ) ) )  u.  (
( ( M  + 
1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  ->  <. (
( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) >.  e.  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X. 
{ f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  |  ( A. i  e.  ( 0 ... M
) E. j  e.  ( 0 ... M
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B  /\  ( ( 1st `  s
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  s
) `  ( M  +  1 ) )  =  ( M  + 
1 ) ) } ) )
4544ralrimiva 2839 . . . 4  |-  ( ph  ->  A. t  e.  ( ( ( 0..^ K )  ^m  ( 1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ( A. i  e.  ( 0 ... M
) E. j  e.  ( 0 ... M
) i  =  [_ ( ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B  -> 
<. ( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) >.  e.  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X. 
{ f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  |  ( A. i  e.  ( 0 ... M
) E. j  e.  ( 0 ... M
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B  /\  ( ( 1st `  s
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  s
) `  ( M  +  1 ) )  =  ( M  + 
1 ) ) } ) )
46 fveq2 5878 . . . . . . . . . . 11  |-  ( s  =  t  ->  ( 1st `  s )  =  ( 1st `  t
) )
47 fveq2 5878 . . . . . . . . . . . . . 14  |-  ( s  =  t  ->  ( 2nd `  s )  =  ( 2nd `  t
) )
4847imaeq1d 5183 . . . . . . . . . . . . 13  |-  ( s  =  t  ->  (
( 2nd `  s
) " ( 1 ... j ) )  =  ( ( 2nd `  t ) " (
1 ... j ) ) )
4948xpeq1d 4873 . . . . . . . . . . . 12  |-  ( s  =  t  ->  (
( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  =  ( ( ( 2nd `  t
) " ( 1 ... j ) )  X.  { 1 } ) )
5047imaeq1d 5183 . . . . . . . . . . . . 13  |-  ( s  =  t  ->  (
( 2nd `  s
) " ( ( j  +  1 ) ... M ) )  =  ( ( 2nd `  t ) " (
( j  +  1 ) ... M ) ) )
5150xpeq1d 4873 . . . . . . . . . . . 12  |-  ( s  =  t  ->  (
( ( 2nd `  s
) " ( ( j  +  1 ) ... M ) )  X.  { 0 } )  =  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) )
5249, 51uneq12d 3621 . . . . . . . . . . 11  |-  ( s  =  t  ->  (
( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) )  =  ( ( ( ( 2nd `  t ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) )
5346, 52oveq12d 6320 . . . . . . . . . 10  |-  ( s  =  t  ->  (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... M ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  t
)  oF  +  ( ( ( ( 2nd `  t )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  t )
" ( ( j  +  1 ) ... M ) )  X. 
{ 0 } ) ) ) )
5453uneq1d 3619 . . . . . . . . 9  |-  ( s  =  t  ->  (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... M ) )  X. 
{ 0 } ) ) )  u.  (
( ( M  + 
1 ) ... N
)  X.  { 0 } ) )  =  ( ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) ) )
5554csbeq1d 3402 . . . . . . . 8  |-  ( s  =  t  ->  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... M ) )  X. 
{ 0 } ) ) )  u.  (
( ( M  + 
1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  =  [_ ( ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
)
5655eqeq2d 2436 . . . . . . 7  |-  ( s  =  t  ->  (
i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... M ) )  X. 
{ 0 } ) ) )  u.  (
( ( M  + 
1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  i  =  [_ ( ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
) )
5756rexbidv 2939 . . . . . 6  |-  ( s  =  t  ->  ( E. j  e.  (
0 ... M ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... M ) )  X. 
{ 0 } ) ) )  u.  (
( ( M  + 
1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  E. j  e.  ( 0 ... M
) i  =  [_ ( ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
) )
5857ralbidv 2864 . . . . 5  |-  ( s  =  t  ->  ( A. i  e.  (
0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... M ) )  X. 
{ 0 } ) ) )  u.  (
( ( M  + 
1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  A. i  e.  ( 0 ... M
) E. j  e.  ( 0 ... M
) i  =  [_ ( ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
) )
5958ralrab 3233 . . . 4  |-  ( A. t  e.  { s  e.  ( ( ( 0..^ K )  ^m  (
1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } )  |  A. i  e.  ( 0 ... M
) E. j  e.  ( 0 ... M
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } <. ( ( 1st `  t )  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t
)  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  e.  { s  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } )  |  ( A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  /\  (
( 1st `  s
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  s
) `  ( M  +  1 ) )  =  ( M  + 
1 ) ) }  <->  A. t  e.  (
( ( 0..^ K )  ^m  ( 1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) ( A. i  e.  ( 0 ... M
) E. j  e.  ( 0 ... M
) i  =  [_ ( ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B  -> 
<. ( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) >.  e.  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X. 
{ f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  |  ( A. i  e.  ( 0 ... M
) E. j  e.  ( 0 ... M
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B  /\  ( ( 1st `  s
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  s
) `  ( M  +  1 ) )  =  ( M  + 
1 ) ) } ) )
6045, 59sylibr 215 . . 3  |-  ( ph  ->  A. t  e.  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... M ) )  X. 
{ f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M
) } )  | 
A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... M ) )  X. 
{ 0 } ) ) )  u.  (
( ( M  + 
1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B } <. ( ( 1st `  t
)  u.  { <. ( M  +  1 ) ,  0 >. } ) ,  ( ( 2nd `  t )  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) >.  e.  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X. 
{ f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  |  ( A. i  e.  ( 0 ... M
) E. j  e.  ( 0 ... M
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B  /\  ( ( 1st `  s
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  s
) `  ( M  +  1 ) )  =  ( M  + 
1 ) ) } )
61 xp1st 6834 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X.  {
f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  -> 
( 1st `  k
)  e.  ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) ) )
62 elmapi 7498 . . . . . . . . . . . . . . 15  |-  ( ( 1st `  k )  e.  ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  ->  ( 1st `  k
) : ( 1 ... ( M  + 
1 ) ) --> ( 0..^ K ) )
6361, 62syl 17 . . . . . . . . . . . . . 14  |-  ( k  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X.  {
f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  -> 
( 1st `  k
) : ( 1 ... ( M  + 
1 ) ) --> ( 0..^ K ) )
64 fzssp1 11842 . . . . . . . . . . . . . 14  |-  ( 1 ... M )  C_  ( 1 ... ( M  +  1 ) )
65 fssres 5763 . . . . . . . . . . . . . 14  |-  ( ( ( 1st `  k
) : ( 1 ... ( M  + 
1 ) ) --> ( 0..^ K )  /\  ( 1 ... M
)  C_  ( 1 ... ( M  + 
1 ) ) )  ->  ( ( 1st `  k )  |`  (
1 ... M ) ) : ( 1 ... M ) --> ( 0..^ K ) )
6663, 64, 65sylancl 666 . . . . . . . . . . . . 13  |-  ( k  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X.  {
f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  -> 
( ( 1st `  k
)  |`  ( 1 ... M ) ) : ( 1 ... M
) --> ( 0..^ K ) )
67 ovex 6330 . . . . . . . . . . . . . 14  |-  ( 0..^ K )  e.  _V
68 ovex 6330 . . . . . . . . . . . . . 14  |-  ( 1 ... M )  e. 
_V
6967, 68elmap 7505 . . . . . . . . . . . . 13  |-  ( ( ( 1st `  k
)  |`  ( 1 ... M ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... M ) )  <-> 
( ( 1st `  k
)  |`  ( 1 ... M ) ) : ( 1 ... M
) --> ( 0..^ K ) )
7066, 69sylibr 215 . . . . . . . . . . . 12  |-  ( k  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X.  {
f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  -> 
( ( 1st `  k
)  |`  ( 1 ... M ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... M ) ) )
7170ad2antlr 731 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  -> 
( ( 1st `  k
)  |`  ( 1 ... M ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... M ) ) )
72 xp2nd 6835 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X.  {
f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  -> 
( 2nd `  k
)  e.  { f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )
73 fvex 5888 . . . . . . . . . . . . . . . . . 18  |-  ( 2nd `  k )  e.  _V
74 f1oeq1 5819 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( 2nd `  k
)  ->  ( f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) )  <->  ( 2nd `  k
) : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) ) )
7573, 74elab 3218 . . . . . . . . . . . . . . . . 17  |-  ( ( 2nd `  k )  e.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) }  <-> 
( 2nd `  k
) : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) )
7672, 75sylib 199 . . . . . . . . . . . . . . . 16  |-  ( k  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X.  {
f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  -> 
( 2nd `  k
) : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) )
77 f1of1 5827 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  k ) : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) )  ->  ( 2nd `  k ) : ( 1 ... ( M  +  1 ) )
-1-1-> ( 1 ... ( M  +  1 ) ) )
7876, 77syl 17 . . . . . . . . . . . . . . 15  |-  ( k  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X.  {
f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  -> 
( 2nd `  k
) : ( 1 ... ( M  + 
1 ) ) -1-1-> ( 1 ... ( M  +  1 ) ) )
79 f1ores 5842 . . . . . . . . . . . . . . 15  |-  ( ( ( 2nd `  k
) : ( 1 ... ( M  + 
1 ) ) -1-1-> ( 1 ... ( M  +  1 ) )  /\  ( 1 ... M )  C_  (
1 ... ( M  + 
1 ) ) )  ->  ( ( 2nd `  k )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( 2nd `  k
) " ( 1 ... M ) ) )
8078, 64, 79sylancl 666 . . . . . . . . . . . . . 14  |-  ( k  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X.  {
f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  -> 
( ( 2nd `  k
)  |`  ( 1 ... M ) ) : ( 1 ... M
)
-1-1-onto-> ( ( 2nd `  k
) " ( 1 ... M ) ) )
8180ad2antlr 731 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  -> 
( ( 2nd `  k
)  |`  ( 1 ... M ) ) : ( 1 ... M
)
-1-1-onto-> ( ( 2nd `  k
) " ( 1 ... M ) ) )
82 dff1o3 5834 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2nd `  k ) : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) )  <->  ( ( 2nd `  k ) : ( 1 ... ( M  +  1 ) )
-onto-> ( 1 ... ( M  +  1 ) )  /\  Fun  `' ( 2nd `  k ) ) )
8382simprbi 465 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  k ) : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) )  ->  Fun  `' ( 2nd `  k ) )
84 imadif 5673 . . . . . . . . . . . . . . . . . 18  |-  ( Fun  `' ( 2nd `  k
)  ->  ( ( 2nd `  k ) "
( ( 1 ... ( M  +  1 ) )  \  {
( M  +  1 ) } ) )  =  ( ( ( 2nd `  k )
" ( 1 ... ( M  +  1 ) ) )  \ 
( ( 2nd `  k
) " { ( M  +  1 ) } ) ) )
8576, 83, 843syl 18 . . . . . . . . . . . . . . . . 17  |-  ( k  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X.  {
f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  -> 
( ( 2nd `  k
) " ( ( 1 ... ( M  +  1 ) ) 
\  { ( M  +  1 ) } ) )  =  ( ( ( 2nd `  k
) " ( 1 ... ( M  + 
1 ) ) ) 
\  ( ( 2nd `  k ) " {
( M  +  1 ) } ) ) )
8685ad2antlr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  -> 
( ( 2nd `  k
) " ( ( 1 ... ( M  +  1 ) ) 
\  { ( M  +  1 ) } ) )  =  ( ( ( 2nd `  k
) " ( 1 ... ( M  + 
1 ) ) ) 
\  ( ( 2nd `  k ) " {
( M  +  1 ) } ) ) )
87 f1ofo 5835 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2nd `  k ) : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) )  ->  ( 2nd `  k ) : ( 1 ... ( M  +  1 ) )
-onto-> ( 1 ... ( M  +  1 ) ) )
88 foima 5812 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2nd `  k ) : ( 1 ... ( M  +  1 ) ) -onto-> ( 1 ... ( M  + 
1 ) )  -> 
( ( 2nd `  k
) " ( 1 ... ( M  + 
1 ) ) )  =  ( 1 ... ( M  +  1 ) ) )
8976, 87, 883syl 18 . . . . . . . . . . . . . . . . . 18  |-  ( k  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X.  {
f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  -> 
( ( 2nd `  k
) " ( 1 ... ( M  + 
1 ) ) )  =  ( 1 ... ( M  +  1 ) ) )
9089ad2antlr 731 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  -> 
( ( 2nd `  k
) " ( 1 ... ( M  + 
1 ) ) )  =  ( 1 ... ( M  +  1 ) ) )
91 f1ofn 5829 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 2nd `  k ) : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) )  ->  ( 2nd `  k )  Fn  (
1 ... ( M  + 
1 ) ) )
9276, 91syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( k  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X.  {
f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  -> 
( 2nd `  k
)  Fn  ( 1 ... ( M  + 
1 ) ) )
93 nn0p1nn 10910 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M  e.  NN0  ->  ( M  +  1 )  e.  NN )
945, 93syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( M  +  1 )  e.  NN )
95 elfz1end 11830 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( M  +  1 )  e.  NN  <->  ( M  +  1 )  e.  ( 1 ... ( M  +  1 ) ) )
9694, 95sylib 199 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( M  +  1 )  e.  ( 1 ... ( M  + 
1 ) ) )
97 fnsnfv 5938 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 2nd `  k
)  Fn  ( 1 ... ( M  + 
1 ) )  /\  ( M  +  1
)  e.  ( 1 ... ( M  + 
1 ) ) )  ->  { ( ( 2nd `  k ) `
 ( M  + 
1 ) ) }  =  ( ( 2nd `  k ) " {
( M  +  1 ) } ) )
9892, 96, 97syl2anr 480 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  ->  { ( ( 2nd `  k
) `  ( M  +  1 ) ) }  =  ( ( 2nd `  k )
" { ( M  +  1 ) } ) )
99 sneq 4006 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 )  ->  { ( ( 2nd `  k
) `  ( M  +  1 ) ) }  =  { ( M  +  1 ) } )
10098, 99sylan9req 2484 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  -> 
( ( 2nd `  k
) " { ( M  +  1 ) } )  =  {
( M  +  1 ) } )
10190, 100difeq12d 3584 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  -> 
( ( ( 2nd `  k ) " (
1 ... ( M  + 
1 ) ) ) 
\  ( ( 2nd `  k ) " {
( M  +  1 ) } ) )  =  ( ( 1 ... ( M  + 
1 ) )  \  { ( M  + 
1 ) } ) )
10286, 101eqtrd 2463 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  -> 
( ( 2nd `  k
) " ( ( 1 ... ( M  +  1 ) ) 
\  { ( M  +  1 ) } ) )  =  ( ( 1 ... ( M  +  1 ) )  \  { ( M  +  1 ) } ) )
103 1z 10968 . . . . . . . . . . . . . . . . . . . . 21  |-  1  e.  ZZ
104 nn0uz 11194 . . . . . . . . . . . . . . . . . . . . . . 23  |-  NN0  =  ( ZZ>= `  0 )
105 1m1e0 10679 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1  -  1 )  =  0
106105fveq2i 5881 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ZZ>= `  ( 1  -  1 ) )  =  (
ZZ>= `  0 )
107104, 106eqtr4i 2454 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN0  =  ( ZZ>= `  ( 1  -  1 ) )
1085, 107syl6eleq 2520 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  M  e.  ( ZZ>= `  ( 1  -  1 ) ) )
109 fzsuc2 11854 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 1  e.  ZZ  /\  M  e.  ( ZZ>= `  ( 1  -  1 ) ) )  -> 
( 1 ... ( M  +  1 ) )  =  ( ( 1 ... M )  u.  { ( M  +  1 ) } ) )
110103, 108, 109sylancr 667 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( 1 ... ( M  +  1 ) )  =  ( ( 1 ... M )  u.  { ( M  +  1 ) } ) )
111110difeq1d 3582 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( 1 ... ( M  +  1 ) )  \  {
( M  +  1 ) } )  =  ( ( ( 1 ... M )  u. 
{ ( M  + 
1 ) } ) 
\  { ( M  +  1 ) } ) )
112 difun2 3875 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 1 ... M
)  u.  { ( M  +  1 ) } )  \  {
( M  +  1 ) } )  =  ( ( 1 ... M )  \  {
( M  +  1 ) } )
113111, 112syl6eq 2479 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 1 ... ( M  +  1 ) )  \  {
( M  +  1 ) } )  =  ( ( 1 ... M )  \  {
( M  +  1 ) } ) )
1145nn0red 10927 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  M  e.  RR )
115 ltp1 10444 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( M  e.  RR  ->  M  <  ( M  +  1 ) )
116 peano2re 9807 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( M  e.  RR  ->  ( M  +  1 )  e.  RR )
117 ltnle 9714 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( M  e.  RR  /\  ( M  +  1
)  e.  RR )  ->  ( M  < 
( M  +  1 )  <->  -.  ( M  +  1 )  <_  M ) )
118116, 117mpdan 672 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( M  e.  RR  ->  ( M  <  ( M  + 
1 )  <->  -.  ( M  +  1 )  <_  M ) )
119115, 118mpbid 213 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M  e.  RR  ->  -.  ( M  +  1
)  <_  M )
120114, 119syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  -.  ( M  + 
1 )  <_  M
)
121 elfzle2 11804 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( M  +  1 )  e.  ( 1 ... M )  ->  ( M  +  1 )  <_  M )
122120, 121nsyl 124 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  ( M  + 
1 )  e.  ( 1 ... M ) )
123 difsn 4131 . . . . . . . . . . . . . . . . . . 19  |-  ( -.  ( M  +  1 )  e.  ( 1 ... M )  -> 
( ( 1 ... M )  \  {
( M  +  1 ) } )  =  ( 1 ... M
) )
124122, 123syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 1 ... M )  \  {
( M  +  1 ) } )  =  ( 1 ... M
) )
125113, 124eqtrd 2463 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 1 ... ( M  +  1 ) )  \  {
( M  +  1 ) } )  =  ( 1 ... M
) )
126125imaeq2d 5184 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2nd `  k
) " ( ( 1 ... ( M  +  1 ) ) 
\  { ( M  +  1 ) } ) )  =  ( ( 2nd `  k
) " ( 1 ... M ) ) )
127126ad2antrr 730 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  -> 
( ( 2nd `  k
) " ( ( 1 ... ( M  +  1 ) ) 
\  { ( M  +  1 ) } ) )  =  ( ( 2nd `  k
) " ( 1 ... M ) ) )
128125ad2antrr 730 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  -> 
( ( 1 ... ( M  +  1 ) )  \  {
( M  +  1 ) } )  =  ( 1 ... M
) )
129102, 127, 1283eqtr3d 2471 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  -> 
( ( 2nd `  k
) " ( 1 ... M ) )  =  ( 1 ... M ) )
130 f1oeq3 5821 . . . . . . . . . . . . . 14  |-  ( ( ( 2nd `  k
) " ( 1 ... M ) )  =  ( 1 ... M )  ->  (
( ( 2nd `  k
)  |`  ( 1 ... M ) ) : ( 1 ... M
)
-1-1-onto-> ( ( 2nd `  k
) " ( 1 ... M ) )  <-> 
( ( 2nd `  k
)  |`  ( 1 ... M ) ) : ( 1 ... M
)
-1-1-onto-> ( 1 ... M
) ) )
131129, 130syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  -> 
( ( ( 2nd `  k )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( ( 2nd `  k
) " ( 1 ... M ) )  <-> 
( ( 2nd `  k
)  |`  ( 1 ... M ) ) : ( 1 ... M
)
-1-1-onto-> ( 1 ... M
) ) )
13281, 131mpbid 213 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  -> 
( ( 2nd `  k
)  |`  ( 1 ... M ) ) : ( 1 ... M
)
-1-1-onto-> ( 1 ... M
) )
13373resex 5164 . . . . . . . . . . . . 13  |-  ( ( 2nd `  k )  |`  ( 1 ... M
) )  e.  _V
134 f1oeq1 5819 . . . . . . . . . . . . 13  |-  ( f  =  ( ( 2nd `  k )  |`  (
1 ... M ) )  ->  ( f : ( 1 ... M
)
-1-1-onto-> ( 1 ... M
)  <->  ( ( 2nd `  k )  |`  (
1 ... M ) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M
) ) )
135133, 134elab 3218 . . . . . . . . . . . 12  |-  ( ( ( 2nd `  k
)  |`  ( 1 ... M ) )  e. 
{ f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M
) }  <->  ( ( 2nd `  k )  |`  ( 1 ... M
) ) : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
136132, 135sylibr 215 . . . . . . . . . . 11  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  -> 
( ( 2nd `  k
)  |`  ( 1 ... M ) )  e. 
{ f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M
) } )
137 opelxpi 4882 . . . . . . . . . . 11  |-  ( ( ( ( 1st `  k
)  |`  ( 1 ... M ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... M ) )  /\  ( ( 2nd `  k )  |`  (
1 ... M ) )  e.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } )  ->  <. ( ( 1st `  k )  |`  ( 1 ... M
) ) ,  ( ( 2nd `  k
)  |`  ( 1 ... M ) ) >.  e.  ( ( ( 0..^ K )  ^m  (
1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )
13871, 136, 137syl2anc 665 . . . . . . . . . 10  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  ->  <. ( ( 1st `  k
)  |`  ( 1 ... M ) ) ,  ( ( 2nd `  k
)  |`  ( 1 ... M ) ) >.  e.  ( ( ( 0..^ K )  ^m  (
1 ... M ) )  X.  { f  |  f : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) } ) )
1391383ad2antr3 1172 . . . . . . . . 9  |-  ( ( ( ph  /\  k  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( M  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( M  + 
1 ) ) -1-1-onto-> ( 1 ... ( M  + 
1 ) ) } ) )  /\  ( A. i  e.  (
0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( 1st `  k
)  oF  +  ( ( ( ( 2nd `  k )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  k )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  /\  (
( 1st `  k
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) ) )  ->  <. ( ( 1st `  k )  |`  (
1 ... M ) ) ,  ( ( 2nd `  k )  |`  (
1 ... M ) )
>.  e.  ( ( ( 0..^ K )  ^m  ( 1 ... M
) )  X.  {
f  |  f : ( 1 ... M
)
-1-1-onto-> ( 1 ... M
) } ) )
140 3anass 986 . . . . . . . . . . 11  |-  ( ( A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ (
( ( 1st `  k
)  oF  +  ( ( ( ( 2nd `  k )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  k )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  /\  (
( 1st `  k
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  <->  ( A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( 1st `  k
)  oF  +  ( ( ( ( 2nd `  k )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  k )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  /\  (
( ( 1st `  k
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) ) ) )
141 ancom 451 . . . . . . . . . . 11  |-  ( ( A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ (
( ( 1st `  k
)  oF  +  ( ( ( ( 2nd `  k )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  k )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  /\  (
( ( 1st `  k
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) ) )  <-> 
( ( ( ( 1st `  k ) `
 ( M  + 
1 ) )  =  0  /\  ( ( 2nd `  k ) `
 ( M  + 
1 ) )  =  ( M  +  1 ) )  /\  A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( 1st `  k
)  oF  +  ( ( ( ( 2nd `  k )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  k )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B ) )
142140, 141bitri 252 . . . . . . . . . 10  |-  ( ( A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ (
( ( 1st `  k
)  oF  +  ( ( ( ( 2nd `  k )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  k )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  /\  (
( 1st `  k
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  <->  ( (
( ( 1st `  k
) `  ( M  +  1 ) )  =  0  /\  (
( 2nd `  k
) `  ( M  +  1 ) )  =  ( M  + 
1 ) )  /\  A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ ( ( ( 1st `  k
)  oF  +  ( ( ( ( 2nd `  k )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  k )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B ) )
14394nnzd 11040 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( M  +  1 )  e.  ZZ )
144 uzid 11174 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( M  +  1 )  e.  ZZ  ->  ( M  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
145 peano2uz 11213 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( M  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) )  ->  ( ( M  +  1 )  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
146143, 144, 1453syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( M  + 
1 )  +  1 )  e.  ( ZZ>= `  ( M  +  1
) ) )
1475nn0zd 11039 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  M  e.  ZZ )
1481nnzd 11040 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  N  e.  ZZ )
149 zltp1le 10987 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  <  N  <->  ( M  +  1 )  <_  N ) )
150 peano2z 10979 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( M  e.  ZZ  ->  ( M  +  1 )  e.  ZZ )
151 eluz 11173 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( M  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  ( M  + 
1 ) )  <->  ( M  +  1 )  <_  N ) )
152150, 151sylan 473 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  ( M  + 
1 ) )  <->  ( M  +  1 )  <_  N ) )
153149, 152bitr4d 259 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  <  N  <->  N  e.  ( ZZ>= `  ( M  +  1 ) ) ) )
154147, 148, 153syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( M  <  N  <->  N  e.  ( ZZ>= `  ( M  +  1 ) ) ) )
1557, 154mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  +  1
) ) )
156 fzsplit2 11825 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( M  + 
1 )  +  1 )  e.  ( ZZ>= `  ( M  +  1
) )  /\  N  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ( ( M  +  1 ) ... N )  =  ( ( ( M  +  1 ) ... ( M  +  1 ) )  u.  (
( ( M  + 
1 )  +  1 ) ... N ) ) )
157146, 155, 156syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( M  + 
1 ) ... N
)  =  ( ( ( M  +  1 ) ... ( M  +  1 ) )  u.  ( ( ( M  +  1 )  +  1 ) ... N ) ) )
158 fzsn 11841 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( M  +  1 )  e.  ZZ  ->  (
( M  +  1 ) ... ( M  +  1 ) )  =  { ( M  +  1 ) } )
159143, 158syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( M  + 
1 ) ... ( M  +  1 ) )  =  { ( M  +  1 ) } )
160159uneq1d 3619 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( M  +  1 ) ... ( M  +  1 ) )  u.  (
( ( M  + 
1 )  +  1 ) ... N ) )  =  ( { ( M  +  1 ) }  u.  (
( ( M  + 
1 )  +  1 ) ... N ) ) )
161157, 160eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( M  + 
1 ) ... N
)  =  ( { ( M  +  1 ) }  u.  (
( ( M  + 
1 )  +  1 ) ... N ) ) )
162161xpeq1d 4873 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( ( M  +  1 ) ... N )  X.  {
0 } )  =  ( ( { ( M  +  1 ) }  u.  ( ( ( M  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) )
163162uneq2d 3620 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( ( n  e.  ( 1 ... M
)  |->  ( ( ( 1st `  k ) `
 n )  +  ( ( ( ( ( 2nd `  k
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  n
) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  =  ( ( n  e.  ( 1 ... M )  |->  ( ( ( 1st `  k
) `  n )  +  ( ( ( ( ( 2nd `  k
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  n
) ) )  u.  ( ( { ( M  +  1 ) }  u.  ( ( ( M  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) )
164 xpundir 4904 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( { ( M  + 
1 ) }  u.  ( ( ( M  +  1 )  +  1 ) ... N
) )  X.  {
0 } )  =  ( ( { ( M  +  1 ) }  X.  { 0 } )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )
165 ovex 6330 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( M  +  1 )  e. 
_V
166 c0ex 9638 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  0  e.  _V
167165, 166xpsn 6078 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( { ( M  +  1 ) }  X.  {
0 } )  =  { <. ( M  + 
1 ) ,  0
>. }
168167uneq1i 3616 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( { ( M  + 
1 ) }  X.  { 0 } )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X. 
{ 0 } ) )  =  ( {
<. ( M  +  1 ) ,  0 >. }  u.  ( (
( ( M  + 
1 )  +  1 ) ... N )  X.  { 0 } ) )
169164, 168eqtri 2451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( { ( M  + 
1 ) }  u.  ( ( ( M  +  1 )  +  1 ) ... N
) )  X.  {
0 } )  =  ( { <. ( M  +  1 ) ,  0 >. }  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) )
170169uneq2i 3617 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( n  e.  ( 1 ... M )  |->  ( ( ( 1st `  k
) `  n )  +  ( ( ( ( ( 2nd `  k
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  n
) ) )  u.  ( ( { ( M  +  1 ) }  u.  ( ( ( M  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) )  =  ( ( n  e.  ( 1 ... M ) 
|->  ( ( ( 1st `  k ) `  n
)  +  ( ( ( ( ( 2nd `  k ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  n
) ) )  u.  ( { <. ( M  +  1 ) ,  0 >. }  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) ) )
171 unass 3623 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( n  e.  ( 1 ... M ) 
|->  ( ( ( 1st `  k ) `  n
)  +  ( ( ( ( ( 2nd `  k ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  n
) ) )  u. 
{ <. ( M  + 
1 ) ,  0
>. } )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  =  ( ( n  e.  ( 1 ... M
)  |->  ( ( ( 1st `  k ) `
 n )  +  ( ( ( ( ( 2nd `  k
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  n
) ) )  u.  ( { <. ( M  +  1 ) ,  0 >. }  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) ) )
172170, 171eqtr4i 2454 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( n  e.  ( 1 ... M )  |->  ( ( ( 1st `  k
) `  n )  +  ( ( ( ( ( 2nd `  k
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  n
) ) )  u.  ( ( { ( M  +  1 ) }  u.  ( ( ( M  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) )  =  ( ( ( n  e.  ( 1 ... M
)  |->  ( ( ( 1st `  k ) `
 n )  +  ( ( ( ( ( 2nd `  k
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  n
) ) )  u. 
{ <. ( M  + 
1 ) ,  0
>. } )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )
173163, 172syl6eq 2479 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( ( n  e.  ( 1 ... M
)  |->  ( ( ( 1st `  k ) `
 n )  +  ( ( ( ( ( 2nd `  k
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  n
) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  =  ( ( ( n  e.  ( 1 ... M )  |->  ( ( ( 1st `  k
) `  n )  +  ( ( ( ( ( 2nd `  k
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  n
) ) )  u. 
{ <. ( M  + 
1 ) ,  0
>. } )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) ) )
174173ad3antrrr 734 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  k  e.  ( (
( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X. 
{ f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } ) )  /\  ( ( ( 1st `  k ) `
 ( M  + 
1 ) )  =  0  /\  ( ( 2nd `  k ) `
 ( M  + 
1 ) )  =  ( M  +  1 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( ( n  e.  ( 1 ... M )  |->  ( ( ( 1st `  k
) `  n )  +  ( ( ( ( ( 2nd `  k
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  n
) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  =  ( ( ( n  e.  ( 1 ... M )  |->  ( ( ( 1st `  k
) `  n )  +  ( ( ( ( ( 2nd `  k
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  n
) ) )  u. 
{ <. ( M  + 
1 ) ,  0
>. } )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) ) )
175165a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( (
( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X. 
{ f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } ) )  /\  ( ( ( 1st `  k ) `
 ( M  + 
1 ) )  =  0  /\  ( ( 2nd `  k ) `
 ( M  + 
1 ) )  =  ( M  +  1 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( M  + 
1 )  e.  _V )
176166a1i 11 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( (
( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X. 
{ f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } ) )  /\  ( ( ( 1st `  k ) `
 ( M  + 
1 ) )  =  0  /\  ( ( 2nd `  k ) `
 ( M  + 
1 ) )  =  ( M  +  1 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  0  e.  _V )
177110eqcomd 2430 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( ( 1 ... M )  u.  {
( M  +  1 ) } )  =  ( 1 ... ( M  +  1 ) ) )
178177ad3antrrr 734 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  k  e.  ( (
( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X. 
{ f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } ) )  /\  ( ( ( 1st `  k ) `
 ( M  + 
1 ) )  =  0  /\  ( ( 2nd `  k ) `
 ( M  + 
1 ) )  =  ( M  +  1 ) ) )  /\  j  e.  ( 0 ... M ) )  ->  ( ( 1 ... M )  u. 
{ ( M  + 
1 ) } )  =  ( 1 ... ( M  +  1 ) ) )
179 fveq2 5878 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  ( M  + 
1 )  ->  (
( 1st `  k
) `  n )  =  ( ( 1st `  k ) `  ( M  +  1 ) ) )
180 fveq2 5878 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  ( M  + 
1 )  ->  (
( ( ( ( 2nd `  k )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  k )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) `  n )  =  ( ( ( ( ( 2nd `  k
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  ( M  +  1 ) ) )
181179, 180oveq12d 6320 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  ( M  + 
1 )  ->  (
( ( 1st `  k
) `  n )  +  ( ( ( ( ( 2nd `  k
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  k
) " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  X.  { 0 } ) ) `  n
) )  =  ( ( ( 1st `  k
) `  ( M