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

Theorem poimirlem17 31921
Description: Lemma for poimir 31937 establishing existence for poimirlem18 31922. (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 )
poimirlem18.3  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  E. p  e.  ran  F ( p `
 n )  =/= 
K )
poimirlem18.4  |-  ( ph  ->  ( 2nd `  T
)  =  0 )
Assertion
Ref Expression
poimirlem17  |-  ( 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 poimirlem17
StepHypRef Expression
1 poimir.0 . . . . 5  |-  ( ph  ->  N  e.  NN )
2 poimirlem22.s . . . . 5  |-  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 } ) ) ) ) }
3 poimirlem22.1 . . . . 5  |-  ( ph  ->  F : ( 0 ... ( N  - 
1 ) ) --> ( ( 0 ... K
)  ^m  ( 1 ... N ) ) )
4 poimirlem22.2 . . . . 5  |-  ( ph  ->  T  e.  S )
5 poimirlem18.3 . . . . 5  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  E. p  e.  ran  F ( p `
 n )  =/= 
K )
6 poimirlem18.4 . . . . 5  |-  ( ph  ->  ( 2nd `  T
)  =  0 )
71, 2, 3, 4, 5, 6poimirlem16 31920 . . . 4  |-  ( ph  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  ( ( n  e.  ( 1 ... N )  |->  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) )  oF  +  ( ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( 1 ... y ) )  X.  { 1 } )  u.  ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( ( y  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) )
8 elfznn0 11894 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  NN0 )
98nn0red 10933 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  RR )
109adantl 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  e.  RR )
111nnzd 11046 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  ZZ )
12 peano2zm 10987 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
1311, 12syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( N  -  1 )  e.  ZZ )
1413zred 11047 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  -  1 )  e.  RR )
1514adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( N  -  1 )  e.  RR )
161nnred 10631 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  RR )
1716adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  RR )
18 elfzle2 11810 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  <_  ( N  -  1 ) )
1918adantl 467 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  <_  ( N  -  1 ) )
2016ltm1d 10546 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  -  1 )  <  N )
2120adantr 466 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( N  -  1 )  <  N )
2210, 15, 17, 19, 21lelttrd 9800 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  <  N )
2322adantlr 719 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  <  N )
24 fveq2 5881 . . . . . . . . . . . . . . 15  |-  ( t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >.  -> 
( 2nd `  t
)  =  ( 2nd `  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. ) )
25 opex 4685 . . . . . . . . . . . . . . . 16  |-  <. (
n  e.  ( 1 ... N )  |->  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >.  e.  _V
26 op2ndg 6820 . . . . . . . . . . . . . . . 16  |-  ( (
<. ( n  e.  ( 1 ... N ) 
|->  ( ( ( 1st `  ( 1st `  T
) ) `  n
)  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) ` 
1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N ) 
|->  if ( n  =  N ,  1 ,  ( n  +  1 ) ) ) )
>.  e.  _V  /\  N  e.  NN )  ->  ( 2nd `  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  =  N )
2725, 1, 26sylancr 667 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 2nd `  <. <.
( n  e.  ( 1 ... N ) 
|->  ( ( ( 1st `  ( 1st `  T
) ) `  n
)  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) ` 
1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N ) 
|->  if ( n  =  N ,  1 ,  ( n  +  1 ) ) ) )
>. ,  N >. )  =  N )
2824, 27sylan9eqr 2485 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  ->  ( 2nd `  t
)  =  N )
2928adantr 466 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( 2nd `  t )  =  N )
3023, 29breqtrrd 4450 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  y  <  ( 2nd `  t ) )
3130iftrued 3919 . . . . . . . . . . 11  |-  ( ( ( ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  if (
y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  =  y )
3231csbeq1d 3402 . . . . . . . . . 10  |-  ( ( ( ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  /\  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 } ) ) ) )
33 vex 3083 . . . . . . . . . . . . 13  |-  y  e. 
_V
34 oveq2 6313 . . . . . . . . . . . . . . . . 17  |-  ( j  =  y  ->  (
1 ... j )  =  ( 1 ... y
) )
3534imaeq2d 5187 . . . . . . . . . . . . . . . 16  |-  ( j  =  y  ->  (
( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  t ) )
" ( 1 ... y ) ) )
3635xpeq1d 4876 . . . . . . . . . . . . . . 15  |-  ( j  =  y  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  t ) ) "
( 1 ... y
) )  X.  {
1 } ) )
37 oveq1 6312 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  y  ->  (
j  +  1 )  =  ( y  +  1 ) )
3837oveq1d 6320 . . . . . . . . . . . . . . . . 17  |-  ( j  =  y  ->  (
( j  +  1 ) ... N )  =  ( ( y  +  1 ) ... N ) )
3938imaeq2d 5187 . . . . . . . . . . . . . . . 16  |-  ( j  =  y  ->  (
( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  t ) )
" ( ( y  +  1 ) ... N ) ) )
4039xpeq1d 4876 . . . . . . . . . . . . . . 15  |-  ( j  =  y  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  t ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) )
4136, 40uneq12d 3621 . . . . . . . . . . . . . 14  |-  ( 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 } ) ) )
4241oveq2d 6321 . . . . . . . . . . . . 13  |-  ( 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 } ) ) ) )
4333, 42csbie 3421 . . . . . . . . . . . 12  |-  [_ 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 } ) ) )
44 fveq2 5881 . . . . . . . . . . . . . . 15  |-  ( t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >.  -> 
( 1st `  t
)  =  ( 1st `  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. ) )
4544fveq2d 5885 . . . . . . . . . . . . . 14  |-  ( t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >.  -> 
( 1st `  ( 1st `  t ) )  =  ( 1st `  ( 1st `  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. ) ) )
46 op1stg 6819 . . . . . . . . . . . . . . . . 17  |-  ( (
<. ( n  e.  ( 1 ... N ) 
|->  ( ( ( 1st `  ( 1st `  T
) ) `  n
)  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) ` 
1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N ) 
|->  if ( n  =  N ,  1 ,  ( n  +  1 ) ) ) )
>.  e.  _V  /\  N  e.  NN )  ->  ( 1st `  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  =  <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. )
4725, 1, 46sylancr 667 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1st `  <. <.
( n  e.  ( 1 ... N ) 
|->  ( ( ( 1st `  ( 1st `  T
) ) `  n
)  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) ` 
1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N ) 
|->  if ( n  =  N ,  1 ,  ( n  +  1 ) ) ) )
>. ,  N >. )  =  <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. )
4847fveq2d 5885 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  ( 1st `  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. ) )  =  ( 1st `  <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ) )
49 ovex 6333 . . . . . . . . . . . . . . . . 17  |-  ( 1 ... N )  e. 
_V
5049mptex 6151 . . . . . . . . . . . . . . . 16  |-  ( n  e.  ( 1 ... N )  |->  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) )  e.  _V
51 fvex 5891 . . . . . . . . . . . . . . . . 17  |-  ( 2nd `  ( 1st `  T
) )  e.  _V
5249mptex 6151 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  ( 1 ... N )  |->  if ( n  =  N , 
1 ,  ( n  +  1 ) ) )  e.  _V
5351, 52coex 6759 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N ) 
|->  if ( n  =  N ,  1 ,  ( n  +  1 ) ) ) )  e.  _V
5450, 53op1st 6815 . . . . . . . . . . . . . . 15  |-  ( 1st `  <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. )  =  ( n  e.  ( 1 ... N )  |->  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) )
5548, 54syl6eq 2479 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1st `  ( 1st `  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. ) )  =  ( n  e.  ( 1 ... N )  |->  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) )
5645, 55sylan9eqr 2485 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  ->  ( 1st `  ( 1st `  t ) )  =  ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) )
5744, 47sylan9eqr 2485 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  ->  ( 1st `  t
)  =  <. (
n  e.  ( 1 ... N )  |->  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. )
5857fveq2d 5885 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  ->  ( 2nd `  ( 1st `  t ) )  =  ( 2nd `  <. ( n  e.  ( 1 ... N )  |->  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ) )
5950, 53op2nd 6816 . . . . . . . . . . . . . . . . 17  |-  ( 2nd `  <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. )  =  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) )
6058, 59syl6eq 2479 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  ->  ( 2nd `  ( 1st `  t ) )  =  ( ( 2nd `  ( 1st `  T
) )  o.  (
n  e.  ( 1 ... N )  |->  if ( n  =  N ,  1 ,  ( n  +  1 ) ) ) ) )
6160imaeq1d 5186 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  ->  ( ( 2nd `  ( 1st `  t
) ) " (
1 ... y ) )  =  ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N ) 
|->  if ( n  =  N ,  1 ,  ( n  +  1 ) ) ) )
" ( 1 ... y ) ) )
6261xpeq1d 4876 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  ->  ( ( ( 2nd `  ( 1st `  t ) ) "
( 1 ... y
) )  X.  {
1 } )  =  ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N ) 
|->  if ( n  =  N ,  1 ,  ( n  +  1 ) ) ) )
" ( 1 ... y ) )  X. 
{ 1 } ) )
6360imaeq1d 5186 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  ->  ( ( 2nd `  ( 1st `  t
) ) " (
( y  +  1 ) ... N ) )  =  ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( ( y  +  1 ) ... N ) ) )
6463xpeq1d 4876 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  ->  ( ( ( 2nd `  ( 1st `  t ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } )  =  ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N ) 
|->  if ( n  =  N ,  1 ,  ( n  +  1 ) ) ) )
" ( ( y  +  1 ) ... N ) )  X. 
{ 0 } ) )
6562, 64uneq12d 3621 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  ->  ( ( ( ( 2nd `  ( 1st `  t ) )
" ( 1 ... y ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) )  =  ( ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( 1 ... y ) )  X.  { 1 } )  u.  ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( ( y  +  1 ) ... N ) )  X.  { 0 } ) ) )
6656, 65oveq12d 6323 . . . . . . . . . . . 12  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  ->  ( ( 1st `  ( 1st `  t
) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t ) )
" ( 1 ... y ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) ) "
( ( y  +  1 ) ... N
) )  X.  {
0 } ) ) )  =  ( ( n  e.  ( 1 ... N )  |->  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) )  oF  +  ( ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( 1 ... y ) )  X.  { 1 } )  u.  ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( ( y  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
6743, 66syl5eq 2475 . . . . . . . . . . 11  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  ->  [_ y  /  j ]_ ( ( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( n  e.  ( 1 ... N ) 
|->  ( ( ( 1st `  ( 1st `  T
) ) `  n
)  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) ` 
1 ) ,  1 ,  0 ) ) )  oF  +  ( ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( 1 ... y ) )  X.  { 1 } )  u.  ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( ( y  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
6867adantr 466 . . . . . . . . . 10  |-  ( ( ( ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  [_ y  / 
j ]_ ( ( 1st `  ( 1st `  t
) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  =  ( ( n  e.  ( 1 ... N )  |->  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) )  oF  +  ( ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( 1 ... y ) )  X.  { 1 } )  u.  ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( ( y  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
6932, 68eqtrd 2463 . . . . . . . . 9  |-  ( ( ( ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  [_ if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  / 
j ]_ ( ( 1st `  ( 1st `  t
) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  =  ( ( n  e.  ( 1 ... N )  |->  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) )  oF  +  ( ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( 1 ... y ) )  X.  { 1 } )  u.  ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( ( y  +  1 ) ... N ) )  X.  { 0 } ) ) ) )
7069mpteq2dva 4510 . . . . . . . 8  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  N >. )  ->  ( 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 ) ) 
|->  ( ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) )  oF  +  ( ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( 1 ... y ) )  X.  { 1 } )  u.  ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( ( y  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) )
7170eqeq2d 2436 . . . . . . 7  |-  ( (
ph  /\  t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  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 } ) ) ) )  <->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  ( ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) )  oF  +  ( ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( 1 ... y ) )  X.  { 1 } )  u.  ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( ( y  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) ) )
7271ex 435 . . . . . 6  |-  ( ph  ->  ( t  =  <. <.
( n  e.  ( 1 ... N ) 
|->  ( ( ( 1st `  ( 1st `  T
) ) `  n
)  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) ` 
1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N ) 
|->  if ( n  =  N ,  1 ,  ( n  +  1 ) ) ) )
>. ,  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 } ) ) ) )  <->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  ( ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) )  oF  +  ( ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( 1 ... y ) )  X.  { 1 } )  u.  ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( ( y  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) ) ) )
7372alrimiv 1767 . . . . 5  |-  ( ph  ->  A. t ( t  =  <. <. ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) >. ,  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 } ) ) ) )  <->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) ) 
|->  ( ( n  e.  ( 1 ... N
)  |->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) )  oF  +  ( ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( 1 ... y ) )  X.  { 1 } )  u.  ( ( ( ( 2nd `  ( 1st `  T ) )  o.  ( n  e.  ( 1 ... N
)  |->  if ( n  =  N ,  1 ,  ( n  + 
1 ) ) ) ) " ( ( y  +  1 ) ... N ) )  X.  { 0 } ) ) ) ) ) ) )
74 oveq2 6313 . . . . . . . . . . 11  |-  ( 1  =  if ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  1
) ,  1 ,  0 )  ->  (
( ( 1st `  ( 1st `  T ) ) `
 n )  +  1 )  =  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) )
7574eleq1d 2491 . . . . . . . . . 10  |-  ( 1  =  if ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  1
) ,  1 ,  0 )  ->  (
( ( ( 1st `  ( 1st `  T
) ) `  n
)  +  1 )  e.  ( 0..^ K )  <->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) )  e.  ( 0..^ K ) ) )
76 oveq2 6313 . . . . . . . . . . 11  |-  ( 0  =  if ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  1
) ,  1 ,  0 )  ->  (
( ( 1st `  ( 1st `  T ) ) `
 n )  +  0 )  =  ( ( ( 1st `  ( 1st `  T ) ) `
 n )  +  if ( n  =  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) ) )
7776eleq1d 2491 . . . . . . . . . 10  |-  ( 0  =  if ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  1
) ,  1 ,  0 )  ->  (
( ( ( 1st `  ( 1st `  T
) ) `  n
)  +  0 )  e.  ( 0..^ K )  <->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  if ( n  =  (
( 2nd `  ( 1st `  T ) ) `
 1 ) ,  1 ,  0 ) )  e.  ( 0..^ K ) ) )
78 fveq2 5881 . . . . . . . . . . . . . 14  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  1
)  ->  ( ( 1st `  ( 1st `  T
) ) `  n
)  =  ( ( 1st `  ( 1st `  T ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ) )
7978oveq1d 6320 . . . . . . . . . . . . 13  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  1
)  ->  ( (
( 1st `  ( 1st `  T ) ) `
 n )  +  1 )  =  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  +  1 ) )
8079adantl 467 . . . . . . . . . . . 12  |-  ( (
ph  /\  n  =  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) )  ->  ( ( ( 1st `  ( 1st `  T ) ) `  n )  +  1 )  =  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  +  1 ) )
81 elrabi 3225 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 ) ) )
8281, 2eleq2s 2527 . . . . . . . . . . . . . . . . . 18  |-  ( T  e.  S  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) ) )
83 xp1st 6837 . . . . . . . . . . . . . . . . . 18  |-  ( 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 ) } ) )
844, 82, 833syl 18 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1st `  T
)  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )
85 xp1st 6837 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 ) ) )
86 elmapi 7504 . . . . . . . . . . . . . . . . 17  |-  ( ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) )  ->  ( 1st `  ( 1st `  T ) ) : ( 1 ... N ) --> ( 0..^ K ) )
8784, 85, 863syl 18 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1st `  ( 1st `  T ) ) : ( 1 ... N ) --> ( 0..^ K ) )
884, 82syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )
89 xp2nd 6838 . . . . . . . . . . . . . . . . . . . 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 ) } )
9088, 83, 893syl 18 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
91 f1oeq1 5822 . . . . . . . . . . . . . . . . . . . 20  |-  ( f  =  ( 2nd `  ( 1st `  T ) )  ->  ( f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
9251, 91elab 3217 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2nd `  ( 1st `  T ) )  e. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) }  <->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
9390, 92sylib 199 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
94 f1of 5831 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) --> ( 1 ... N
) )
9593, 94syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) --> ( 1 ... N ) )
96 nnuz 11201 . . . . . . . . . . . . . . . . . . 19  |-  NN  =  ( ZZ>= `  1 )
971, 96syl6eleq 2517 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
98 eluzfz1 11813 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... N
) )
9997, 98syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  1  e.  ( 1 ... N ) )
10095, 99ffvelrnd 6038 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) ) `
 1 )  e.  ( 1 ... N
) )
10187, 100ffvelrnd 6038 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  e.  ( 0..^ K ) )
102 elfzonn0 11967 . . . . . . . . . . . . . . 15  |-  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  e.  ( 0..^ K )  -> 
( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  e.  NN0 )
103 peano2nn0 10917 . . . . . . . . . . . . . . 15  |-  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  e.  NN0  ->  ( ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 1 ) )  +  1 )  e. 
NN0 )
104101, 102, 1033syl 18 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 1 ) )  +  1 )  e. 
NN0 )
105 elfzo0 11963 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  e.  ( 0..^ K )  <->  ( (
( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  e.  NN0  /\  K  e.  NN  /\  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  <  K
) )
106101, 105sylib 199 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 1 ) )  e.  NN0  /\  K  e.  NN  /\  ( ( 1st `  ( 1st `  T ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) )  <  K ) )
107106simp2d 1018 . . . . . . . . . . . . . 14  |-  ( ph  ->  K  e.  NN )
108 elfzolt2 11936 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  e.  ( 0..^ K )  -> 
( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  <  K
)
109101, 108syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  <  K
)
110101, 102syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  e.  NN0 )
111110nn0zd 11045 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  e.  ZZ )
112107nnzd 11046 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  K  e.  ZZ )
113 zltp1le 10993 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  e.  ZZ  /\  K  e.  ZZ )  ->  ( ( ( 1st `  ( 1st `  T ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) )  <  K  <->  ( (
( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  +  1 )  <_  K )
)
114111, 112, 113syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 1 ) )  <  K  <->  ( (
( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  +  1 )  <_  K )
)
115109, 114mpbid 213 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 1st `  ( 1st `  T
) ) `  (
( 2nd `  ( 1st `  T ) ) `
 1 ) )  +  1 )  <_  K )
116 fvex 5891 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  ( 1st `  T ) ) ` 
1 )  e.  _V
117 eleq1 2495 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  1
)  ->  ( n  e.  ( 1 ... N
)  <->  ( ( 2nd `  ( 1st `  T
) ) `  1
)  e.  ( 1 ... N ) ) )
118117anbi2d 708 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  1
)  ->  ( ( ph  /\  n  e.  ( 1 ... N ) )  <->  ( ph  /\  ( ( 2nd `  ( 1st `  T ) ) `
 1 )  e.  ( 1 ... N
) ) ) )
119 fveq2 5881 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  1
)  ->  ( p `  n )  =  ( p `  ( ( 2nd `  ( 1st `  T ) ) ` 
1 ) ) )
120119neeq1d 2697 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  1
)  ->  ( (
p `  n )  =/=  K  <->  ( p `  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) )  =/=  K ) )
121120rexbidv 2936 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  1
)  ->  ( E. p  e.  ran  F ( p `  n )  =/=  K  <->  E. p  e.  ran  F ( p `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  =/=  K
) )
122118, 121imbi12d 321 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  ( ( 2nd `  ( 1st `  T
) ) `  1
)  ->  ( (
( ph  /\  n  e.  ( 1 ... N
) )  ->  E. p  e.  ran  F ( p `
 n )  =/= 
K )  <->  ( ( ph  /\  ( ( 2nd `  ( 1st `  T
) ) `  1
)  e.  ( 1 ... N ) )  ->  E. p  e.  ran  F ( p `  (
( 2nd `  ( 1st `  T ) ) `
 1 ) )  =/=  K ) ) )
123116, 122, 5vtocl 3133 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( ( 2nd `  ( 1st `  T
) ) `  1
)  e.  ( 1 ... N ) )  ->  E. p  e.  ran  F ( p `  (
( 2nd `  ( 1st `  T ) ) `
 1 ) )  =/=  K )
124100, 123mpdan 672 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  E. p  e.  ran  F ( p `  (
( 2nd `  ( 1st `  T ) ) `
 1 ) )  =/=  K )
125 fveq1 5880 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( p  =  ( ( 1st `  ( 1st `  T
) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( ( y  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) )  ->  ( p `  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) )  =  ( ( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( ( y  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) ) `  ( ( 2nd `  ( 1st `  T ) ) ` 
1 ) ) )
126100adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  ( 1st `  T ) ) `
 1 )  e.  ( 1 ... N
) )
127 ffn 5746 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( 1st `  ( 1st `  T ) ) : ( 1 ... N
) --> ( 0..^ K )  ->  ( 1st `  ( 1st `  T
) )  Fn  (
1 ... N ) )
12887, 127syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( 1st `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
129128adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( 1st `  ( 1st `  T
) )  Fn  (
1 ... N ) )
130 1ex 9645 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  1  e.  _V
131 fnconstg 5788 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 1  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) ) )
132130, 131ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )
133 c0ex 9644 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  e.  _V
134 fnconstg 5788 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( 0  e.  _V  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( ( y  +  1 )  +  1 ) ... N ) ) )
135133, 134ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( ( y  +  1 )  +  1 ) ... N ) )
136132, 135pm3.2i 456 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  X. 
{ 1 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )  /\  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( ( y  +  1 )  +  1 ) ... N
) )  X.  {
0 } )  Fn  ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) ) )
137 dff1o3 5837 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( ( 2nd `  ( 1st `  T
) ) : ( 1 ... N )
-onto-> ( 1 ... N
)  /\  Fun  `' ( 2nd `  ( 1st `  T ) ) ) )
138137simprbi 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  Fun  `' ( 2nd `  ( 1st `  T ) ) )
13993, 138syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  Fun  `' ( 2nd `  ( 1st `  T
) ) )
140 imain 5677 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( Fun  `' ( 2nd `  ( 1st `  T ) )  ->  ( ( 2nd `  ( 1st `  T
) ) " (
( 1 ... (
y  +  1 ) )  i^i  ( ( ( y  +  1 )  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  i^i  ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) ) ) )
141139, 140syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( y  +  1 ) )  i^i  ( ( ( y  +  1 )  +  1 ) ... N
) ) )  =  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " (
( ( y  +  1 )  +  1 ) ... N ) ) ) )
142 nn0p1nn 10916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  NN0  ->  ( y  +  1 )  e.  NN )
1438, 142syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
y  +  1 )  e.  NN )
144143nnred 10631 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
y  +  1 )  e.  RR )
145144ltp1d 10544 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
y  +  1 )  <  ( ( y  +  1 )  +  1 ) )
146 fzdisj 11833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( y  +  1 )  <  ( ( y  +  1 )  +  1 )  ->  (
( 1 ... (
y  +  1 ) )  i^i  ( ( ( y  +  1 )  +  1 ) ... N ) )  =  (/) )
147146imaeq2d 5187 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( y  +  1 )  <  ( ( y  +  1 )  +  1 )  ->  (
( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( y  +  1 ) )  i^i  ( ( ( y  +  1 )  +  1 ) ... N
) ) )  =  ( ( 2nd `  ( 1st `  T ) )
" (/) ) )
148 ima0 5202 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 2nd `  ( 1st `  T ) ) " (/) )  =  (/)
149147, 148syl6eq 2479 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( y  +  1 )  <  ( ( y  +  1 )  +  1 )  ->  (
( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( y  +  1 ) )  i^i  ( ( ( y  +  1 )  +  1 ) ... N
) ) )  =  (/) )
150145, 149syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( y  +  1 ) )  i^i  ( ( ( y  +  1 )  +  1 ) ... N
) ) )  =  (/) )
151141, 150sylan9req 2484 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  i^i  ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) ) )  =  (/) )
152 fnun 5700 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... (
y  +  1 ) ) )  X.  {
1 } )  Fn  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  /\  ( ( ( 2nd `  ( 1st `  T
) ) " (
( ( y  +  1 )  +  1 ) ... N ) )  X.  { 0 } )  Fn  (
( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) ) )  /\  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... (
y  +  1 ) ) )  i^i  (
( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) ) )  =  (/) )  ->  (
( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) ) ) )
153136, 151, 152sylancr 667 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) ) ) )
154 imaundi 5267 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 2nd `  ( 1st `  T ) ) "
( ( 1 ... ( y  +  1 ) )  u.  (
( ( y  +  1 )  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) ) )
155143peano2nnd 10633 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
( y  +  1 )  +  1 )  e.  NN )
156155, 96syl6eleq 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
( y  +  1 )  +  1 )  e.  ( ZZ>= `  1
) )
157156adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( y  +  1 )  +  1 )  e.  ( ZZ>= `  1
) )
1581nncnd 10632 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ph  ->  N  e.  CC )
159 npcan1 10051 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
160158, 159syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
161160adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  =  N )
162 elfzuz3 11804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  ( N  -  1 )  e.  ( ZZ>= `  y
) )
163 eluzp1p1 11191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( N  -  1 )  e.  ( ZZ>= `  y
)  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  ( y  +  1 ) ) )
164162, 163syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
( N  -  1 )  +  1 )  e.  ( ZZ>= `  (
y  +  1 ) ) )
165164adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  e.  ( ZZ>= `  (
y  +  1 ) ) )
166161, 165eqeltrrd 2508 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  ( y  +  1 ) ) )
167 fzsplit2 11831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( y  +  1 )  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ( ZZ>= `  ( y  +  1 ) ) )  ->  ( 1 ... N )  =  ( ( 1 ... ( y  +  1 ) )  u.  (
( ( y  +  1 )  +  1 ) ... N ) ) )
168157, 166, 167syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
1 ... N )  =  ( ( 1 ... ( y  +  1 ) )  u.  (
( ( y  +  1 )  +  1 ) ... N ) ) )
169168imaeq2d 5187 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( y  +  1 ) )  u.  ( ( ( y  +  1 )  +  1 ) ... N
) ) ) )
170 f1ofo 5838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N )
-onto-> ( 1 ... N
) )
171 foima 5815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
) -onto-> ( 1 ... N )  ->  (
( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
17293, 170, 1713syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
173172adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  ( 1st `  T ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
174169, 173eqtr3d 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  ( 1st `  T ) )
" ( ( 1 ... ( y  +  1 ) )  u.  ( ( ( y  +  1 )  +  1 ) ... N
) ) )  =  ( 1 ... N
) )
175154, 174syl5eqr 2477 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  u.  ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
176175fneq2d 5685 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... (
y  +  1 ) ) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( ( y  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) )  Fn  ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )  u.  ( ( 2nd `  ( 1st `  T
) ) " (
( ( y  +  1 )  +  1 ) ... N ) ) )  <->  ( (
( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( ( y  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) )  Fn  ( 1 ... N ) ) )
177153, 176mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) )  Fn  ( 1 ... N ) )
17849a1i 11 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
1 ... N )  e. 
_V )
179 inidm 3671 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
180 eqidd 2423 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  (
( 2nd `  ( 1st `  T ) ) `
 1 )  e.  ( 1 ... N
) )  ->  (
( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  =  ( ( 1st `  ( 1st `  T ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) ) )
181 f1ofn 5832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  T
) )  Fn  (
1 ... N ) )
18293, 181syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) )  Fn  ( 1 ... N ) )
183182adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( 2nd `  ( 1st `  T
) )  Fn  (
1 ... N ) )
184 fzss2 11845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( N  e.  ( ZZ>= `  (
y  +  1 ) )  ->  ( 1 ... ( y  +  1 ) )  C_  ( 1 ... N
) )
185166, 184syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
1 ... ( y  +  1 ) )  C_  ( 1 ... N
) )
186143, 96syl6eleq 2517 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
y  +  1 )  e.  ( ZZ>= `  1
) )
187 eluzfz1 11813 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( y  +  1 )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... (
y  +  1 ) ) )
188186, 187syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  1  e.  ( 1 ... (
y  +  1 ) ) )
189188adantl 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  1  e.  ( 1 ... (
y  +  1 ) ) )
190 fnfvima 6158 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( 2nd `  ( 1st `  T ) )  Fn  ( 1 ... N )  /\  (
1 ... ( y  +  1 ) )  C_  ( 1 ... N
)  /\  1  e.  ( 1 ... (
y  +  1 ) ) )  ->  (
( 2nd `  ( 1st `  T ) ) `
 1 )  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) ) )
191183, 185, 189, 190syl3anc 1264 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  ( 1st `  T ) ) `
 1 )  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) ) )
192 fvun1 5952 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )  X.  { 1 } )  Fn  ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... (
y  +  1 ) ) )  /\  (
( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } )  Fn  ( ( 2nd `  ( 1st `  T
) ) " (
( ( y  +  1 )  +  1 ) ... N ) )  /\  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  i^i  ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) ) )  =  (/)  /\  (
( 2nd `  ( 1st `  T ) ) `
 1 )  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) ) ) )  ->  ( (
( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) ) `  ( ( 2nd `  ( 1st `  T ) ) ` 
1 ) )  =  ( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... (
y  +  1 ) ) )  X.  {
1 } ) `  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) ) )
193132, 135, 192mp3an12 1350 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )  i^i  ( ( 2nd `  ( 1st `  T
) ) " (
( ( y  +  1 )  +  1 ) ... N ) ) )  =  (/)  /\  ( ( 2nd `  ( 1st `  T ) ) `
 1 )  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) ) )  ->  ( ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( ( y  +  1 )  +  1 ) ... N
) )  X.  {
0 } ) ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) )  =  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )  X.  { 1 } ) `  ( ( 2nd `  ( 1st `  T ) ) ` 
1 ) ) )
194151, 191, 193syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... (
y  +  1 ) ) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( ( y  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) )  =  ( ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  X. 
{ 1 } ) `
 ( ( 2nd `  ( 1st `  T
) ) `  1
) ) )
195130fvconst2 6135 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 2nd `  ( 1st `  T ) ) `
 1 )  e.  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... ( y  +  1 ) ) )  -> 
( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... (
y  +  1 ) ) )  X.  {
1 } ) `  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) )  =  1 )
196191, 195syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )  X.  { 1 } ) `  ( ( 2nd `  ( 1st `  T ) ) ` 
1 ) )  =  1 )
197194, 196eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... (
y  +  1 ) ) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( ( y  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) )  =  1 )
198197adantr 466 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  (
( 2nd `  ( 1st `  T ) ) `
 1 )  e.  ( 1 ... N
) )  ->  (
( ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... (
y  +  1 ) ) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  T
) ) " (
( ( y  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) )  =  1 )
199129, 177, 178, 178, 179, 180, 198ofval 6554 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  (
( 2nd `  ( 1st `  T ) ) `
 1 )  e.  ( 1 ... N
) )  ->  (
( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  (
( 2nd `  ( 1st `  T ) ) `
 1 ) )  =  ( ( ( 1st `  ( 1st `  T ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) )  +  1 ) )
200126, 199mpdan 672 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( 1st `  ( 1st `  T ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  T
) ) " (
1 ... ( y  +  1 ) ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  T ) )
" ( ( ( y  +  1 )  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) `  (
( 2nd `  ( 1st `  T ) ) `
 1 ) )  =  ( ( ( 1st `  ( 1st `  T ) ) `  ( ( 2nd `  ( 1st `  T ) ) `
 1 ) )  +  1 ) )
201125, 200sylan9eqr 2485 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  p  =  ( ( 1st