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

Theorem poimirlem27 31881
Description: Lemma for poimir 31887 showing that the difference between admissible faces in the whole cube and admissible faces on the back face is even. Equation (7) of [Kulpa] p. 548. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0  |-  ( ph  ->  N  e.  NN )
poimirlem28.1  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  ->  B  =  C )
poimirlem28.2  |-  ( (
ph  /\  p :
( 1 ... N
) --> ( 0 ... K ) )  ->  B  e.  ( 0 ... N ) )
poimirlem28.3  |-  ( (
ph  /\  ( n  e.  ( 1 ... N
)  /\  p :
( 1 ... N
) --> ( 0 ... K )  /\  (
p `  n )  =  0 ) )  ->  B  <  n
)
poimirlem28.4  |-  ( (
ph  /\  ( n  e.  ( 1 ... N
)  /\  p :
( 1 ... N
) --> ( 0 ... K )  /\  (
p `  n )  =  K ) )  ->  B  =/=  ( n  - 
1 ) )
Assertion
Ref Expression
poimirlem27  |-  ( ph  ->  2  ||  ( (
# `  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { ( 2nd `  t ) } ) i  =  [_ ( 1st `  t )  / 
s ]_ C } )  -  ( # `  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( 0 ... ( N  -  1 ) ) i  =  C  /\  ( ( 1st `  s ) `  N
)  =  0  /\  ( ( 2nd `  s
) `  N )  =  N ) } ) ) )
Distinct variable groups:    f, i,
j, n, p, s, t    ph, j, n    j, N, n    ph, i, p, s, t    B, f, i, j, n, s, t    f, K, i, j, n, p, s, t    f, N, i, p, s, t    C, i, n, p, t
Allowed substitution hints:    ph( f)    B( p)    C( f, j, s)

Proof of Theorem poimirlem27
Dummy variables  m  q  u  w  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfi 12185 . . . . . 6  |-  ( 0 ... K )  e. 
Fin
2 fzfi 12185 . . . . . 6  |-  ( 1 ... N )  e. 
Fin
3 mapfi 7873 . . . . . 6  |-  ( ( ( 0 ... K
)  e.  Fin  /\  ( 1 ... N
)  e.  Fin )  ->  ( ( 0 ... K )  ^m  (
1 ... N ) )  e.  Fin )
41, 2, 3mp2an 676 . . . . 5  |-  ( ( 0 ... K )  ^m  ( 1 ... N ) )  e. 
Fin
5 fzfi 12185 . . . . 5  |-  ( 0 ... ( N  - 
1 ) )  e. 
Fin
6 mapfi 7873 . . . . 5  |-  ( ( ( ( 0 ... K )  ^m  (
1 ... N ) )  e.  Fin  /\  (
0 ... ( N  - 
1 ) )  e. 
Fin )  ->  (
( ( 0 ... K )  ^m  (
1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) )  e. 
Fin )
74, 5, 6mp2an 676 . . . 4  |-  ( ( ( 0 ... K
)  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) )  e. 
Fin
87a1i 11 . . 3  |-  ( ph  ->  ( ( ( 0 ... K )  ^m  ( 1 ... N
) )  ^m  (
0 ... ( N  - 
1 ) ) )  e.  Fin )
9 2z 10970 . . . 4  |-  2  e.  ZZ
109a1i 11 . . 3  |-  ( ph  ->  2  e.  ZZ )
11 fzofi 12187 . . . . . . . 8  |-  ( 0..^ K )  e.  Fin
12 mapfi 7873 . . . . . . . 8  |-  ( ( ( 0..^ K )  e.  Fin  /\  (
1 ... N )  e. 
Fin )  ->  (
( 0..^ K )  ^m  ( 1 ... N ) )  e. 
Fin )
1311, 2, 12mp2an 676 . . . . . . 7  |-  ( ( 0..^ K )  ^m  ( 1 ... N
) )  e.  Fin
14 mapfi 7873 . . . . . . . . 9  |-  ( ( ( 1 ... N
)  e.  Fin  /\  ( 1 ... N
)  e.  Fin )  ->  ( ( 1 ... N )  ^m  (
1 ... N ) )  e.  Fin )
152, 2, 14mp2an 676 . . . . . . . 8  |-  ( ( 1 ... N )  ^m  ( 1 ... N ) )  e. 
Fin
16 f1of 5828 . . . . . . . . . 10  |-  ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  f :
( 1 ... N
) --> ( 1 ... N ) )
1716ss2abi 3533 . . . . . . . . 9  |-  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  C_  { f  |  f : ( 1 ... N ) --> ( 1 ... N
) }
18 ovex 6330 . . . . . . . . . 10  |-  ( 1 ... N )  e. 
_V
1918, 18mapval 7489 . . . . . . . . 9  |-  ( ( 1 ... N )  ^m  ( 1 ... N ) )  =  { f  |  f : ( 1 ... N ) --> ( 1 ... N ) }
2017, 19sseqtr4i 3497 . . . . . . . 8  |-  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  C_  ( (
1 ... N )  ^m  ( 1 ... N
) )
21 ssfi 7795 . . . . . . . 8  |-  ( ( ( ( 1 ... N )  ^m  (
1 ... N ) )  e.  Fin  /\  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) }  C_  (
( 1 ... N
)  ^m  ( 1 ... N ) ) )  ->  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  e.  Fin )
2215, 20, 21mp2an 676 . . . . . . 7  |-  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  e.  Fin
23 xpfi 7845 . . . . . . 7  |-  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  e.  Fin  /\  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) }  e.  Fin )  ->  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  e. 
Fin )
2413, 22, 23mp2an 676 . . . . . 6  |-  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  e. 
Fin
25 fzfi 12185 . . . . . 6  |-  ( 0 ... N )  e. 
Fin
26 xpfi 7845 . . . . . 6  |-  ( ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  e.  Fin  /\  ( 0 ... N
)  e.  Fin )  ->  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  e.  Fin )
2724, 25, 26mp2an 676 . . . . 5  |-  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  e.  Fin
28 rabfi 7799 . . . . 5  |-  ( ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  e.  Fin  ->  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  ( x  =  ( 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 } ) ) ) )  /\  ( ( 0 ... ( N  -  1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  A. n  e.  ( 1 ... N ) ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
) ) ) }  e.  Fin )
2927, 28ax-mp 5 . . . 4  |-  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  ( x  =  ( 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 } ) ) ) )  /\  ( ( 0 ... ( N  -  1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  A. n  e.  ( 1 ... N ) ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
) ) ) }  e.  Fin
30 hashcl 12538 . . . . 5  |-  ( { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  ( x  =  ( 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 } ) ) ) )  /\  ( ( 0 ... ( N  -  1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  A. n  e.  ( 1 ... N ) ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
) ) ) }  e.  Fin  ->  ( # `
 { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  ( x  =  ( 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 } ) ) ) )  /\  ( ( 0 ... ( N  -  1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  A. n  e.  ( 1 ... N ) ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
) ) ) } )  e.  NN0 )
3130nn0zd 11039 . . . 4  |-  ( { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  ( x  =  ( 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 } ) ) ) )  /\  ( ( 0 ... ( N  -  1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  A. n  e.  ( 1 ... N ) ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
) ) ) }  e.  Fin  ->  ( # `
 { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  ( x  =  ( 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 } ) ) ) )  /\  ( ( 0 ... ( N  -  1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  A. n  e.  ( 1 ... N ) ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
) ) ) } )  e.  ZZ )
3229, 31mp1i 13 . . 3  |-  ( (
ph  /\  x  e.  ( ( ( 0 ... K )  ^m  ( 1 ... N
) )  ^m  (
0 ... ( N  - 
1 ) ) ) )  ->  ( # `  {
t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  ( x  =  ( 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 } ) ) ) )  /\  ( ( 0 ... ( N  -  1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  A. n  e.  ( 1 ... N ) ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
) ) ) } )  e.  ZZ )
33 dfrex2 2876 . . . . 5  |-  ( E. t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) ( ( 0 ... ( N  -  1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  A. n  e.  ( 1 ... N ) ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
) )  <->  -.  A. t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  -.  (
( 0 ... ( N  -  1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  A. n  e.  ( 1 ... N
) ( E. p  e.  ran  x ( p `
 n )  =/=  0  /\  E. p  e.  ran  x ( p `
 n )  =/= 
K ) ) )
34 nfv 1751 . . . . . 6  |-  F/ t ( ph  /\  x  e.  ( ( ( 0 ... K )  ^m  ( 1 ... N
) )  ^m  (
0 ... ( N  - 
1 ) ) ) )
35 nfcv 2584 . . . . . . 7  |-  F/_ t
2
36 nfcv 2584 . . . . . . 7  |-  F/_ t  ||
37 nfcv 2584 . . . . . . . 8  |-  F/_ t #
38 nfrab1 3009 . . . . . . . 8  |-  F/_ t { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  ( x  =  ( 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 } ) ) ) )  /\  ( ( 0 ... ( N  -  1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  A. n  e.  ( 1 ... N ) ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
) ) ) }
3937, 38nffv 5885 . . . . . . 7  |-  F/_ t
( # `  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  ( x  =  ( 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 } ) ) ) )  /\  ( ( 0 ... ( N  -  1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  A. n  e.  ( 1 ... N ) ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
) ) ) } )
4035, 36, 39nfbr 4465 . . . . . 6  |-  F/ t 2  ||  ( # `  { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  ( x  =  ( 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 } ) ) ) )  /\  ( ( 0 ... ( N  -  1 ) )  C_  ran  ( p  e.  ran  x  |->  B )  /\  A. n  e.  ( 1 ... N ) ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
) ) ) } )
41 neq0 3772 . . . . . . . . . . . 12  |-  ( -. 
{ t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) }  =  (/)  <->  E. s  s  e. 
{ t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) } )
42 iddvds 14304 . . . . . . . . . . . . . . . . 17  |-  ( 2  e.  ZZ  ->  2  ||  2 )
439, 42ax-mp 5 . . . . . . . . . . . . . . . 16  |-  2  ||  2
44 vex 3084 . . . . . . . . . . . . . . . . . . 19  |-  s  e. 
_V
45 hashsng 12549 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  _V  ->  ( # `
 { s } )  =  1 )
4644, 45ax-mp 5 . . . . . . . . . . . . . . . . . 18  |-  ( # `  { s } )  =  1
4746oveq2i 6313 . . . . . . . . . . . . . . . . 17  |-  ( 1  +  ( # `  {
s } ) )  =  ( 1  +  1 )
48 df-2 10669 . . . . . . . . . . . . . . . . 17  |-  2  =  ( 1  +  1 )
4947, 48eqtr4i 2454 . . . . . . . . . . . . . . . 16  |-  ( 1  +  ( # `  {
s } ) )  =  2
5043, 49breqtrri 4446 . . . . . . . . . . . . . . 15  |-  2  ||  ( 1  +  (
# `  { s } ) )
51 rabfi 7799 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  e.  Fin  ->  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) }  e.  Fin )
52 diffi 7806 . . . . . . . . . . . . . . . . . . . 20  |-  ( { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) }  e.  Fin  ->  ( { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  e.  Fin )
5327, 51, 52mp2b 10 . . . . . . . . . . . . . . . . . . 19  |-  ( { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  e.  Fin
54 snfi 7654 . . . . . . . . . . . . . . . . . . 19  |-  { s }  e.  Fin
55 incom 3655 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  i^i  { s } )  =  ( { s }  i^i  ( { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } ) )
56 disjdif 3867 . . . . . . . . . . . . . . . . . . . 20  |-  ( { s }  i^i  ( { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } ) )  =  (/)
5755, 56eqtri 2451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  i^i  { s } )  =  (/)
58 hashun 12561 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  e.  Fin  /\  { s }  e.  Fin  /\  ( ( { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  i^i  { s } )  =  (/) )  ->  ( # `  (
( { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  u.  { s } ) )  =  ( ( # `  ( { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } ) )  +  (
# `  { s } ) ) )
5953, 54, 57, 58mp3an 1360 . . . . . . . . . . . . . . . . . 18  |-  ( # `  ( ( { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  u.  { s } ) )  =  ( ( # `  ( { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } ) )  +  (
# `  { s } ) )
60 difsnid 4143 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  u.  { s } )  =  {
t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } )
6160fveq2d 5882 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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
) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  u.  { s } ) )  =  ( # `  {
t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } ) )
6259, 61syl5eqr 2477 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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
) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } ) )  +  (
# `  { s } ) )  =  ( # `  {
t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } ) )
6362adantl 467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  x  e.  ( (
( 0 ... K
)  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) ) )  /\  A. n  e.  ( 1 ... N
) ( E. p  e.  ran  x ( p `
 n )  =/=  0  /\  E. p  e.  ran  x ( p `
 n )  =/= 
K ) )  /\  s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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
) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } ) )  +  (
# `  { s } ) )  =  ( # `  {
t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 poimir.0 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  N  e.  NN )
6564ad3antrrr 734 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  ( (
( 0 ... K
)  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) ) )  /\  A. n  e.  ( 1 ... N
) ( E. p  e.  ran  x ( p `
 n )  =/=  0  /\  E. p  e.  ran  x ( p `
 n )  =/= 
K ) )  /\  s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } )  ->  N  e.  NN )
66 fveq2 5878 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  u  ->  ( 2nd `  t )  =  ( 2nd `  u
) )
6766breq2d 4432 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  u  ->  (
y  <  ( 2nd `  t )  <->  y  <  ( 2nd `  u ) ) )
6867ifbid 3931 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  u  ->  if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  =  if ( y  <  ( 2nd `  u
) ,  y ,  ( y  +  1 ) ) )
6968csbeq1d 3402 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 } ) ) ) )
70 fveq2 5878 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  u  ->  ( 1st `  t )  =  ( 1st `  u
) )
7170fveq2d 5882 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  u  ->  ( 1st `  ( 1st `  t
) )  =  ( 1st `  ( 1st `  u ) ) )
7270fveq2d 5882 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( t  =  u  ->  ( 2nd `  ( 1st `  t
) )  =  ( 2nd `  ( 1st `  u ) ) )
7372imaeq1d 5183 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  u  ->  (
( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  u ) )
" ( 1 ... j ) ) )
7473xpeq1d 4873 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  u  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  u ) ) "
( 1 ... j
) )  X.  {
1 } ) )
7572imaeq1d 5183 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  u  ->  (
( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  u ) )
" ( ( j  +  1 ) ... N ) ) )
7675xpeq1d 4873 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  u  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  u ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )
7774, 76uneq12d 3621 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 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 } ) ) )
7871, 77oveq12d 6320 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 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 } ) ) ) )
7978csbeq2dv 3809 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 } ) ) ) )
8069, 79eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 } ) ) ) )
8180mpteq2dv 4508 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 } ) ) ) ) )
82 breq1 4423 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  w  ->  (
y  <  ( 2nd `  u )  <->  w  <  ( 2nd `  u ) ) )
83 id 23 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  w  ->  y  =  w )
84 oveq1 6309 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( y  =  w  ->  (
y  +  1 )  =  ( w  + 
1 ) )
8582, 83, 84ifbieq12d 3936 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  w  ->  if ( y  <  ( 2nd `  u ) ,  y ,  ( y  +  1 ) )  =  if ( w  <  ( 2nd `  u
) ,  w ,  ( w  +  1 ) ) )
8685csbeq1d 3402 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  w  ->  [_ 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 } ) ) )  =  [_ if ( w  <  ( 2nd `  u ) ,  w ,  ( w  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  u ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  u
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  u ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
87 oveq2 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  =  i  ->  (
1 ... j )  =  ( 1 ... i
) )
8887imaeq2d 5184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  =  i  ->  (
( 2nd `  ( 1st `  u ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  u ) )
" ( 1 ... i ) ) )
8988xpeq1d 4873 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  i  ->  (
( ( 2nd `  ( 1st `  u ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  u ) ) "
( 1 ... i
) )  X.  {
1 } ) )
90 oveq1 6309 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  =  i  ->  (
j  +  1 )  =  ( i  +  1 ) )
9190oveq1d 6317 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  =  i  ->  (
( j  +  1 ) ... N )  =  ( ( i  +  1 ) ... N ) )
9291imaeq2d 5184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  =  i  ->  (
( 2nd `  ( 1st `  u ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  u ) )
" ( ( i  +  1 ) ... N ) ) )
9392xpeq1d 4873 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  i  ->  (
( ( 2nd `  ( 1st `  u ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  u ) ) "
( ( i  +  1 ) ... N
) )  X.  {
0 } ) )
9489, 93uneq12d 3621 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  i  ->  (
( ( ( 2nd `  ( 1st `  u
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  u ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) )  =  ( ( ( ( 2nd `  ( 1st `  u ) )
" ( 1 ... i ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  u ) ) "
( ( i  +  1 ) ... N
) )  X.  {
0 } ) ) )
9594oveq2d 6318 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  i  ->  (
( 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 ... i ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  u ) )
" ( ( i  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
9695cbvcsbv 3401 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  [_ if ( w  <  ( 2nd `  u ) ,  w ,  ( w  + 
1 ) )  / 
j ]_ ( ( 1st `  ( 1st `  u
) )  oF  +  ( ( ( ( 2nd `  ( 1st `  u ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  u ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  =  [_ if ( w  <  ( 2nd `  u ) ,  w ,  ( w  + 
1 ) )  / 
i ]_ ( ( 1st `  ( 1st `  u
) )  oF  +  ( ( ( ( 2nd `  ( 1st `  u ) )
" ( 1 ... i ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  u ) ) "
( ( i  +  1 ) ... N
) )  X.  {
0 } ) ) )
9786, 96syl6eq 2479 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  =  w  ->  [_ 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 } ) ) )  =  [_ if ( w  <  ( 2nd `  u ) ,  w ,  ( w  +  1 ) )  /  i ]_ (
( 1st `  ( 1st `  u ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  u
) ) " (
1 ... i ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  u ) )
" ( ( i  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
9897cbvmptv 4513 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 } ) ) ) )  =  ( w  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( w  <  ( 2nd `  u
) ,  w ,  ( w  +  1 ) )  /  i ]_ ( ( 1st `  ( 1st `  u ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  u
) ) " (
1 ... i ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  u ) )
" ( ( i  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
9981, 98syl6eq 2479 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 } ) ) ) )  =  ( w  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( w  <  ( 2nd `  u
) ,  w ,  ( w  +  1 ) )  /  i ]_ ( ( 1st `  ( 1st `  u ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  u
) ) " (
1 ... i ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  u ) )
" ( ( i  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
10099eqeq2d 2436 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  u  ->  (
x  =  ( 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 } ) ) ) )  <->  x  =  ( w  e.  (
0 ... ( N  - 
1 ) )  |->  [_ if ( w  <  ( 2nd `  u ) ,  w ,  ( w  +  1 ) )  /  i ]_ (
( 1st `  ( 1st `  u ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  u
) ) " (
1 ... i ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  u ) )
" ( ( i  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) ) )
101100cbvrabv 3080 . . . . . . . . . . . . . . . . . . 19  |-  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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
) )  |  x  =  ( w  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( w  <  ( 2nd `  u
) ,  w ,  ( w  +  1 ) )  /  i ]_ ( ( 1st `  ( 1st `  u ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  u
) ) " (
1 ... i ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  u ) )
" ( ( i  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) }
102 elmapi 7498 . . . . . . . . . . . . . . . . . . . 20  |-  ( x  e.  ( ( ( 0 ... K )  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) )  ->  x : ( 0 ... ( N  -  1 ) ) --> ( ( 0 ... K )  ^m  ( 1 ... N ) ) )
103102ad3antlr 735 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  ( (
( 0 ... K
)  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) ) )  /\  A. n  e.  ( 1 ... N
) ( E. p  e.  ran  x ( p `
 n )  =/=  0  /\  E. p  e.  ran  x ( p `
 n )  =/= 
K ) )  /\  s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } )  ->  x :
( 0 ... ( N  -  1 ) ) --> ( ( 0 ... K )  ^m  ( 1 ... N
) ) )
104 simpr 462 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  x  e.  ( (
( 0 ... K
)  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) ) )  /\  A. n  e.  ( 1 ... N
) ( E. p  e.  ran  x ( p `
 n )  =/=  0  /\  E. p  e.  ran  x ( p `
 n )  =/= 
K ) )  /\  s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } )  ->  s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } )
105 simpl 458 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
)  ->  E. p  e.  ran  x ( p `
 n )  =/=  0 )
106105ralimi 2818 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. n  e.  ( 1 ... N ) ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
)  ->  A. n  e.  ( 1 ... N
) E. p  e. 
ran  x ( p `
 n )  =/=  0 )
107106ad2antlr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  ( (
( 0 ... K
)  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) ) )  /\  A. n  e.  ( 1 ... N
) ( E. p  e.  ran  x ( p `
 n )  =/=  0  /\  E. p  e.  ran  x ( p `
 n )  =/= 
K ) )  /\  s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } )  ->  A. n  e.  ( 1 ... N
) E. p  e. 
ran  x ( p `
 n )  =/=  0 )
108 fveq2 5878 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( n  =  m  ->  (
p `  n )  =  ( p `  m ) )
109108neeq1d 2701 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  m  ->  (
( p `  n
)  =/=  0  <->  (
p `  m )  =/=  0 ) )
110109rexbidv 2939 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  m  ->  ( E. p  e.  ran  x ( p `  n )  =/=  0  <->  E. p  e.  ran  x
( p `  m
)  =/=  0 ) )
111 fveq1 5877 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  =  q  ->  (
p `  m )  =  ( q `  m ) )
112111neeq1d 2701 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( p  =  q  ->  (
( p `  m
)  =/=  0  <->  (
q `  m )  =/=  0 ) )
113112cbvrexv 3056 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E. p  e.  ran  x
( p `  m
)  =/=  0  <->  E. q  e.  ran  x ( q `  m )  =/=  0 )
114110, 113syl6bb 264 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  m  ->  ( E. p  e.  ran  x ( p `  n )  =/=  0  <->  E. q  e.  ran  x
( q `  m
)  =/=  0 ) )
115114rspccva 3181 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. n  e.  ( 1 ... N ) E. p  e.  ran  x ( p `  n )  =/=  0  /\  m  e.  (
1 ... N ) )  ->  E. q  e.  ran  x ( q `  m )  =/=  0
)
116107, 115sylan 473 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  x  e.  ( ( ( 0 ... K
)  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) ) )  /\  A. n  e.  ( 1 ... N
) ( E. p  e.  ran  x ( p `
 n )  =/=  0  /\  E. p  e.  ran  x ( p `
 n )  =/= 
K ) )  /\  s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } )  /\  m  e.  ( 1 ... N
) )  ->  E. q  e.  ran  x ( q `
 m )  =/=  0 )
117 simpr 462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
)  ->  E. p  e.  ran  x ( p `
 n )  =/= 
K )
118117ralimi 2818 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. n  e.  ( 1 ... N ) ( E. p  e.  ran  x ( p `  n )  =/=  0  /\  E. p  e.  ran  x ( p `  n )  =/=  K
)  ->  A. n  e.  ( 1 ... N
) E. p  e. 
ran  x ( p `
 n )  =/= 
K )
119118ad2antlr 731 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  x  e.  ( (
( 0 ... K
)  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) ) )  /\  A. n  e.  ( 1 ... N
) ( E. p  e.  ran  x ( p `
 n )  =/=  0  /\  E. p  e.  ran  x ( p `
 n )  =/= 
K ) )  /\  s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } )  ->  A. n  e.  ( 1 ... N
) E. p  e. 
ran  x ( p `
 n )  =/= 
K )
120108neeq1d 2701 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( n  =  m  ->  (
( p `  n
)  =/=  K  <->  ( p `  m )  =/=  K
) )
121120rexbidv 2939 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  =  m  ->  ( E. p  e.  ran  x ( p `  n )  =/=  K  <->  E. p  e.  ran  x
( p `  m
)  =/=  K ) )
122111neeq1d 2701 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( p  =  q  ->  (
( p `  m
)  =/=  K  <->  ( q `  m )  =/=  K
) )
123122cbvrexv 3056 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E. p  e.  ran  x
( p `  m
)  =/=  K  <->  E. q  e.  ran  x ( q `
 m )  =/= 
K )
124121, 123syl6bb 264 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  m  ->  ( E. p  e.  ran  x ( p `  n )  =/=  K  <->  E. q  e.  ran  x
( q `  m
)  =/=  K ) )
125124rspccva 3181 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. n  e.  ( 1 ... N ) E. p  e.  ran  x ( p `  n )  =/=  K  /\  m  e.  (
1 ... N ) )  ->  E. q  e.  ran  x ( q `  m )  =/=  K
)
126119, 125sylan 473 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  x  e.  ( ( ( 0 ... K
)  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) ) )  /\  A. n  e.  ( 1 ... N
) ( E. p  e.  ran  x ( p `
 n )  =/=  0  /\  E. p  e.  ran  x ( p `
 n )  =/= 
K ) )  /\  s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } )  /\  m  e.  ( 1 ... N
) )  ->  E. q  e.  ran  x ( q `
 m )  =/= 
K )
12765, 101, 103, 104, 116, 126poimirlem22 31876 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  x  e.  ( (
( 0 ... K
)  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) ) )  /\  A. n  e.  ( 1 ... N
) ( E. p  e.  ran  x ( p `
 n )  =/=  0  /\  E. p  e.  ran  x ( p `
 n )  =/= 
K ) )  /\  s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } )  ->  E! z  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } z  =/=  s )
128 eldifsn 4122 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  ( { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  <->  ( z  e. 
{ t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) }  /\  z  =/=  s
) )
129128eubii 2288 . . . . . . . . . . . . . . . . . . 19  |-  ( E! z  z  e.  ( { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  <->  E! z ( z  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) }  /\  z  =/=  s
) )
13053elexi 3091 . . . . . . . . . . . . . . . . . . . 20  |-  ( { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  e.  _V
131 euhash1 12592 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } )  e.  _V  ->  ( ( # `  ( { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } ) )  =  1  <-> 
E! z  z  e.  ( { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } ) ) )
132130, 131ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( (
# `  ( {
t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } ) )  =  1  <-> 
E! z  z  e.  ( { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } ) )
133 df-reu 2782 . . . . . . . . . . . . . . . . . . 19  |-  ( E! z  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } z  =/=  s  <->  E! z
( z  e.  {
t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) }  /\  z  =/=  s
) )
134129, 132, 1333bitr4ri 281 . . . . . . . . . . . . . . . . . 18  |-  ( E! z  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( 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 } ) ) ) ) } z  =/=  s  <->  ( # `  ( { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  x  =  ( 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 } ) ) ) ) } 
\  { s } ) )  =  1 )
135127, 134sylib 199 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  x  e.  ( (
( 0 ... K
)  ^m  ( 1 ... N ) )  ^m  ( 0 ... ( N  -  1 ) ) ) )  /\  A. n  e.  ( 1 ... N
) ( E. p  e.  ran  x ( p `
 n )  =/=  0  /\  E. p  e.  ran  x ( p `
 n )  =/= 
K ) )  /\  s  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  x  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <