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

Theorem poimirlem20 32005
Description: Lemma for poimir 32018 establishing existence for poimirlem21 32006. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0  |-  ( ph  ->  N  e.  NN )
poimirlem22.s  |-  S  =  { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  F  =  ( y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) }
poimirlem22.1  |-  ( ph  ->  F : ( 0 ... ( N  - 
1 ) ) --> ( ( 0 ... K
)  ^m  ( 1 ... N ) ) )
poimirlem22.2  |-  ( ph  ->  T  e.  S )
poimirlem22.3  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  E. p  e.  ran  F ( p `
 n )  =/=  0 )
poimirlem21.4  |-  ( ph  ->  ( 2nd `  T
)  =  N )
Assertion
Ref Expression
poimirlem20  |-  ( ph  ->  E. z  e.  S  z  =/=  T )
Distinct variable groups:    f, j, n, p, t, y, z    ph, j, n, y    j, F, n, y    j, N, n, y    T, j, n, y    ph, p, t    f, K, j, n, p, t    f, N, p, t    T, f, p    ph, z    f, F, p, t, z    z, K    z, N    t, T, z    S, j, n, p, t, y, z
Allowed substitution hints:    ph( f)    S( f)    K( y)

Proof of Theorem poimirlem20
StepHypRef Expression
1 oveq2 6323 . . . . . . . . 9  |-  ( 1  =  if ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
) ,  1 ,  0 )  ->  (
( ( 1st `  ( 1st `  T ) ) `
 n )  - 
1 )  =  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  -  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 N ) ,  1 ,  0 ) ) )
21eleq1d 2524 . . . . . . . 8  |-  ( 1  =  if ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
) ,  1 ,  0 )  ->  (
( ( ( 1st `  ( 1st `  T
) ) `  n
)  -  1 )  e.  ( 0..^ K )  <->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  -  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 N ) ,  1 ,  0 ) )  e.  ( 0..^ K ) ) )
3 oveq2 6323 . . . . . . . . 9  |-  ( 0  =  if ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
) ,  1 ,  0 )  ->  (
( ( 1st `  ( 1st `  T ) ) `
 n )  - 
0 )  =  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  -  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 N ) ,  1 ,  0 ) ) )
43eleq1d 2524 . . . . . . . 8  |-  ( 0  =  if ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
) ,  1 ,  0 )  ->  (
( ( ( 1st `  ( 1st `  T
) ) `  n
)  -  0 )  e.  ( 0..^ K )  <->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  -  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 N ) ,  1 ,  0 ) )  e.  ( 0..^ K ) ) )
5 fveq2 5888 . . . . . . . . . . . 12  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
)  ->  ( ( 1st `  ( 1st `  T
) ) `  n
)  =  ( ( 1st `  ( 1st `  T ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 N ) ) )
65oveq1d 6330 . . . . . . . . . . 11  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
)  ->  ( (
( 1st `  ( 1st `  T ) ) `
 n )  - 
1 )  =  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  -  1 ) )
76adantl 472 . . . . . . . . . 10  |-  ( (
ph  /\  n  =  ( ( 2nd `  ( 1st `  T ) ) `
 N ) )  ->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  -  1 )  =  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  -  1 ) )
8 poimirlem22.2 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  T  e.  S )
9 elrabi 3205 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T  e.  { t  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  |  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  t
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) }  ->  T  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )
10 poimirlem22.s . . . . . . . . . . . . . . . . . . . . 21  |-  S  =  { t  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  |  F  =  ( y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) }
119, 10eleq2s 2558 . . . . . . . . . . . . . . . . . . . 20  |-  ( T  e.  S  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) ) )
128, 11syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )
13 xp1st 6850 . . . . . . . . . . . . . . . . . . 19  |-  ( T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  ->  ( 1st `  T )  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
1412, 13syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1st `  T
)  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )
15 xp1st 6850 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1st `  T )  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  (
1 ... N ) ) )
1614, 15syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  (
1 ... N ) ) )
17 elmapi 7519 . . . . . . . . . . . . . . . . 17  |-  ( ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) )  ->  ( 1st `  ( 1st `  T ) ) : ( 1 ... N ) --> ( 0..^ K ) )
1816, 17syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1st `  ( 1st `  T ) ) : ( 1 ... N ) --> ( 0..^ K ) )
19 xp2nd 6851 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1st `  T )  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 2nd `  ( 1st `  T ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
2014, 19syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
21 fvex 5898 . . . . . . . . . . . . . . . . . . . 20  |-  ( 2nd `  ( 1st `  T
) )  e.  _V
22 f1oeq1 5828 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( 2nd `  ( 1st `  T ) )  ->  ( f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
2321, 22elab 3197 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2nd `  ( 1st `  T ) )  e. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) }  <->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
2420, 23sylib 201 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
25 f1of 5837 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) --> ( 1 ... N
) )
2624, 25syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) --> ( 1 ... N ) )
27 poimir.0 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  NN )
28 elfz1end 11858 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  NN  <->  N  e.  ( 1 ... N
) )
2927, 28sylib 201 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  N  e.  ( 1 ... N ) )
3026, 29ffvelrnd 6046 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) ) `
 N )  e.  ( 1 ... N
) )
3118, 30ffvelrnd 6046 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  e.  ( 0..^ K ) )
32 elfzonn0 11991 . . . . . . . . . . . . . . 15  |-  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  e.  ( 0..^ K )  -> 
( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  e.  NN0 )
3331, 32syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  e.  NN0 )
34 fvex 5898 . . . . . . . . . . . . . . . . 17  |-  ( ( 2nd `  ( 1st `  T ) ) `  N )  e.  _V
35 eleq1 2528 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
)  ->  ( n  e.  ( 1 ... N
)  <->  ( ( 2nd `  ( 1st `  T
) ) `  N
)  e.  ( 1 ... N ) ) )
3635anbi2d 715 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
)  ->  ( ( ph  /\  n  e.  ( 1 ... N ) )  <->  ( ph  /\  ( ( 2nd `  ( 1st `  T ) ) `
 N )  e.  ( 1 ... N
) ) ) )
37 fveq2 5888 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
)  ->  ( p `  n )  =  ( p `  ( ( 2nd `  ( 1st `  T ) ) `  N ) ) )
3837neeq1d 2695 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
)  ->  ( (
p `  n )  =/=  0  <->  ( p `  ( ( 2nd `  ( 1st `  T ) ) `
 N ) )  =/=  0 ) )
3938rexbidv 2913 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
)  ->  ( E. p  e.  ran  F ( p `  n )  =/=  0  <->  E. p  e.  ran  F ( p `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  =/=  0
) )
4036, 39imbi12d 326 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
)  ->  ( (
( ph  /\  n  e.  ( 1 ... N
) )  ->  E. p  e.  ran  F ( p `
 n )  =/=  0 )  <->  ( ( ph  /\  ( ( 2nd `  ( 1st `  T
) ) `  N
)  e.  ( 1 ... N ) )  ->  E. p  e.  ran  F ( p `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  =/=  0 ) ) )
41 poimirlem22.3 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  E. p  e.  ran  F ( p `
 n )  =/=  0 )
4234, 40, 41vtocl 3112 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( ( 2nd `  ( 1st `  T
) ) `  N
)  e.  ( 1 ... N ) )  ->  E. p  e.  ran  F ( p `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  =/=  0 )
4330, 42mpdan 679 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E. p  e.  ran  F ( p `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  =/=  0 )
44 fveq1 5887 . . . . . . . . . . . . . . . . . . . . 21  |-  ( p  =  ( ( 1st `  ( 1st `  T
) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) ) )  ->  ( p `  ( ( 2nd `  ( 1st `  T ) ) `
 N ) )  =  ( ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) ) ) `  ( ( 2nd `  ( 1st `  T ) ) `  N ) ) )
4530adantr 471 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  ( 1st `  T ) ) `
 N )  e.  ( 1 ... N
) )
46 ffn 5751 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 1st `  ( 1st `  T ) ) : ( 1 ... N
) --> ( 0..^ K )  ->  ( 1st `  ( 1st `  T
) )  Fn  (
1 ... N ) )
4718, 46syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
4847adantr 471 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( 1st `  ( 1st `  T
) )  Fn  (
1 ... N ) )
49 1ex 9664 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  1  e.  _V
50 fnconstg 5794 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 1  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) ) )
5149, 50ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )
52 c0ex 9663 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  e.  _V
53 fnconstg 5794 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( y  +  1 ) ... N ) ) )
5452, 53ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( y  +  1 ) ... N ) )
5551, 54pm3.2i 461 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  /\  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } )  Fn  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) )
56 dff1o3 5843 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( ( 2nd `  ( 1st `  T
) ) : ( 1 ... N )
-onto-> ( 1 ... N
)  /\  Fun  `' ( 2nd `  ( 1st `  T ) ) ) )
5756simprbi 470 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  Fun  `' ( 2nd `  ( 1st `  T ) ) )
5824, 57syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  Fun  `' ( 2nd `  ( 1st `  T
) ) )
59 imain 5681 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( Fun  `' ( 2nd `  ( 1st `  T ) )  ->  ( ( 2nd `  ( 1st `  T
) ) " (
( 1 ... y
)  i^i  ( (
y  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  i^i  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) ) )
6058, 59syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... y )  i^i  ( ( y  +  1 ) ... N
) ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " (
( y  +  1 ) ... N ) ) ) )
61 elfznn0 11916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  NN0 )
6261nn0red 10955 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  RR )
6362ltp1d 10565 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  <  ( y  +  1 ) )
64 fzdisj 11855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  <  ( y  +  1 )  ->  (
( 1 ... y
)  i^i  ( (
y  +  1 ) ... N ) )  =  (/) )
6563, 64syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
( 1 ... y
)  i^i  ( (
y  +  1 ) ... N ) )  =  (/) )
6665imaeq2d 5187 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
( 2nd `  ( 1st `  T ) )
" ( ( 1 ... y )  i^i  ( ( y  +  1 ) ... N
) ) )  =  ( ( 2nd `  ( 1st `  T ) )
" (/) ) )
67 ima0 5202 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 2nd `  ( 1st `  T ) ) " (/) )  =  (/)
6866, 67syl6eq 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
( 2nd `  ( 1st `  T ) )
" ( ( 1 ... y )  i^i  ( ( y  +  1 ) ... N
) ) )  =  (/) )
6960, 68sylan9req 2517 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  i^i  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) )  =  (/) )
70 fnun 5704 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... y
) )  X.  {
1 } )  Fn  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  /\  ( ( ( 2nd `  ( 1st `  T
) ) " (
( y  +  1 ) ... N ) )  X.  { 0 } )  Fn  (
( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) )  /\  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... y
) )  i^i  (
( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) )  =  (/) )  ->  (
( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) ) )
7155, 69, 70sylancr 674 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) ) )
72 imaundi 5267 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 2nd `  ( 1st `  T ) ) "
( ( 1 ... y )  u.  (
( y  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) )
73 nn0p1nn 10938 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  e.  NN0  ->  ( y  +  1 )  e.  NN )
74 nnuz 11223 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  NN  =  ( ZZ>= `  1 )
7573, 74syl6eleq 2550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  e.  NN0  ->  ( y  +  1 )  e.  ( ZZ>= `  1 )
)
7661, 75syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
y  +  1 )  e.  ( ZZ>= `  1
) )
7776adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
y  +  1 )  e.  ( ZZ>= `  1
) )
7827nncnd 10653 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  N  e.  CC )
79 npcan1 10072 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
8078, 79syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
8180adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  =  N )
82 elfzuz3 11826 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  ( N  -  1 )  e.  ( ZZ>= `  y
) )
83 peano2uz 11241 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( N  -  1 )  e.  ( ZZ>= `  y
)  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  y )
)
8482, 83syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
( N  -  1 )  +  1 )  e.  ( ZZ>= `  y
) )
8584adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  e.  ( ZZ>= `  y
) )
8681, 85eqeltrrd 2541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  y )
)
87 fzsplit2 11853 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( y  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ( ZZ>= `  y )
)  ->  ( 1 ... N )  =  ( ( 1 ... y )  u.  (
( y  +  1 ) ... N ) ) )
8877, 86, 87syl2anc 671 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
1 ... N )  =  ( ( 1 ... y )  u.  (
( y  +  1 ) ... N ) ) )
8988imaeq2d 5187 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... y )  u.  ( ( y  +  1 ) ... N
) ) ) )
90 f1ofo 5844 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N )
-onto-> ( 1 ... N
) )
91 foima 5821 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
) -onto-> ( 1 ... N )  ->  (
( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
9224, 90, 913syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
9392adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
9489, 93eqtr3d 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  ( 1st `  T ) )
" ( ( 1 ... y )  u.  ( ( y  +  1 ) ... N
) ) )  =  ( 1 ... N
) )
9572, 94syl5eqr 2510 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
9695fneq2d 5689 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... y
) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( y  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " (
( y  +  1 ) ... N ) ) )  <->  ( (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) )  Fn  ( 1 ... N ) ) )
9771, 96mpbid 215 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( 1 ... N ) )
98 ovex 6343 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 1 ... N )  e. 
_V
9998a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
1 ... N )  e. 
_V )
100 inidm 3653 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
101 eqidd 2463 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  (
( 2nd `  ( 1st `  T ) ) `
 N )  e.  ( 1 ... N
) )  ->  (
( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  =  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) ) )
102 f1ofn 5838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) )  Fn  (
1 ... N ) )
10324, 102syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
104103adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( 2nd `  ( 1st `  T
) )  Fn  (
1 ... N ) )
105 fzss1 11866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( y  +  1 )  e.  ( ZZ>= `  1
)  ->  ( (
y  +  1 ) ... N )  C_  ( 1 ... N
) )
10676, 105syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
( y  +  1 ) ... N ) 
C_  ( 1 ... N ) )
107106adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( y  +  1 ) ... N ) 
C_  ( 1 ... N ) )
108 eluzp1p1 11213 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( N  -  1 )  e.  ( ZZ>= `  y
)  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  ( y  +  1 ) ) )
109 uzss 11208 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  (
y  +  1 ) )  ->  ( ZZ>= `  ( ( N  - 
1 )  +  1 ) )  C_  ( ZZ>=
`  ( y  +  1 ) ) )
11082, 108, 1093syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  ( ZZ>=
`  ( ( N  -  1 )  +  1 ) )  C_  ( ZZ>= `  ( y  +  1 ) ) )
111110adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( ZZ>=
`  ( ( N  -  1 )  +  1 ) )  C_  ( ZZ>= `  ( y  +  1 ) ) )
11227nnzd 11068 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  N  e.  ZZ )
113 uzid 11202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  ZZ  ->  N  e.  ( ZZ>= `  N )
)
114112, 113syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  N  e.  ( ZZ>= `  N ) )
11580fveq2d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( ZZ>= `  ( ( N  -  1 )  +  1 ) )  =  ( ZZ>= `  N
) )
116114, 115eleqtrrd 2543 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  N  e.  ( ZZ>= `  ( ( N  - 
1 )  +  1 ) ) )
117116adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  ( ( N  -  1 )  +  1 ) ) )
118111, 117sseldd 3445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  ( y  +  1 ) ) )
119 eluzfz2 11836 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ( ZZ>= `  (
y  +  1 ) )  ->  N  e.  ( ( y  +  1 ) ... N
) )
120118, 119syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ( ( y  +  1 ) ... N
) )
121 fnfvima 6168 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 2nd `  ( 1st `  T ) )  Fn  ( 1 ... N )  /\  (
( y  +  1 ) ... N ) 
C_  ( 1 ... N )  /\  N  e.  ( ( y  +  1 ) ... N
) )  ->  (
( 2nd `  ( 1st `  T ) ) `
 N )  e.  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) )
122104, 107, 120, 121syl3anc 1276 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  ( 1st `  T ) ) `
 N )  e.  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) )
123 fvun2 5960 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  Fn  ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... y
) )  /\  (
( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( y  +  1 ) ... N ) )  /\  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  i^i  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) )  =  (/)  /\  (
( 2nd `  ( 1st `  T ) ) `
 N )  e.  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) ) )  ->  ( (
( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  ( ( 2nd `  ( 1st `  T ) ) `  N ) )  =  ( ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) `  ( ( 2nd `  ( 1st `  T ) ) `
 N ) ) )
12451, 54, 123mp3an12 1363 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " (
( y  +  1 ) ... N ) ) )  =  (/)  /\  ( ( 2nd `  ( 1st `  T ) ) `
 N )  e.  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) )  ->  ( ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  =  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
( y  +  1 ) ... N ) )  X.  { 0 } ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) ) )
12569, 122, 124syl2anc 671 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... y
) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( y  +  1 ) ... N ) )  X.  { 0 } ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 N ) )  =  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) ) )
12652fvconst2 6144 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 2nd `  ( 1st `  T ) ) `
 N )  e.  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  -> 
( ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) `  ( ( 2nd `  ( 1st `  T ) ) `
 N ) )  =  0 )
127122, 126syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( 2nd `  ( 1st `  T
) ) " (
( y  +  1 ) ... N ) )  X.  { 0 } ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  =  0 )
128125, 127eqtrd 2496 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... y
) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( y  +  1 ) ... N ) )  X.  { 0 } ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 N ) )  =  0 )
129128adantr 471 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  (
( 2nd `  ( 1st `  T ) ) `
 N )  e.  ( 1 ... N
) )  ->  (
( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... y
) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( y  +  1 ) ... N ) )  X.  { 0 } ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 N ) )  =  0 )
13048, 97, 99, 99, 100, 101, 129ofval 6567 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  (
( 2nd `  ( 1st `  T ) ) `
 N )  e.  ( 1 ... N
) )  ->  (
( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  =  ( ( ( 1st `  ( 1st `  T ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 N ) )  +  0 ) )
13145, 130mpdan 679 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  =  ( ( ( 1st `  ( 1st `  T ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 N ) )  +  0 ) )
13233nn0cnd 10956 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  e.  CC )
133132addid1d 9859 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  +  0 )  =  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) ) )
134133adantr 471 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  +  0 )  =  ( ( 1st `  ( 1st `  T ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 N ) ) )
135131, 134eqtrd 2496 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  =  ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) ) )
13644, 135sylan9eqr 2518 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  p  =  ( ( 1st `  ( 1st `  T
) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) ) ) )  ->  (
p `  ( ( 2nd `  ( 1st `  T
) ) `  N
) )  =  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) ) )
137136adantllr 730 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  p  e.  ran  F )  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  p  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )  -> 
( p `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  =  ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) ) )
138 fveq2 5888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( t  =  T  ->  ( 2nd `  t )  =  ( 2nd `  T
) )
139138breq2d 4428 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( t  =  T  ->  (
y  <  ( 2nd `  t )  <->  y  <  ( 2nd `  T ) ) )
140139ifbid 3915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( t  =  T  ->  if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  =  if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) ) )
141140csbeq1d 3382 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( t  =  T  ->  [_ if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  [_ if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
142 fveq2 5888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( t  =  T  ->  ( 1st `  t )  =  ( 1st `  T
) )
143142fveq2d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( t  =  T  ->  ( 1st `  ( 1st `  t
) )  =  ( 1st `  ( 1st `  T ) ) )
144142fveq2d 5892 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( t  =  T  ->  ( 2nd `  ( 1st `  t
) )  =  ( 2nd `  ( 1st `  T ) ) )
145144imaeq1d 5186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) ) )
146145xpeq1d 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... j
) )  X.  {
1 } ) )
147144imaeq1d 5186 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) ) )
148147xpeq1d 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )
149146, 148uneq12d 3601 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( t  =  T  ->  (
( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) )  =  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )
150143, 149oveq12d 6333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( t  =  T  ->  (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
151150csbeq2dv 3793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( t  =  T  ->  [_ if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  [_ if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
152141, 151eqtrd 2496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( t  =  T  ->  [_ if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  [_ if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
153152mpteq2dv 4504 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  T  ->  (
y  e.  ( 0 ... ( N  - 
1 ) )  |->  [_ if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )  =  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
154153eqeq2d 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  T  ->  ( F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  t
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )  <->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  [_ if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) ) )
155154, 10elrab2 3210 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( T  e.  S  <->  ( T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  /\  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) ) )
156155simprbi 470 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( T  e.  S  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
1578, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
15862adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  e.  RR )
159 peano2zm 11009 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
160112, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( N  -  1 )  e.  ZZ )
161160zred 11069 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( N  -  1 )  e.  RR )
162161adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( N  -  1 )  e.  RR )
16327nnred 10652 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  N  e.  RR )
164163adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  RR )
165 elfzle2 11832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  <_  ( N  -  1 ) )
166165adantl 472 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  <_  ( N  -  1 ) )
167163ltm1d 10567 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ph  ->  ( N  -  1 )  <  N )
168167adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( N  -  1 )  <  N )
169158, 162, 164, 166, 168lelttrd 9819 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  <  N )
170 poimirlem21.4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( 2nd `  T
)  =  N )
171170adantr 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( 2nd `  T )  =  N )
172169, 171breqtrrd 4443 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  <  ( 2nd `  T
) )
173172iftrued 3901 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  if ( y  <  ( 2nd `  T ) ,  y ,  ( y  +  1 ) )  =  y )
174173csbeq1d 3382 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  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  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
175 vex 3060 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  y  e. 
_V
176 oveq2 6323 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  =  y  ->  (
1 ... j )  =  ( 1 ... y
) )
177176imaeq2d 5187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  =  y  ->  (
( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) ) )
178177xpeq1d 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  =  y  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... y
) )  X.  {
1 } ) )
179 oveq1 6322 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  =  y  ->  (
j  +  1 )  =  ( y  +  1 ) )
180179oveq1d 6330 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  =  y  ->  (
( j  +  1 ) ... N )  =  ( ( y  +  1 ) ... N ) )
181180imaeq2d 5187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  =  y  ->  (
( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) ) )
182181xpeq1d 4876 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  =  y  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) )
183178, 182uneq12d 3601 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  =  y  ->  (
( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) )  =  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) ) )
184183oveq2d 6331 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  y  ->  (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
185175, 184csbie 3401 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  [_ y  /  j ]_ (
( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) )
186174, 185syl6eq 2512 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  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 } ) ) )  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
187186mpteq2dva 4503 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( 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 ) ) 
|->  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
188157, 187eqtrd 2496 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) ) ) ) )
189188rneqd 5081 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ran  F  =  ran  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
190189eleq2d 2525 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( p  e.  ran  F  <-> 
p  e.  ran  (
y  e.  ( 0 ... ( N  - 
1 ) )  |->  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) ) )
191 eqid 2462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) ) ) )  =  ( y  e.  ( 0 ... ( N  - 
1 ) )  |->  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
192 ovex 6343 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) ) )  e.  _V
193191, 192elrnmpti 5104 . . . . . . . . . . . . . . . . . . . . 21  |-  ( p  e.  ran  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) ) ) )  <->  E. y  e.  ( 0 ... ( N  -  1 ) ) p  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
194190, 193syl6bb 269 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( p  e.  ran  F  <->  E. y  e.  (
0 ... ( N  - 
1 ) ) p  =  ( ( 1st `  ( 1st `  T
) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) ) ) ) )
195194biimpa 491 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  p  e.  ran  F )  ->  E. y  e.  ( 0 ... ( N  -  1 ) ) p  =  ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
196137, 195r19.29a 2944 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  p  e.  ran  F )  ->  (
p `  ( ( 2nd `  ( 1st `  T
) ) `  N
) )  =  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) ) )
197196neeq1d 2695 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  p  e.  ran  F )  ->  (
( p `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  =/=  0  <->  ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  =/=  0 ) )
198197biimpd 212 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  p  e.  ran  F )  ->  (
( p `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  =/=  0  ->  (
( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  =/=  0
) )
199198rexlimdva 2891 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( E. p  e. 
ran  F ( p `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  =/=  0  ->  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  =/=  0
) )
20043, 199mpd 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  =/=  0
)
201 elnnne0 10912 . . . . . . . . . . . . . 14  |-  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  e.  NN  <->  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  e.  NN0  /\  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  =/=  0
) )
20233, 200, 201sylanbrc 675 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  e.  NN )
203 nnm1nn0 10940 . . . . . . . . . . . . 13  |-  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  e.  NN  ->  ( ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  -  1 )  e. 
NN0 )
204202, 203syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  -  1 )  e. 
NN0 )
205 elfzo0 11987 . . . . . . . . . . . . . 14  |-  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  e.  ( 0..^ K )  <->  ( (
( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  e.  NN0  /\  K  e.  NN  /\  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  <  K
) )
20631, 205sylib 201 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  e.  NN0  /\  K  e.  NN  /\  ( ( 1st `  ( 1st `  T ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 N ) )  <  K ) )
207206simp2d 1027 . . . . . . . . . . . 12  |-  ( ph  ->  K  e.  NN )
208204nn0red 10955 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  -  1 )  e.  RR )
20933nn0red 10955 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  e.  RR )
210207nnred 10652 . . . . . . . . . . . . 13  |-  ( ph  ->  K  e.  RR )
211209ltm1d 10567 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  -  1 )  < 
( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) ) )
212 elfzolt2 11960 . . . . . . . . . . . . . 14  |-  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  e.  ( 0..^ K )  -> 
( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  <  K
)
21331, 212syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  <  K
)
214208, 209, 210, 211, 213lttrd 9822 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  -  1 )  < 
K )
215 elfzo0 11987 . . . . . . . . . . . 12  |-  ( ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  -  1 )  e.  ( 0..^ K )  <->  ( (
( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  -  1 )  e.  NN0  /\  K  e.  NN  /\  (
( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  N
) )  -  1 )  <  K ) )
216204, 207, 214, 215syl3anbrc 1198 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 N ) )  -  1 )  e.  ( 0..^ K ) )
217216adantr 471 . . . . . . . . . 10  |-  ( (
ph  /\  n  =  ( ( 2nd `  ( 1st `  T ) ) `
 N ) )  ->  ( ( ( 1st `  ( 1st `  T ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 N ) )  -  1 )  e.  ( 0..^ K ) )
2187, 217eqeltrd 2540 . . . . . . . . 9  |-  ( (
ph  /\  n  =  ( ( 2nd `  ( 1st `  T ) ) `
 N ) )  ->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  -  1 )  e.  ( 0..^ K ) )
219218adantlr 726 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
) )  ->  (
( ( 1st `  ( 1st `  T ) ) `
 n )  - 
1 )  e.  ( 0..^ K ) )
22018ffvelrnda 6045 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( 1st `  ( 1st `  T ) ) `
 n )  e.  ( 0..^ K ) )
221 elfzonn0 11991 . . . . . . . . . . . . 13  |-  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  e.  ( 0..^ K )  ->  ( ( 1st `  ( 1st `  T
) ) `  n
)  e.  NN0 )
222220, 221syl 17 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( 1st `  ( 1st `  T ) ) `
 n )  e. 
NN0 )
223222nn0cnd 10956 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( 1st `  ( 1st `  T ) ) `
 n )  e.  CC )
224223subid1d 10001 . . . . . . . . . 10  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( ( 1st `  ( 1st `  T ) ) `
 n )  - 
0 )  =  ( ( 1st `  ( 1st `  T ) ) `
 n ) )
225224, 220eqeltrd 2540 . . . . . . . . 9  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( ( 1st `  ( 1st `  T ) ) `
 n )  - 
0 )  e.  ( 0..^ K ) )
226225adantr 471 . . . . . . . 8  |-  ( ( ( ph  /\  n  e.  ( 1 ... N
) )  /\  -.  n  =  ( ( 2nd `  ( 1st `  T
) ) `  N
) )  ->  (
( ( 1st `  ( 1st `  T ) ) `
 n )  - 
0 )  e.  ( 0..^ K ) )
2272, 4, 219, 226ifbothda 3928 . . . . . . 7  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  (
( ( 1st `  ( 1st `  T ) ) `
 n )  -  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 N ) ,  1 ,  0 ) )  e.  ( 0..^ K ) )
228 eqid 2462 . . . . . . 7  |-  ( n  e.  ( 1 ... N )  |->  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  -  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 N ) ,  1 ,  0 ) ) )  =  ( n  e.  ( 1 ... N )  |->  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  -  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 N ) ,  1 ,  0 ) ) )
229227, 228fmptd 6069 . . . . . 6  |-  ( ph  ->  ( n  e.  ( 1 ... N ) 
|->  ( ( ( 1st `  ( 1st `  T
) ) `  n
)  -  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `  N ) ,  1 ,  0 ) ) ) : ( 1 ... N ) --> ( 0..^ K ) )
230 ovex 6343 . . . . . . 7  |-  ( 0..^ K )  e.  _V
231230, 98elmap 7526 . . . . . 6  |-  ( ( n  e.  ( 1 ... N )  |->  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  -  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 N ) ,  1 ,  0 ) ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) )  <->  ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  -  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 N ) ,  1 ,  0 ) ) ) : ( 1 ... N ) --> ( 0..^ K ) )
232229, 231sylibr 217 . . . . 5  |-  ( ph  ->  ( n  e.  ( 1 ... N ) 
|->  ( ( ( 1st `  ( 1st `  T
) ) `  n
)  -  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `  N ) ,  1 ,  0 ) ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N
) ) )
233 simpr 467 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( ( 1  +  1 ) ... N
) )  ->  n  e.  ( ( 1  +  1 ) ... N
) )
234 1z 10996 . . . . . . . . . . . . . . . 16  |-  1  e.  ZZ
235 peano2z 11007 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  ZZ  ->  (
1  +  1 )  e.  ZZ )
236234, 235ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( 1  +  1 )  e.  ZZ
237112, 236jctil 544 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1  +  1 )  e.  ZZ  /\  N  e.  ZZ ) )
238 elfzelz 11829 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( ( 1  +  1 ) ... N )  ->  n  e.  ZZ )
239238, 234jctir 545 . . . . . . . . . . . . . 14  |-  ( n  e.  ( ( 1  +  1 ) ... N )  ->  (
n  e.  ZZ  /\  1  e.  ZZ )
)
240 fzsubel 11863 . . . . . . . . . . . . . 14  |-  ( ( ( ( 1  +  1 )  e.  ZZ  /\  N  e.  ZZ )  /\  ( n  e.  ZZ  /\  1  e.  ZZ ) )  -> 
( n  e.  ( ( 1  +  1 ) ... N )  <-> 
( n  -  1 )  e.  ( ( ( 1  +  1 )  -  1 ) ... ( N  - 
1 ) ) ) )
241237, 239, 240syl2an 484 . . . . . . . . . . . . 13  |-  ( (
ph  /\  n  e.  ( ( 1  +  1 ) ... N
) )  ->  (
n  e.  ( ( 1  +  1 ) ... N )  <->  ( n  -  1 )  e.  ( ( ( 1  +  1 )  - 
1 ) ... ( N  -  1 ) ) ) )
242233, 241mpbid 215 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  e.  ( ( 1  +  1 ) ... N
) )  ->  (
n  -  1 )  e.  ( ( ( 1  +  1 )  -  1 ) ... ( N  -  1 ) ) )
243 ax-1cn 9623 . . . . . . . . . . . . . 14  |-  1  e.  CC
244243, 243pncan3oi 9917 . . . . . . . . . . . . 13  |-  ( ( 1  +  1 )  -  1 )  =  1
245244oveq1i 6325 . . . . . . . . . . . 12  |-  ( ( ( 1  +  1 )  -  1 ) ... ( N  - 
1 ) )  =  ( 1 ... ( N  -  1 ) )
246242, 245syl6eleq 2550 . . . . . . . . . . 11  |-  ( (
ph  /\  n  e.  ( ( 1  +  1 ) ... N
) )  ->  (
n  -  1 )  e.  ( 1 ... ( N  -  1 ) ) )
247246ralrimiva 2814 . . . . . . . . . 10  |-  ( ph  ->  A. n  e.  ( ( 1  +  1 ) ... N ) ( n  -  1 )  e.  ( 1 ... ( N  - 
1 ) ) )
248 simpr 467 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( 1 ... ( N  -  1 ) ) )  ->  y  e.  ( 1 ... ( N  -  1 ) ) )
249160, 234jctil 544 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1  e.  ZZ  /\  ( N  -  1 )  e.  ZZ ) )
250 elfzelz 11829 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 1 ... ( N  -  1 ) )  ->  y  e.  ZZ )
251250, 234jctir 545 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 1 ... ( N  -  1 ) )  ->  (
y  e.  ZZ  /\  1  e.  ZZ )
)
252 fzaddel 11862 . . . . . . . . . . . . . . 15  |-  ( ( ( 1  e.  ZZ  /\  ( N  -  1 )  e.  ZZ )  /\  ( y  e.  ZZ  /\  1  e.  ZZ ) )  -> 
( y  e.  ( 1 ... ( N  -  1 ) )  <-> 
( y  +  1 )  e.  ( ( 1  +  1 ) ... ( ( N  -  1 )  +  1 ) ) ) )
253249, 251, 252syl2an 484 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( 1 ... ( N  -  1 ) ) )  ->  (
y  e.  ( 1 ... ( N  - 
1 ) )  <->  ( y  +  1 )  e.  ( ( 1  +  1 ) ... (
( N  -  1 )  +  1 ) ) ) )
254248, 253mpbid 215 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( 1 ... ( N  -  1 ) ) )  ->  (
y  +  1 )  e.  ( ( 1  +  1 ) ... ( ( N  - 
1 )  +  1 ) ) )
25580oveq2d 6331 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( 1  +  1 ) ... (
( N  -  1 )  +  1 ) )  =  ( ( 1  +  1 ) ... N ) )
256255adantr 471 . . . . . . . . . . . . 13  |-  ( (
ph  /\  y  e.  ( 1 ... ( N  -  1 ) ) )  ->  (
( 1  +  1 ) ... ( ( N  -  1 )  +  1 ) )  =  ( ( 1  +  1 ) ... N ) )
257254, 256eleqtrd 2542 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( 1 ... ( N  -  1 ) ) )  ->  (
y  +  1 )  e.  ( ( 1  +  1 ) ... N ) )
258238zcnd 11070 . . . . . . . . . . . . . . 15  |-  ( n  e.  ( ( 1  +  1 ) ... N )  ->  n  e.  CC )
259250zcnd 11070 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( 1 ... ( N  -  1 ) )  ->  y  e.  CC )
260 subadd2 9905 . . . . . . . . . . . . . . . . 17  |-  ( ( n  e.  CC  /\  1  e.  CC  /\  y  e.  CC )  ->  (
( n  -  1 )  =  y  <->  ( y  +  1 )  =  n ) )
261243, 260mp3an2 1361 . . . . . . . . . . . . . . . 16  |-  ( ( n  e.  CC  /\  y  e.  CC )  ->  ( ( n  - 
1 )  =  y  <-> 
( y  +  1 )  =  n ) )
262 eqcom 2469 . . . . . . . . . . . . . . . 16  |-  ( y  =  ( n  - 
1 )  <->  ( n  -  1 )  =  y )
263 eqcom 2469 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( y  +  1 )  <->  ( y  +  1 )  =  n )
264261, 262, 2633bitr4g 296 . . . . . . . . . . . . . . 15  |-  ( ( n  e.  CC  /\  y  e.  CC )  ->  ( y  =  ( n  -  1 )  <-> 
n  =  ( y  +  1 ) ) )
265258, 259, 264syl2anr 485 . . . . . . . . . . . . . 14  |-  ( ( y  e.  ( 1 ... ( N  - 
1 ) )  /\  n  e.  ( (
1  +  1 ) ... N ) )  ->  ( y  =  ( n  -  1 )  <->  n  =  (
y  +  1 ) ) )
266265ralrimiva 2814 . . . . . . . . . . . . 13  |-  ( y  e.  ( 1 ... ( N  -  1 ) )  ->  A. n  e.  ( ( 1  +  1 ) ... N
) ( y  =  ( n  -  1 )  <->  n  =  (
y  +  1 ) ) )
267266adantl 472 . . . . . . . . . . . 12  |-  ( (
ph  /\  y  e.  ( 1 ... ( N  -  1 ) ) )  ->  A. n  e.  ( ( 1  +  1 ) ... N
) ( y  =  ( n  -  1 )  <->  n  =  (
y  +  1 ) ) )
268 reu6i 3241 . . . . . . . . . . . 12  |-  ( ( ( y  +  1 )  e.  ( ( 1  +  1 ) ... N )  /\  A. n  e.  ( ( 1  +  1 ) ... N ) ( y  =  ( n  -  1 )  <->  n  =  ( y  +  1 ) ) )  ->  E! n  e.  (
( 1  +  1 ) ... N ) y  =  ( n  -  1 ) )
269257, 267, 268syl2anc 671 . . . . . . . . . . 11  |-  ( (
ph  /\  y  e.  ( 1 ... ( N  -  1 ) ) )  ->  E! n  e.  ( (
1  +  1 ) ... N ) y  =  ( n  - 
1 ) )
270269ralrimiva 2814 . . . . . . . . . 10  |-  ( ph  ->  A. y  e.  ( 1 ... ( N  -  1 ) ) E! n  e.  ( ( 1  +  1 ) ... N ) y  =  ( n  -  1 ) )
271 eqid 2462 . . . . . . . . . . 11  |-  ( n  e.  ( ( 1  +  1 ) ... N )  |->  ( n  -  1 ) )  =  ( n  e.  ( ( 1  +  1 ) ... N
)  |->  ( n  - 
1 ) )
272271f1ompt 6067 . . . . . . . . . 10  |-  ( ( n  e.  ( ( 1  +  1 ) ... N )  |->  ( n  -  1 ) ) : ( ( 1  +  1 ) ... N ) -1-1-onto-> ( 1 ... ( N  - 
1 ) )  <->  ( A. n  e.  ( (
1  +  1 ) ... N ) ( n  -  1 )  e.  ( 1 ... ( N  -  1 ) )  /\  A. y  e.  ( 1 ... ( N  - 
1 ) ) E! n  e.  ( ( 1  +  1 ) ... N ) y  =  ( n  - 
1 ) ) )
273247, 270, 272sylanbrc 675 . . . . . . . . 9  |-  ( ph  ->  ( n  e.  ( ( 1  +  1 ) ... N ) 
|->  ( n  -  1 ) ) : ( ( 1  +  1 ) ... N ) -1-1-onto-> ( 1 ... ( N  -  1 ) ) )
274 f1osng 5876 . . . . . . . . . 10  |-  ( ( 1  e.  _V  /\  N  e.  NN )  ->  { <. 1 ,  N >. } : { 1 } -1-1-onto-> { N } )
27549, 27, 274sylancr 674 . . . . . . . . 9  |-  ( ph  ->  { <. 1 ,  N >. } : { 1 } -1-1-onto-> { N } )
276161, 163ltnled 9808 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( N  - 
1 )  <  N  <->  -.  N  <_  ( N  -  1 ) ) )
277167, 276mpbid 215 . . . . . . . . . . 11  |-  ( ph  ->  -.  N  <_  ( N  -  1 ) )
278 elfzle2 11832 . . . . . . . . . . 11  |-  ( N  e.  ( 1 ... ( N  -  1 ) )  ->  N  <_  ( N  -  1 ) )
279277, 278nsyl 126 . . . . . . . . . 10  |-  ( ph  ->  -.  N  e.  ( 1 ... ( N  -  1 ) ) )
280 disjsn 4044 . . . . . . . . . 10  |-  ( ( ( 1 ... ( N  -  1 ) )  i^i  { N } )  =  (/)  <->  -.  N  e.  ( 1 ... ( N  - 
1 ) ) )
281279, 280sylibr 217 . . . . . . . . 9  |-  ( ph  ->  ( ( 1 ... ( N  -  1 ) )  i^i  { N } )  =  (/) )
282 1re 9668 . . . . . . . . . . . . . 14  |-  1  e.  RR
283282ltp1i 10538 . . . . . . . . . . . . 13  |-  1  <  ( 1  +  1 )
284236zrei 10972 . . . . . . . . . . . . . 14  |-  ( 1  +  1 )  e.  RR
285282, 284ltnlei 9781 . . . . . . . . . . . . 13  |-  ( 1  <  ( 1  +  1 )  <->  -.  (
1  +  1 )  <_  1 )
286283, 285mpbi 213 . . . . . . . . . . . 12  |-  -.  (
1  +  1 )  <_  1
287 elfzle1 11831 . . . . . . . . . . . 12  |-  ( 1  e.  ( ( 1  +  1 ) ... N )  ->  (
1  +  1 )  <_  1 )
288286, 287mto 181 . . . . . . . . . . 11  |-  -.  1  e.  ( ( 1  +  1 ) ... N
)
289 disjsn 4044 . . . . . . . . . . 11  |-  ( ( ( ( 1  +  1 ) ... N
)  i^i  { 1 } )  =  (/)  <->  -.  1  e.  ( (
1  +  1 ) ... N ) )
290288, 289mpbir 214 . . . . . . . . . 10  |-  ( ( ( 1  +  1 ) ... N )  i^i  { 1 } )  =  (/)
291 f1oun 5856 . . . . . . . . . 10  |-  ( ( ( ( n  e.  ( ( 1  +  1 ) ... N
)  |->  ( n  - 
1 ) ) : ( ( 1  +  1 ) ... N
)
-1-1-onto-> ( 1 ... ( N  -  1 ) )  /\  { <. 1 ,  N >. } : { 1 } -1-1-onto-> { N } )  /\  ( ( ( ( 1  +  1 ) ... N )  i^i 
{ 1 } )  =  (/)  /\  (
( 1 ... ( N  -  1 ) )  i^i  { N } )  =  (/) ) )  ->  (
( n  e.  ( ( 1  +  1 ) ... N ) 
|->  ( n  -  1 ) )  u.  { <. 1 ,  N >. } ) : ( ( ( 1  +  1 ) ... N )  u.  { 1 } ) -1-1-onto-> ( ( 1 ... ( N  -  1 ) )  u.  { N } ) )
292290, 291mpanr1 694 . . . . . . . . 9  |-  ( ( ( ( n  e.  ( ( 1  +  1 ) ... N
)  |->  ( n  - 
1 ) ) : ( ( 1  +  1 ) ... N
)
-1-1-onto-> ( 1 ... ( N  -  1 ) )  /\  { <. 1 ,  N >. } : { 1 } -1-1-onto-> { N } )  /\  ( ( 1 ... ( N  -  1 ) )  i^i  { N } )  =  (/) )  ->  ( ( n  e.  ( ( 1  +  1 ) ... N )  |->  ( n  -  1 ) )  u.  { <. 1 ,  N >. } ) : ( ( ( 1  +  1 ) ... N )  u.  {
1 } ) -1-1-onto-> ( ( 1 ... ( N  -  1 ) )  u.  { N }
) )
293273, 275, 281, 292syl21anc 1275 . . . . . . . 8  |-  ( ph  ->  ( ( n  e.  ( ( 1  +  1 ) ... N
)  |->  ( n  - 
1 ) )  u. 
{ <. 1 ,  N >. } ) : ( ( ( 1  +  1 ) ... N
)  u.  { 1 } ) -1-1-onto-> ( ( 1 ... ( N  -  1 ) )  u.  { N } ) )
294 eleq1 2528 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  (
n  e.  ( ( 1  +  1 ) ... N )  <->  1  e.  ( ( 1  +  1 ) ... N
) ) )
295288, 294mtbiri 309 . . . . . . . . . . . . . 14  |-  ( n  =  1  ->  -.  n  e.  ( (
1  +  1