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

Theorem poimirlem26 31886
Description: Lemma for poimir 31893 showing an even difference between the number of admissible faces and the number of admissible simplices. Equation (6) 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 ) )
Assertion
Ref Expression
poimirlem26  |-  ( 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 ) E. j  e.  ( 0 ... N ) i  =  C }
) ) )
Distinct variable groups:    f, i,
j, p, s, t    ph, j    j, N    ph, i, p, s, t    B, f, i, j, s, t   
f, K, i, j, p, s, t    f, N, i, p, s, t    C, i, p, t
Allowed substitution hints:    ph( f)    B( p)    C( f, j, s)

Proof of Theorem poimirlem26
Dummy variables  k  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzofi 12188 . . . . . 6  |-  ( 0..^ K )  e.  Fin
2 fzfi 12186 . . . . . 6  |-  ( 1 ... N )  e. 
Fin
3 mapfi 7874 . . . . . 6  |-  ( ( ( 0..^ K )  e.  Fin  /\  (
1 ... N )  e. 
Fin )  ->  (
( 0..^ K )  ^m  ( 1 ... N ) )  e. 
Fin )
41, 2, 3mp2an 677 . . . . 5  |-  ( ( 0..^ K )  ^m  ( 1 ... N
) )  e.  Fin
5 mapfi 7874 . . . . . . 7  |-  ( ( ( 1 ... N
)  e.  Fin  /\  ( 1 ... N
)  e.  Fin )  ->  ( ( 1 ... N )  ^m  (
1 ... N ) )  e.  Fin )
62, 2, 5mp2an 677 . . . . . 6  |-  ( ( 1 ... N )  ^m  ( 1 ... N ) )  e. 
Fin
7 f1of 5829 . . . . . . . 8  |-  ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  f :
( 1 ... N
) --> ( 1 ... N ) )
87ss2abi 3534 . . . . . . 7  |-  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  C_  { f  |  f : ( 1 ... N ) --> ( 1 ... N
) }
9 ovex 6331 . . . . . . . 8  |-  ( 1 ... N )  e. 
_V
109, 9mapval 7490 . . . . . . 7  |-  ( ( 1 ... N )  ^m  ( 1 ... N ) )  =  { f  |  f : ( 1 ... N ) --> ( 1 ... N ) }
118, 10sseqtr4i 3498 . . . . . 6  |-  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  C_  ( (
1 ... N )  ^m  ( 1 ... N
) )
12 ssfi 7796 . . . . . 6  |-  ( ( ( ( 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 )
136, 11, 12mp2an 677 . . . . 5  |-  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  e.  Fin
144, 13pm3.2i 457 . . . 4  |-  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  e. 
Fin  /\  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  e.  Fin )
15 xpfi 7846 . . . 4  |-  ( ( ( ( 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 )
1614, 15mp1i 13 . . 3  |-  ( ph  ->  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  e.  Fin )
17 2z 10971 . . . 4  |-  2  e.  ZZ
1817a1i 11 . . 3  |-  ( ph  ->  2  e.  ZZ )
19 snfi 7655 . . . . . . 7  |-  { x }  e.  Fin
20 fzfi 12186 . . . . . . . 8  |-  ( 0 ... N )  e. 
Fin
21 rabfi 7800 . . . . . . . 8  |-  ( ( 0 ... N )  e.  Fin  ->  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N
) N  =/=  [_ x  /  s ]_ C
) }  e.  Fin )
2220, 21ax-mp 5 . . . . . . 7  |-  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N
) N  =/=  [_ x  /  s ]_ C
) }  e.  Fin
23 xpfi 7846 . . . . . . 7  |-  ( ( { x }  e.  Fin  /\  { y  e.  ( 0 ... N
)  |  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C
) }  e.  Fin )  ->  ( { x }  X.  { y  e.  ( 0 ... N
)  |  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C
) } )  e. 
Fin )
2419, 22, 23mp2an 677 . . . . . 6  |-  ( { x }  X.  {
y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } )  e.  Fin
25 hashcl 12539 . . . . . 6  |-  ( ( { x }  X.  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } )  e.  Fin  ->  ( # `
 ( { x }  X.  { y  e.  ( 0 ... N
)  |  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C
) } ) )  e.  NN0 )
2624, 25ax-mp 5 . . . . 5  |-  ( # `  ( { x }  X.  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } ) )  e.  NN0
2726nn0zi 10964 . . . 4  |-  ( # `  ( { x }  X.  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } ) )  e.  ZZ
2827a1i 11 . . 3  |-  ( (
ph  /\  x  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )  ->  ( # `
 ( { x }  X.  { y  e.  ( 0 ... N
)  |  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C
) } ) )  e.  ZZ )
29 poimir.0 . . . . . . . . . 10  |-  ( ph  ->  N  e.  NN )
3029adantr 467 . . . . . . . . 9  |-  ( (
ph  /\  x  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )  ->  N  e.  NN )
3130adantr 467 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C )  ->  N  e.  NN )
32 nfv 1752 . . . . . . . . . 10  |-  F/ j  p  =  ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t ) " (
1 ... k ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( k  +  1 ) ... N ) )  X.  { 0 } ) ) )
33 nfcsb1v 3412 . . . . . . . . . . 11  |-  F/_ j [_ k  /  j ]_ [_ t  /  s ]_ C
3433nfeq2 2602 . . . . . . . . . 10  |-  F/ j  B  =  [_ k  /  j ]_ [_ t  /  s ]_ C
3532, 34nfim 1977 . . . . . . . . 9  |-  F/ j ( p  =  ( ( 1st `  t
)  oF  +  ( ( ( ( 2nd `  t )
" ( 1 ... k ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  t )
" ( ( k  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  ->  B  =  [_ k  /  j ]_ [_ t  /  s ]_ C )
36 oveq2 6311 . . . . . . . . . . . . . . 15  |-  ( j  =  k  ->  (
1 ... j )  =  ( 1 ... k
) )
3736imaeq2d 5185 . . . . . . . . . . . . . 14  |-  ( j  =  k  ->  (
( 2nd `  t
) " ( 1 ... j ) )  =  ( ( 2nd `  t ) " (
1 ... k ) ) )
3837xpeq1d 4874 . . . . . . . . . . . . 13  |-  ( j  =  k  ->  (
( ( 2nd `  t
) " ( 1 ... j ) )  X.  { 1 } )  =  ( ( ( 2nd `  t
) " ( 1 ... k ) )  X.  { 1 } ) )
39 oveq1 6310 . . . . . . . . . . . . . . . 16  |-  ( j  =  k  ->  (
j  +  1 )  =  ( k  +  1 ) )
4039oveq1d 6318 . . . . . . . . . . . . . . 15  |-  ( j  =  k  ->  (
( j  +  1 ) ... N )  =  ( ( k  +  1 ) ... N ) )
4140imaeq2d 5185 . . . . . . . . . . . . . 14  |-  ( j  =  k  ->  (
( 2nd `  t
) " ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  t ) " (
( k  +  1 ) ... N ) ) )
4241xpeq1d 4874 . . . . . . . . . . . . 13  |-  ( j  =  k  ->  (
( ( 2nd `  t
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } )  =  ( ( ( 2nd `  t
) " ( ( k  +  1 ) ... N ) )  X.  { 0 } ) )
4338, 42uneq12d 3622 . . . . . . . . . . . 12  |-  ( j  =  k  ->  (
( ( ( 2nd `  t ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) )  =  ( ( ( ( 2nd `  t ) " (
1 ... k ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( k  +  1 ) ... N ) )  X.  { 0 } ) ) )
4443oveq2d 6319 . . . . . . . . . . 11  |-  ( j  =  k  ->  (
( 1st `  t
)  oF  +  ( ( ( ( 2nd `  t )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  t )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  t
)  oF  +  ( ( ( ( 2nd `  t )
" ( 1 ... k ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  t )
" ( ( k  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
4544eqeq2d 2437 . . . . . . . . . 10  |-  ( j  =  k  ->  (
p  =  ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  <->  p  =  ( ( 1st `  t
)  oF  +  ( ( ( ( 2nd `  t )
" ( 1 ... k ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  t )
" ( ( k  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
46 csbeq1a 3405 . . . . . . . . . . 11  |-  ( j  =  k  ->  [_ t  /  s ]_ C  =  [_ k  /  j ]_ [_ t  /  s ]_ C )
4746eqeq2d 2437 . . . . . . . . . 10  |-  ( j  =  k  ->  ( B  =  [_ t  / 
s ]_ C  <->  B  =  [_ k  /  j ]_ [_ t  /  s ]_ C ) )
4845, 47imbi12d 322 . . . . . . . . 9  |-  ( j  =  k  ->  (
( p  =  ( ( 1st `  t
)  oF  +  ( ( ( ( 2nd `  t )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  t )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  ->  B  =  [_ t  /  s ]_ C )  <->  ( p  =  ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t
) " ( 1 ... k ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( k  +  1 ) ... N ) )  X.  { 0 } ) ) )  ->  B  =  [_ k  / 
j ]_ [_ t  / 
s ]_ C ) ) )
49 nfv 1752 . . . . . . . . . . 11  |-  F/ s  p  =  ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )
50 nfcsb1v 3412 . . . . . . . . . . . 12  |-  F/_ s [_ t  /  s ]_ C
5150nfeq2 2602 . . . . . . . . . . 11  |-  F/ s  B  =  [_ t  /  s ]_ C
5249, 51nfim 1977 . . . . . . . . . 10  |-  F/ s ( p  =  ( ( 1st `  t
)  oF  +  ( ( ( ( 2nd `  t )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  t )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  ->  B  =  [_ t  /  s ]_ C )
53 fveq2 5879 . . . . . . . . . . . . 13  |-  ( s  =  t  ->  ( 1st `  s )  =  ( 1st `  t
) )
54 fveq2 5879 . . . . . . . . . . . . . . . 16  |-  ( s  =  t  ->  ( 2nd `  s )  =  ( 2nd `  t
) )
5554imaeq1d 5184 . . . . . . . . . . . . . . 15  |-  ( s  =  t  ->  (
( 2nd `  s
) " ( 1 ... j ) )  =  ( ( 2nd `  t ) " (
1 ... j ) ) )
5655xpeq1d 4874 . . . . . . . . . . . . . 14  |-  ( s  =  t  ->  (
( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  =  ( ( ( 2nd `  t
) " ( 1 ... j ) )  X.  { 1 } ) )
5754imaeq1d 5184 . . . . . . . . . . . . . . 15  |-  ( s  =  t  ->  (
( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  t ) " (
( j  +  1 ) ... N ) ) )
5857xpeq1d 4874 . . . . . . . . . . . . . 14  |-  ( s  =  t  ->  (
( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } )  =  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) )
5956, 58uneq12d 3622 . . . . . . . . . . . . 13  |-  ( s  =  t  ->  (
( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) )  =  ( ( ( ( 2nd `  t ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )
6053, 59oveq12d 6321 . . . . . . . . . . . 12  |-  ( s  =  t  ->  (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  t
)  oF  +  ( ( ( ( 2nd `  t )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  t )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
6160eqeq2d 2437 . . . . . . . . . . 11  |-  ( s  =  t  ->  (
p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  <->  p  =  ( ( 1st `  t
)  oF  +  ( ( ( ( 2nd `  t )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  t )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
62 csbeq1a 3405 . . . . . . . . . . . 12  |-  ( s  =  t  ->  C  =  [_ t  /  s ]_ C )
6362eqeq2d 2437 . . . . . . . . . . 11  |-  ( s  =  t  ->  ( B  =  C  <->  B  =  [_ t  /  s ]_ C ) )
6461, 63imbi12d 322 . . . . . . . . . 10  |-  ( s  =  t  ->  (
( p  =  ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  ->  B  =  C )  <->  ( p  =  ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  ->  B  =  [_ t  / 
s ]_ C ) ) )
65 poimirlem28.1 . . . . . . . . . 10  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  ->  B  =  C )
6652, 64, 65chvar 2068 . . . . . . . . 9  |-  ( p  =  ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  ->  B  =  [_ t  / 
s ]_ C )
6735, 48, 66chvar 2068 . . . . . . . 8  |-  ( p  =  ( ( 1st `  t )  oF  +  ( ( ( ( 2nd `  t
) " ( 1 ... k ) )  X.  { 1 } )  u.  ( ( ( 2nd `  t
) " ( ( k  +  1 ) ... N ) )  X.  { 0 } ) ) )  ->  B  =  [_ k  / 
j ]_ [_ t  / 
s ]_ C )
68 simpll 759 . . . . . . . . 9  |-  ( ( ( ph  /\  x  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C )  ->  ph )
69 poimirlem28.2 . . . . . . . . 9  |-  ( (
ph  /\  p :
( 1 ... N
) --> ( 0 ... K ) )  ->  B  e.  ( 0 ... N ) )
7068, 69sylan 474 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  ( (
( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )  /\  A. j  e.  ( 0 ... N
) N  =/=  [_ x  /  s ]_ C
)  /\  p :
( 1 ... N
) --> ( 0 ... K ) )  ->  B  e.  ( 0 ... N ) )
71 xp1st 6835 . . . . . . . . . 10  |-  ( x  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 1st `  x
)  e.  ( ( 0..^ K )  ^m  ( 1 ... N
) ) )
72 elmapi 7499 . . . . . . . . . 10  |-  ( ( 1st `  x )  e.  ( ( 0..^ K )  ^m  (
1 ... N ) )  ->  ( 1st `  x
) : ( 1 ... N ) --> ( 0..^ K ) )
7371, 72syl 17 . . . . . . . . 9  |-  ( x  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 1st `  x
) : ( 1 ... N ) --> ( 0..^ K ) )
7473ad2antlr 732 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C )  ->  ( 1st `  x ) : ( 1 ... N
) --> ( 0..^ K ) )
75 xp2nd 6836 . . . . . . . . . 10  |-  ( x  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 2nd `  x
)  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
76 fvex 5889 . . . . . . . . . . 11  |-  ( 2nd `  x )  e.  _V
77 f1oeq1 5820 . . . . . . . . . . 11  |-  ( f  =  ( 2nd `  x
)  ->  ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  x
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
7876, 77elab 3219 . . . . . . . . . 10  |-  ( ( 2nd `  x )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  <-> 
( 2nd `  x
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
7975, 78sylib 200 . . . . . . . . 9  |-  ( x  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 2nd `  x
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
8079ad2antlr 732 . . . . . . . 8  |-  ( ( ( ph  /\  x  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C )  ->  ( 2nd `  x ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) )
81 nfcv 2585 . . . . . . . . . . . . 13  |-  F/_ j N
82 nfcv 2585 . . . . . . . . . . . . . 14  |-  F/_ j
x
8382, 33nfcsb 3414 . . . . . . . . . . . . 13  |-  F/_ j [_ x  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C
8481, 83nfne 2757 . . . . . . . . . . . 12  |-  F/ j  N  =/=  [_ x  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C
85 nfcv 2585 . . . . . . . . . . . . . . 15  |-  F/_ t C
8685, 50, 62cbvcsb 3401 . . . . . . . . . . . . . 14  |-  [_ x  /  s ]_ C  =  [_ x  /  t ]_ [_ t  /  s ]_ C
8746csbeq2dv 3810 . . . . . . . . . . . . . 14  |-  ( j  =  k  ->  [_ x  /  t ]_ [_ t  /  s ]_ C  =  [_ x  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C )
8886, 87syl5eq 2476 . . . . . . . . . . . . 13  |-  ( j  =  k  ->  [_ x  /  s ]_ C  =  [_ x  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C )
8988neeq2d 2703 . . . . . . . . . . . 12  |-  ( j  =  k  ->  ( N  =/=  [_ x  /  s ]_ C  <->  N  =/=  [_ x  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C
) )
9084, 89rspc 3177 . . . . . . . . . . 11  |-  ( k  e.  ( 0 ... N )  ->  ( A. j  e.  (
0 ... N ) N  =/=  [_ x  /  s ]_ C  ->  N  =/=  [_ x  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C ) )
9190impcom 432 . . . . . . . . . 10  |-  ( ( A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C  /\  k  e.  (
0 ... N ) )  ->  N  =/=  [_ x  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C
)
9291adantll 719 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  ( (
( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )  /\  A. j  e.  ( 0 ... N
) N  =/=  [_ x  /  s ]_ C
)  /\  k  e.  ( 0 ... N
) )  ->  N  =/=  [_ x  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C )
93 1st2nd2 6842 . . . . . . . . . . 11  |-  ( x  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  ->  x  =  <. ( 1st `  x ) ,  ( 2nd `  x )
>. )
9493csbeq1d 3403 . . . . . . . . . 10  |-  ( x  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  ->  [_ x  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C  =  [_ <. ( 1st `  x ) ,  ( 2nd `  x
) >.  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C )
9594ad3antlr 736 . . . . . . . . 9  |-  ( ( ( ( ph  /\  x  e.  ( (
( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )  /\  A. j  e.  ( 0 ... N
) N  =/=  [_ x  /  s ]_ C
)  /\  k  e.  ( 0 ... N
) )  ->  [_ x  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C  =  [_ <. ( 1st `  x
) ,  ( 2nd `  x ) >.  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C )
9692, 95neeqtrd 2720 . . . . . . . 8  |-  ( ( ( ( ph  /\  x  e.  ( (
( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )  /\  A. j  e.  ( 0 ... N
) N  =/=  [_ x  /  s ]_ C
)  /\  k  e.  ( 0 ... N
) )  ->  N  =/=  [_ <. ( 1st `  x
) ,  ( 2nd `  x ) >.  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C )
9731, 67, 70, 74, 80, 96poimirlem25 31885 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C )  ->  2  ||  ( # `  {
y  e.  ( 0 ... N )  | 
A. i  e.  ( 0 ... ( N  -  1 ) ) E. k  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ <. ( 1st `  x
) ,  ( 2nd `  x ) >.  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C } ) )
98 nfv 1752 . . . . . . . . . . . . . 14  |-  F/ k  i  =  [_ x  /  s ]_ C
9983nfeq2 2602 . . . . . . . . . . . . . 14  |-  F/ j  i  =  [_ x  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C
10088eqeq2d 2437 . . . . . . . . . . . . . 14  |-  ( j  =  k  ->  (
i  =  [_ x  /  s ]_ C  <->  i  =  [_ x  / 
t ]_ [_ k  / 
j ]_ [_ t  / 
s ]_ C ) )
10198, 99, 100cbvrex 3053 . . . . . . . . . . . . 13  |-  ( E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ x  /  s ]_ C  <->  E. k  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ x  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C
)
10294eqeq2d 2437 . . . . . . . . . . . . . 14  |-  ( x  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( i  =  [_ x  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C  <->  i  =  [_ <. ( 1st `  x ) ,  ( 2nd `  x
) >.  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C ) )
103102rexbidv 2940 . . . . . . . . . . . . 13  |-  ( x  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( E. k  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
t ]_ [_ k  / 
j ]_ [_ t  / 
s ]_ C  <->  E. k  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. ( 1st `  x ) ,  ( 2nd `  x
) >.  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C ) )
104101, 103syl5rbb 262 . . . . . . . . . . . 12  |-  ( x  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( E. k  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. ( 1st `  x ) ,  ( 2nd `  x
) >.  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C 
<->  E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ x  /  s ]_ C ) )
105104ralbidv 2865 . . . . . . . . . . 11  |-  ( x  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( A. i  e.  ( 0 ... ( N  -  1 ) ) E. k  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. ( 1st `  x ) ,  ( 2nd `  x
) >.  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C 
<-> 
A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ x  /  s ]_ C ) )
106 iba 506 . . . . . . . . . . 11  |-  ( A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C  ->  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ x  /  s ]_ C  <->  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N
) N  =/=  [_ x  /  s ]_ C
) ) )
107105, 106sylan9bb 705 . . . . . . . . . 10  |-  ( ( x  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C )  ->  ( A. i  e.  (
0 ... ( N  - 
1 ) ) E. k  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ <. ( 1st `  x
) ,  ( 2nd `  x ) >.  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C  <->  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) ) )
108107rabbidv 3073 . . . . . . . . 9  |-  ( ( x  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C )  ->  { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. k  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ <. ( 1st `  x
) ,  ( 2nd `  x ) >.  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C }  =  {
y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } )
109108fveq2d 5883 . . . . . . . 8  |-  ( ( x  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C )  ->  ( # `
 { y  e.  ( 0 ... N
)  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. k  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. ( 1st `  x ) ,  ( 2nd `  x
) >.  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C } )  =  (
# `  { y  e.  ( 0 ... N
)  |  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C
) } ) )
110109adantll 719 . . . . . . 7  |-  ( ( ( ph  /\  x  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C )  ->  ( # `
 { y  e.  ( 0 ... N
)  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. k  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. ( 1st `  x ) ,  ( 2nd `  x
) >.  /  t ]_ [_ k  /  j ]_ [_ t  /  s ]_ C } )  =  (
# `  { y  e.  ( 0 ... N
)  |  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C
) } ) )
11197, 110breqtrd 4446 . . . . . 6  |-  ( ( ( ph  /\  x  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C )  ->  2  ||  ( # `  {
y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } ) )
112111ex 436 . . . . 5  |-  ( (
ph  /\  x  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )  ->  ( A. j  e.  (
0 ... N ) N  =/=  [_ x  /  s ]_ C  ->  2  ||  ( # `  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N
) N  =/=  [_ x  /  s ]_ C
) } ) ) )
113 dvds0 14311 . . . . . . . 8  |-  ( 2  e.  ZZ  ->  2  ||  0 )
11417, 113ax-mp 5 . . . . . . 7  |-  2  ||  0
115 hash0 12549 . . . . . . 7  |-  ( # `  (/) )  =  0
116114, 115breqtrri 4447 . . . . . 6  |-  2  ||  ( # `  (/) )
117 simpr 463 . . . . . . . . . 10  |-  ( ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N
) N  =/=  [_ x  /  s ]_ C
)  ->  A. j  e.  ( 0 ... N
) N  =/=  [_ x  /  s ]_ C
)
118117con3i 141 . . . . . . . . 9  |-  ( -. 
A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C  ->  -.  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) )
119118ralrimivw 2841 . . . . . . . 8  |-  ( -. 
A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C  ->  A. y  e.  ( 0 ... N )  -.  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) )
120 rabeq0 3785 . . . . . . . 8  |-  ( { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) }  =  (/)  <->  A. y  e.  ( 0 ... N )  -.  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) )
121119, 120sylibr 216 . . . . . . 7  |-  ( -. 
A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C  ->  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) }  =  (/) )
122121fveq2d 5883 . . . . . 6  |-  ( -. 
A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C  ->  ( # `  {
y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } )  =  ( # `  (/) ) )
123116, 122syl5breqr 4458 . . . . 5  |-  ( -. 
A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C  ->  2  ||  ( # `  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } ) )
124112, 123pm2.61d1 163 . . . 4  |-  ( (
ph  /\  x  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )  ->  2  ||  ( # `  {
y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } ) )
125 hashxp 12605 . . . . . 6  |-  ( ( { x }  e.  Fin  /\  { y  e.  ( 0 ... N
)  |  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C
) }  e.  Fin )  ->  ( # `  ( { x }  X.  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } ) )  =  ( (
# `  { x } )  x.  ( # `
 { y  e.  ( 0 ... N
)  |  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C
) } ) ) )
12619, 22, 125mp2an 677 . . . . 5  |-  ( # `  ( { x }  X.  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } ) )  =  ( (
# `  { x } )  x.  ( # `
 { y  e.  ( 0 ... N
)  |  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C
) } ) )
127 vex 3085 . . . . . . 7  |-  x  e. 
_V
128 hashsng 12550 . . . . . . 7  |-  ( x  e.  _V  ->  ( # `
 { x }
)  =  1 )
129127, 128ax-mp 5 . . . . . 6  |-  ( # `  { x } )  =  1
130129oveq1i 6313 . . . . 5  |-  ( (
# `  { x } )  x.  ( # `
 { y  e.  ( 0 ... N
)  |  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ x  /  s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C
) } ) )  =  ( 1  x.  ( # `  {
y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } ) )
131 hashcl 12539 . . . . . . . 8  |-  ( { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) }  e.  Fin  ->  ( # `  {
y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } )  e.  NN0 )
13222, 131ax-mp 5 . . . . . . 7  |-  ( # `  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } )  e.  NN0
133132nn0cni 10883 . . . . . 6  |-  ( # `  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } )  e.  CC
134133mulid2i 9648 . . . . 5  |-  ( 1  x.  ( # `  {
y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } ) )  =  ( # `  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } )
135126, 130, 1343eqtri 2456 . . . 4  |-  ( # `  ( { x }  X.  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } ) )  =  ( # `  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } )
136124, 135syl6breqr 4462 . . 3  |-  ( (
ph  /\  x  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )  ->  2  ||  ( # `  ( { x }  X.  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } ) ) )
13716, 18, 28, 136fsumdvds 14341 . 2  |-  ( ph  ->  2  ||  sum_ x  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) ( # `  ( { x }  X.  { y  e.  ( 0 ... N )  |  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ x  / 
s ]_ C  /\  A. j  e.  ( 0 ... N ) N  =/=  [_ x  /  s ]_ C ) } ) ) )
1384, 13, 15mp2an 677 . . . . . 6  |-  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  e. 
Fin
139 xpfi 7846 . . . . . 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 )
140138, 20, 139mp2an 677 . . . . 5  |-  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  e.  Fin
141 rabfi 7800 . . . . 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
) )  |  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { ( 2nd `  t ) } ) i  =  [_ ( 1st `  t )  / 
s ]_ C }  e.  Fin )
142140, 141ax-mp 5 . . . 4  |-  { 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 }  e.  Fin
14329nncnd 10627 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  CC )
144 npcan1 10046 . . . . . . . . . . . 12  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
145143, 144syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
146 nnm1nn0 10913 . . . . . . . . . . . . . 14  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  NN0 )
14729, 146syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  -  1 )  e.  NN0 )
148147nn0zd 11040 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  -  1 )  e.  ZZ )
149 uzid 11175 . . . . . . . . . . . 12  |-  ( ( N  -  1 )  e.  ZZ  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
150 peano2uz 11214 . . . . . . . . . . . 12  |-  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
151148, 149, 1503syl 18 . . . . . . . . . . 11  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1
) ) )
152145, 151eqeltrrd 2512 . . . . . . . . . 10  |-  ( ph  ->  N  e.  ( ZZ>= `  ( N  -  1
) ) )
153 fzss2 11840 . . . . . . . . . 10  |-  ( N  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( 0 ... ( N  - 
1 ) )  C_  ( 0 ... N
) )
154 ssralv 3526 . . . . . . . . . 10  |-  ( ( 0 ... ( N  -  1 ) ) 
C_  ( 0 ... N )  ->  ( A. i  e.  (
0 ... N ) E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  /  s ]_ C  ->  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
) )
155152, 153, 1543syl 18 . . . . . . . . 9  |-  ( ph  ->  ( A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C  ->  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  / 
s ]_ C ) )
156155adantr 467 . . . . . . . 8  |-  ( (
ph  /\  N  =  [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  ->  ( A. i  e.  (
0 ... N ) E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  /  s ]_ C  ->  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
) )
157 raldifb 3606 . . . . . . . . . . . 12  |-  ( A. j  e.  ( 0 ... N ) ( j  e/  { ( 2nd `  t ) }  ->  -.  i  =  [_ ( 1st `  t
)  /  s ]_ C )  <->  A. j  e.  ( ( 0 ... N )  \  {
( 2nd `  t
) } )  -.  i  =  [_ ( 1st `  t )  / 
s ]_ C )
158 nfv 1752 . . . . . . . . . . . . . . 15  |-  F/ j
ph
159 nfcsb1v 3412 . . . . . . . . . . . . . . . 16  |-  F/_ j [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C
160159nfeq2 2602 . . . . . . . . . . . . . . 15  |-  F/ j  N  =  [_ ( 2nd `  t )  / 
j ]_ [_ ( 1st `  t )  /  s ]_ C
161158, 160nfan 1985 . . . . . . . . . . . . . 14  |-  F/ j ( ph  /\  N  =  [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )
162 nfv 1752 . . . . . . . . . . . . . 14  |-  F/ j  i  e.  ( 0 ... ( N  - 
1 ) )
163161, 162nfan 1985 . . . . . . . . . . . . 13  |-  F/ j ( ( ph  /\  N  =  [_ ( 2nd `  t )  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  /\  i  e.  ( 0 ... ( N  -  1 ) ) )
164 nnel 2771 . . . . . . . . . . . . . . . . 17  |-  ( -.  j  e/  { ( 2nd `  t ) }  <->  j  e.  {
( 2nd `  t
) } )
165 elsn 4011 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  { ( 2nd `  t ) }  <->  j  =  ( 2nd `  t ) )
166164, 165bitri 253 . . . . . . . . . . . . . . . 16  |-  ( -.  j  e/  { ( 2nd `  t ) }  <->  j  =  ( 2nd `  t ) )
167 csbeq1a 3405 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  ( 2nd `  t
)  ->  [_ ( 1st `  t )  /  s ]_ C  =  [_ ( 2nd `  t )  / 
j ]_ [_ ( 1st `  t )  /  s ]_ C )
168167eqeq2d 2437 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  ( 2nd `  t
)  ->  ( N  =  [_ ( 1st `  t
)  /  s ]_ C 
<->  N  =  [_ ( 2nd `  t )  / 
j ]_ [_ ( 1st `  t )  /  s ]_ C ) )
169168biimparc 490 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  =  [_ ( 2nd `  t )  / 
j ]_ [_ ( 1st `  t )  /  s ]_ C  /\  j  =  ( 2nd `  t
) )  ->  N  =  [_ ( 1st `  t
)  /  s ]_ C )
17029nnred 10626 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  N  e.  RR )
171170ltm1d 10541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( N  -  1 )  <  N )
172147nn0red 10928 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ph  ->  ( N  -  1 )  e.  RR )
173172, 170ltnled 9784 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( ( N  - 
1 )  <  N  <->  -.  N  <_  ( N  -  1 ) ) )
174171, 173mpbid 214 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  -.  N  <_  ( N  -  1 ) )
175 elfzle2 11805 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  e.  ( 0 ... ( N  -  1 ) )  ->  N  <_  ( N  -  1 ) )
176174, 175nsyl 125 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  -.  N  e.  ( 0 ... ( N  -  1 ) ) )
177 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  N  ->  (
i  e.  ( 0 ... ( N  - 
1 ) )  <->  N  e.  ( 0 ... ( N  -  1 ) ) ) )
178177notbid 296 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( i  =  N  ->  ( -.  i  e.  (
0 ... ( N  - 
1 ) )  <->  -.  N  e.  ( 0 ... ( N  -  1 ) ) ) )
179176, 178syl5ibrcom 226 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( i  =  N  ->  -.  i  e.  ( 0 ... ( N  -  1 ) ) ) )
180179con2d 119 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( i  e.  ( 0 ... ( N  -  1 ) )  ->  -.  i  =  N ) )
181180imp 431 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  i  e.  ( 0 ... ( N  -  1 ) ) )  ->  -.  i  =  N )
182 eqeq2 2438 . . . . . . . . . . . . . . . . . . . . 21  |-  ( N  =  [_ ( 1st `  t )  /  s ]_ C  ->  ( i  =  N  <->  i  =  [_ ( 1st `  t
)  /  s ]_ C ) )
183182notbid 296 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  =  [_ ( 1st `  t )  /  s ]_ C  ->  ( -.  i  =  N  <->  -.  i  =  [_ ( 1st `  t
)  /  s ]_ C ) )
184181, 183syl5ibcom 224 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  i  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( N  =  [_ ( 1st `  t )  /  s ]_ C  ->  -.  i  =  [_ ( 1st `  t
)  /  s ]_ C ) )
185169, 184syl5 34 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  i  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( N  =  [_ ( 2nd `  t )  /  j ]_ [_ ( 1st `  t )  / 
s ]_ C  /\  j  =  ( 2nd `  t
) )  ->  -.  i  =  [_ ( 1st `  t )  /  s ]_ C ) )
186185expdimp 439 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  i  e.  ( 0 ... ( N  -  1 ) ) )  /\  N  =  [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  ->  (
j  =  ( 2nd `  t )  ->  -.  i  =  [_ ( 1st `  t )  /  s ]_ C ) )
187186an32s 812 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  N  =  [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  /\  i  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
j  =  ( 2nd `  t )  ->  -.  i  =  [_ ( 1st `  t )  /  s ]_ C ) )
188166, 187syl5bi 221 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  N  =  [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  /\  i  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( -.  j  e/  { ( 2nd `  t ) }  ->  -.  i  =  [_ ( 1st `  t
)  /  s ]_ C ) )
189 idd 26 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  N  =  [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  /\  i  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( -.  i  =  [_ ( 1st `  t )  / 
s ]_ C  ->  -.  i  =  [_ ( 1st `  t )  /  s ]_ C ) )
190188, 189jad 166 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  N  =  [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  /\  i  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( j  e/  {
( 2nd `  t
) }  ->  -.  i  =  [_ ( 1st `  t )  /  s ]_ C )  ->  -.  i  =  [_ ( 1st `  t )  /  s ]_ C ) )
191190adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  N  =  [_ ( 2nd `  t )  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  /\  i  e.  ( 0 ... ( N  -  1 ) ) )  /\  j  e.  ( 0 ... N
) )  ->  (
( j  e/  {
( 2nd `  t
) }  ->  -.  i  =  [_ ( 1st `  t )  /  s ]_ C )  ->  -.  i  =  [_ ( 1st `  t )  /  s ]_ C ) )
192163, 191ralimdaa 2828 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  N  =  [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  /\  i  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( A. j  e.  (
0 ... N ) ( j  e/  { ( 2nd `  t ) }  ->  -.  i  =  [_ ( 1st `  t
)  /  s ]_ C )  ->  A. j  e.  ( 0 ... N
)  -.  i  = 
[_ ( 1st `  t
)  /  s ]_ C ) )
193157, 192syl5bir 222 . . . . . . . . . . 11  |-  ( ( ( ph  /\  N  =  [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  /\  i  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( A. j  e.  (
( 0 ... N
)  \  { ( 2nd `  t ) } )  -.  i  = 
[_ ( 1st `  t
)  /  s ]_ C  ->  A. j  e.  ( 0 ... N )  -.  i  =  [_ ( 1st `  t )  /  s ]_ C
) )
194193con3d 139 . . . . . . . . . 10  |-  ( ( ( ph  /\  N  =  [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  /\  i  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( -.  A. j  e.  ( 0 ... N )  -.  i  =  [_ ( 1st `  t )  /  s ]_ C  ->  -.  A. j  e.  ( ( 0 ... N )  \  {
( 2nd `  t
) } )  -.  i  =  [_ ( 1st `  t )  / 
s ]_ C ) )
195 dfrex2 2877 . . . . . . . . . 10  |-  ( E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  /  s ]_ C  <->  -.  A. j  e.  ( 0 ... N
)  -.  i  = 
[_ ( 1st `  t
)  /  s ]_ C )
196 dfrex2 2877 . . . . . . . . . 10  |-  ( E. j  e.  ( ( 0 ... N ) 
\  { ( 2nd `  t ) } ) i  =  [_ ( 1st `  t )  / 
s ]_ C  <->  -.  A. j  e.  ( ( 0 ... N )  \  {
( 2nd `  t
) } )  -.  i  =  [_ ( 1st `  t )  / 
s ]_ C )
197194, 195, 1963imtr4g 274 . . . . . . . . 9  |-  ( ( ( ph  /\  N  =  [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  /\  i  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( E. j  e.  (
0 ... N ) i  =  [_ ( 1st `  t )  /  s ]_ C  ->  E. j  e.  ( ( 0 ... N )  \  {
( 2nd `  t
) } ) i  =  [_ ( 1st `  t )  /  s ]_ C ) )
198197ralimdva 2834 . . . . . . . 8  |-  ( (
ph  /\  N  =  [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  ->  ( A. i  e.  (
0 ... ( N  - 
1 ) ) E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  /  s ]_ C  ->  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
( 2nd `  t
) } ) i  =  [_ ( 1st `  t )  /  s ]_ C ) )
199156, 198syld 46 . . . . . . 7  |-  ( (
ph  /\  N  =  [_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C )  ->  ( A. i  e.  (
0 ... N ) E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  /  s ]_ C  ->  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
( 2nd `  t
) } ) i  =  [_ ( 1st `  t )  /  s ]_ C ) )
200199expimpd 607 . . . . . 6  |-  ( ph  ->  ( ( N  = 
[_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C  /\  A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
)  ->  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
( 2nd `  t
) } ) i  =  [_ ( 1st `  t )  /  s ]_ C ) )
201200adantr 467 . . . . 5  |-  ( (
ph  /\  t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) ) )  -> 
( ( N  = 
[_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C  /\  A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
)  ->  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
( 2nd `  t
) } ) i  =  [_ ( 1st `  t )  /  s ]_ C ) )
202201ss2rabdv 3543 . . . 4  |-  ( ph  ->  { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  ( N  = 
[_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C  /\  A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
) }  C_  { 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 } )
203 hashssdif 12588 . . . 4  |-  ( ( { 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 }  e.  Fin  /\ 
{ t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  ( N  = 
[_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C  /\  A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
) }  C_  { 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 } )  ->  ( # `  ( { 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 }  \  {
t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  ( N  = 
[_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C  /\  A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
) } ) )  =  ( ( # `  { 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 } )  -  ( # `  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  ( N  =  [_ ( 2nd `  t )  / 
j ]_ [_ ( 1st `  t )  /  s ]_ C  /\  A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
) } ) ) )
204142, 202, 203sylancr 668 . . 3  |-  ( ph  ->  ( # `  ( { 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 }  \  {
t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  ( N  = 
[_ ( 2nd `  t
)  /  j ]_ [_ ( 1st `  t
)  /  s ]_ C  /\  A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
) } ) )  =  ( ( # `  { 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 } )  -  ( # `  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  ( N  =  [_ ( 2nd `  t )  / 
j ]_ [_ ( 1st `  t )  /  s ]_ C  /\  A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
) } ) ) )
205 xp2nd 6836 . . . . . . . 8  |-  ( t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  ->  ( 2nd `  t )  e.  ( 0 ... N
) )
206 df-ne 2621 . . . . . . . . . . . 12  |-  ( N  =/=  [_ ( 1st `  t
)  /  s ]_ C 
<->  -.  N  =  [_ ( 1st `  t )  /  s ]_ C
)
207206ralbii 2857 . . . . . . . . . . 11  |-  ( A. j  e.  ( 0 ... N ) N  =/=  [_ ( 1st `  t
)  /  s ]_ C 
<-> 
A. j  e.  ( 0 ... N )  -.  N  =  [_ ( 1st `  t )  /  s ]_ C
)
208 ralnex 2872 . . . . . . . . . . 11  |-  ( A. j  e.  ( 0 ... N )  -.  N  =  [_ ( 1st `  t )  / 
s ]_ C  <->  -.  E. j  e.  ( 0 ... N
) N  =  [_ ( 1st `  t )  /  s ]_ C
)
209207, 208bitri 253 . . . . . . . . . 10  |-  ( A. j  e.  ( 0 ... N ) N  =/=  [_ ( 1st `  t
)  /  s ]_ C 
<->  -.  E. j  e.  ( 0 ... N
) N  =  [_ ( 1st `  t )  /  s ]_ C
)
21029nnnn0d 10927 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  NN0 )
211 nn0uz 11195 . . . . . . . . . . . . . . . . . . 19  |-  NN0  =  ( ZZ>= `  0 )
212210, 211syl6eleq 2521 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
213145, 212eqeltrd 2511 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  e.  ( ZZ>= ` 
0 ) )
214 fzsplit2 11826 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( N  - 
1 )  +  1 )  e.  ( ZZ>= ` 
0 )  /\  N  e.  ( ZZ>= `  ( N  -  1 ) ) )  ->  ( 0 ... N )  =  ( ( 0 ... ( N  -  1 ) )  u.  (
( ( N  - 
1 )  +  1 ) ... N ) ) )
215213, 152, 214syl2anc 666 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 0 ... N
)  =  ( ( 0 ... ( N  -  1 ) )  u.  ( ( ( N  -  1 )  +  1 ) ... N ) ) )
216145oveq1d 6318 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( ( N  -  1 )  +  1 ) ... N
)  =  ( N ... N ) )
21729nnzd 11041 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  ZZ )
218 fzsn 11842 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  ZZ  ->  ( N ... N )  =  { N } )
219217, 218syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( N ... N
)  =  { N } )
220216, 219eqtrd 2464 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( ( N  -  1 )  +  1 ) ... N
)  =  { N } )
221220uneq2d 3621 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 0 ... ( N  -  1 ) )  u.  (
( ( N  - 
1 )  +  1 ) ... N ) )  =  ( ( 0 ... ( N  -  1 ) )  u.  { N }
) )
222215, 221eqtrd 2464 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 0 ... N
)  =  ( ( 0 ... ( N  -  1 ) )  u.  { N }
) )
223222raleqdv 3032 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C  <->  A. i  e.  ( ( 0 ... ( N  -  1 ) )  u.  { N }
) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
) )
224 difss 3593 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0 ... N ) 
\  { ( 2nd `  t ) } ) 
C_  ( 0 ... N )
225 ssrexv 3527 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 0 ... N
)  \  { ( 2nd `  t ) } )  C_  ( 0 ... N )  -> 
( E. j  e.  ( ( 0 ... N )  \  {
( 2nd `  t
) } ) i  =  [_ ( 1st `  t )  /  s ]_ C  ->  E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
) )
226224, 225ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( E. j  e.  ( ( 0 ... N ) 
\  { ( 2nd `  t ) } ) i  =  [_ ( 1st `  t )  / 
s ]_ C  ->  E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
)
227226ralimi 2819 . . . . . . . . . . . . . . . 16  |-  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { ( 2nd `  t ) } ) i  =  [_ ( 1st `  t )  / 
s ]_ C  ->  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
)
228227biantrurd 511 . . . . . . . . . . . . . . 15  |-  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { ( 2nd `  t ) } ) i  =  [_ ( 1st `  t )  / 
s ]_ C  ->  ( A. i  e.  { N } E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  / 
s ]_ C  <->  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  /  s ]_ C  /\  A. i  e.  { N } E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  /  s ]_ C ) ) )
229 ralunb 3648 . . . . . . . . . . . . . . 15  |-  ( A. i  e.  ( (
0 ... ( N  - 
1 ) )  u. 
{ N } ) E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  / 
s ]_ C  <->  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  /  s ]_ C  /\  A. i  e.  { N } E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  /  s ]_ C ) )
230228, 229syl6rbbr 268 . . . . . . . . . . . . . 14  |-  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { ( 2nd `  t ) } ) i  =  [_ ( 1st `  t )  / 
s ]_ C  ->  ( A. i  e.  (
( 0 ... ( N  -  1 ) )  u.  { N } ) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C  <->  A. i  e.  { N } E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  / 
s ]_ C ) )
231223, 230sylan9bb 705 . . . . . . . . . . . . 13  |-  ( (
ph  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
( 2nd `  t
) } ) i  =  [_ ( 1st `  t )  /  s ]_ C )  ->  ( A. i  e.  (
0 ... N ) E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  /  s ]_ C  <->  A. i  e.  { N } E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C
) )
232231adantlr 720 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( 2nd `  t )  e.  ( 0 ... N
) )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { ( 2nd `  t ) } ) i  =  [_ ( 1st `  t )  / 
s ]_ C )  -> 
( A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( 1st `  t )  /  s ]_ C  <->  A. i  e.  { N } E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  / 
s ]_ C ) )
233 nn0fz0 11892 . . . . . . . . . . . . . . . 16  |-  ( N  e.  NN0  <->  N  e.  (
0 ... N ) )
234210, 233sylib 200 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  ( 0 ... N ) )
235234ad2antrr 731 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( 2nd `  t )  e.  ( 0 ... N
) )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { ( 2nd `  t ) } ) i  =  [_ ( 1st `  t )  / 
s ]_ C )  ->  N  e.  ( 0 ... N ) )
236 eqeq1 2427 . . . . . . . . . . . . . . . . 17  |-  ( i  =  N  ->  (
i  =  [_ ( 1st `  t )  / 
s ]_ C  <->  N  =  [_ ( 1st `  t
)  /  s ]_ C ) )
237236rexbidv 2940 . . . . . . . . . . . . . . . 16  |-  ( i  =  N  ->  ( E. j  e.  (
0 ... N ) i  =  [_ ( 1st `  t )  /  s ]_ C  <->  E. j  e.  ( 0 ... N ) N  =  [_ ( 1st `  t )  / 
s ]_ C ) )
238237rspcva 3181 . . . . . . . . . . . . . . 15  |-  ( ( N  e.  ( 0 ... N )  /\  A. i  e.  ( 0 ... N ) E. j  e.  ( 0 ... N ) i  =  [_ ( 1st `  t )  /  s ]_ C )  ->  E. j  e.  ( 0 ... N
) N  =  [_ ( 1st `  t )  /  s ]_ C
)
239 nfv 1752 . . . . . . . . . . . . . . . . 17  |-  F/ j ( ph  /\  ( 2nd `  t )  e.  ( 0 ... N
) )
240 nfcv 2585 . . . . . . . . . . . . . . . . . 18  |-  F/_ j
( 0 ... ( N  -  1 ) )
241 nfre1 2887 . . . . . . . . . . . . . . . . . 18  |-  F/ j E. j  e.  ( ( 0 ... N
)  \  { ( 2nd `  t ) } ) i  =  [_ ( 1st `  t )  /  s ]_ C
242240, 241nfral 2812 . . . . . . . . . . . . . . . . 17  |-  F/ j A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { ( 2nd `  t ) } ) i  =  [_ ( 1st `  t )  /  s ]_ C
243239, 242nfan 1985 . . . . . . . . . . . . . . . 16  |-  F/ j ( ( ph  /\  ( 2nd `  t )  e.  ( 0 ... N ) )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { ( 2nd `  t ) } ) i  =  [_ ( 1st `  t )  / 
s ]_ C )
244 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( N  =  [_ ( 1st `  t )  /  s ]_ C  ->  ( N  e.  ( 0 ... ( N  -  1 ) )  <->  [_ ( 1st `  t )  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) ) ) )
245244notbid 296 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( N  =  [_ ( 1st `  t )  /  s ]_ C  ->  ( -.  N  e.  ( 0 ... ( N  - 
1 ) )  <->  -.  [_ ( 1st `  t )  / 
s ]_ C  e.  ( 0 ... ( N  -  1 ) ) ) )
246176, 245syl5ibcom 224 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( N  =  [_ ( 1st `  t )  /  s ]_ C  ->  -.  [_ ( 1st `  t )  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) ) ) )
247246ad3antrrr 735 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  ( 2nd `  t )  e.  ( 0 ... N ) )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { ( 2nd `  t ) } ) i  =  [_ ( 1st `  t )  / 
s ]_ C )  /\  j  e.  ( 0 ... N ) )  ->  ( N  = 
[_ ( 1st `  t
)  /  s ]_ C  ->  -.  [_ ( 1st `  t )  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) ) ) )
248 eldifsn 4123 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  e.  ( ( 0 ... N )  \  { ( 2nd `  t
) } )  <->  ( j  e.  ( 0 ... N
)  /\  j  =/=  ( 2nd `  t ) ) )
249 diffi 7807 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( 0 ... N )  e.  Fin  ->  (
( 0 ... N
)  \  { ( 2nd `  t ) } )  e.  Fin )
25020, 249ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 0 ... N ) 
\  { ( 2nd `  t ) } )  e.  Fin
251 ssrab2 3547 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  { j  e.  ( ( 0 ... N )  \  { ( 2nd `  t
) } )  | 
[_ ( 1st `  t
)  /  s ]_ C  e.  ( 0 ... ( N  - 
1 ) ) } 
C_  ( ( 0 ... N )  \  { ( 2nd `  t
) } )
252 ssdomg 7620 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( 0 ... N
)  \  { ( 2nd `  t ) } )  e.  Fin  ->  ( { j  e.  ( ( 0 ... N
)  \  { ( 2nd `  t ) } )  |  [_ ( 1st `  t )  / 
s ]_ C  e.  ( 0 ... ( N  -  1 ) ) }  C_  ( (
0 ... N )  \  { ( 2nd `  t
) } )  ->  { j  e.  ( ( 0 ... N
)  \  { ( 2nd `  t ) } )  |  [_ ( 1st `  t )  / 
s ]_ C  e.  ( 0 ... ( N  -  1 ) ) }  ~<_  ( ( 0 ... N )  \  { ( 2nd `  t
) } ) ) )
253250, 251, 252mp2 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  { j  e.  ( ( 0 ... N )  \  { ( 2nd `  t
) } )  | 
[_ ( 1st `  t
)  /  s ]_ C  e.  ( 0 ... ( N  - 
1 ) ) }  ~<_  ( ( 0 ... N )  \  {
( 2nd `  t
) } )
254 snssi 4142 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( 2nd `  t )  e.  ( 0 ... N )  ->  { ( 2nd `  t ) }  C_  ( 0 ... N ) )
255 hashssdif 12588 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( 0 ... N
)  e.  Fin  /\  { ( 2nd `  t
) }  C_  (
0 ... N ) )  ->  ( # `  (
( 0 ... N
)  \  { ( 2nd `  t ) } ) )  =  ( ( # `  (
0 ... N ) )  -  ( # `  {
( 2nd `  t
) } ) ) )
25620, 254, 255sylancr 668 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( 2nd `  t )  e.  ( 0 ... N )  ->  ( # `
 ( ( 0 ... N )  \  { ( 2nd `  t
) } ) )  =  ( ( # `  ( 0 ... N
) )  -  ( # `
 { ( 2nd `  t ) } ) ) )
257 ax-1cn 9599 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  1  e.  CC
258 addsub 9888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( N  e.  CC  /\  1  e.  CC  /\  1  e.  CC )  ->  (
( N  +  1 )  -  1 )  =  ( ( N  -  1 )  +  1 ) )
259257, 257, 258mp3an23 1353 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( N  e.  CC  ->  (
( N  +  1 )  -  1 )  =  ( ( N  -  1 )  +  1 ) )
260143, 259syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( ( N  + 
1 )  -  1 )  =  ( ( N  -  1 )  +  1 ) )
261 hashfz0 12603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( N  e.  NN0  ->  ( # `  ( 0 ... N
) )  =  ( N  +  1 ) )
262210, 261syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( # `  (
0 ... N ) )  =  ( N  + 
1 ) )
263 fvex 5889 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( 2nd `  t )  e.  _V
264 hashsng 12550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( ( 2nd `  t )  e.  _V  ->  ( # `
 { ( 2nd `  t ) } )  =  1 )
265263, 264mp1i 13 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ph  ->  ( # `  {
( 2nd `  t
) } )  =  1 )
266262, 265oveq12d 6321 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( ( # `  (
0 ... N ) )  -  ( # `  {
( 2nd `  t
) } ) )  =  ( ( N  +  1 )  - 
1 ) )
267 hashfz0 12603 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( N  -  1 )  e.  NN0  ->  ( # `  ( 0 ... ( N  -  1 ) ) )  =  ( ( N  -  1 )  +  1 ) )
26829, 146, 2673syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  ( # `  (
0 ... ( N  - 
1 ) ) )  =  ( ( N  -  1 )  +  1 ) )
269260, 266, 2683eqtr4d 2474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( ( # `  (
0 ... N ) )  -  ( # `  {
( 2nd `  t
) } ) )  =  ( # `  (
0 ... ( N  - 
1 ) ) ) )
270256, 269sylan9eqr 2486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  ( 2nd `  t )  e.  ( 0 ... N ) )  ->  ( # `  (
( 0 ... N
)  \  { ( 2nd `  t ) } ) )  =  (
# `  ( 0 ... ( N  -  1 ) ) ) )
271 fzfi 12186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( 0 ... ( N  - 
1 ) )  e. 
Fin
272 hashen 12531 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( 0 ... N )  \  {
( 2nd `