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

Theorem poimirlem22 32026
Description: Lemma for poimir 32037, that a given face belongs to exactly two simplices, provided it's not on the boundary of the cube. (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 )
poimirlem22.4  |-  ( (
ph  /\  n  e.  ( 1 ... N
) )  ->  E. p  e.  ran  F ( p `
 n )  =/= 
K )
Assertion
Ref Expression
poimirlem22  |-  ( 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 poimirlem22
StepHypRef Expression
1 poimir.0 . . . . 5  |-  ( ph  ->  N  e.  NN )
21adantr 472 . . . 4  |-  ( (
ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  N  e.  NN )
3 poimirlem22.s . . . 4  |-  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 } ) ) ) ) }
4 poimirlem22.1 . . . . 5  |-  ( ph  ->  F : ( 0 ... ( N  - 
1 ) ) --> ( ( 0 ... K
)  ^m  ( 1 ... N ) ) )
54adantr 472 . . . 4  |-  ( (
ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  F :
( 0 ... ( N  -  1 ) ) --> ( ( 0 ... K )  ^m  ( 1 ... N
) ) )
6 poimirlem22.2 . . . . 5  |-  ( ph  ->  T  e.  S )
76adantr 472 . . . 4  |-  ( (
ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  T  e.  S )
8 simpr 468 . . . 4  |-  ( (
ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )
92, 3, 5, 7, 8poimirlem15 32019 . . 3  |-  ( (
ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  <. <. ( 1st `  ( 1st `  T
) ) ,  ( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) )
>. ,  ( 2nd `  T ) >.  e.  S
)
10 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  T  ->  ( 2nd `  t )  =  ( 2nd `  T
) )
1110breq2d 4407 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  =  T  ->  (
y  <  ( 2nd `  t )  <->  y  <  ( 2nd `  T ) ) )
1211ifbid 3894 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  T  ->  if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  =  if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) ) )
1312csbeq1d 3356 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 } ) ) ) )
14 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  T  ->  ( 1st `  t )  =  ( 1st `  T
) )
1514fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  =  T  ->  ( 1st `  ( 1st `  t
) )  =  ( 1st `  ( 1st `  T ) ) )
1614fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  T  ->  ( 2nd `  ( 1st `  t
) )  =  ( 2nd `  ( 1st `  T ) ) )
1716imaeq1d 5173 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) ) )
1817xpeq1d 4862 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... j
) )  X.  {
1 } ) )
1916imaeq1d 5173 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) ) )
2019xpeq1d 4862 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )
2118, 20uneq12d 3580 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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 } ) ) )
2215, 21oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 } ) ) ) )
2322csbeq2dv 3785 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 } ) ) ) )
2413, 23eqtrd 2505 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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 } ) ) ) )
2524mpteq2dv 4483 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 } ) ) ) ) )
2625eqeq2d 2481 . . . . . . . . . . . . . . . . . 18  |-  ( 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 } ) ) ) ) ) )
2726, 3elrab2 3186 . . . . . . . . . . . . . . . . 17  |-  ( 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 } ) ) ) ) ) )
2827simprbi 471 . . . . . . . . . . . . . . . 16  |-  ( 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 } ) ) ) ) )
296, 28syl 17 . . . . . . . . . . . . . . 15  |-  ( 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 } ) ) ) ) )
3029adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  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 } ) ) ) ) )
31 elrabi 3181 . . . . . . . . . . . . . . . . . . . . 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 ) ) )
3231, 3eleq2s 2567 . . . . . . . . . . . . . . . . . . . 20  |-  ( T  e.  S  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) ) )
336, 32syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )
34 xp1st 6842 . . . . . . . . . . . . . . . . . . 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 ) } ) )
3533, 34syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1st `  T
)  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )
36 xp1st 6842 . . . . . . . . . . . . . . . . . 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 ) ) )
3735, 36syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  (
1 ... N ) ) )
38 elmapi 7511 . . . . . . . . . . . . . . . . 17  |-  ( ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) )  ->  ( 1st `  ( 1st `  T ) ) : ( 1 ... N ) --> ( 0..^ K ) )
3937, 38syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 1st `  ( 1st `  T ) ) : ( 1 ... N ) --> ( 0..^ K ) )
40 elfzoelz 11947 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  ( 0..^ K )  ->  n  e.  ZZ )
4140ssriv 3422 . . . . . . . . . . . . . . . 16  |-  ( 0..^ K )  C_  ZZ
42 fss 5749 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1st `  ( 1st `  T ) ) : ( 1 ... N ) --> ( 0..^ K )  /\  (
0..^ K )  C_  ZZ )  ->  ( 1st `  ( 1st `  T
) ) : ( 1 ... N ) --> ZZ )
4339, 41, 42sylancl 675 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 1st `  ( 1st `  T ) ) : ( 1 ... N ) --> ZZ )
4443adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  ( 1st `  ( 1st `  T
) ) : ( 1 ... N ) --> ZZ )
45 xp2nd 6843 . . . . . . . . . . . . . . . . 17  |-  ( ( 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 ) } )
4635, 45syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
47 fvex 5889 . . . . . . . . . . . . . . . . 17  |-  ( 2nd `  ( 1st `  T
) )  e.  _V
48 f1oeq1 5818 . . . . . . . . . . . . . . . . 17  |-  ( f  =  ( 2nd `  ( 1st `  T ) )  ->  ( f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
4947, 48elab 3173 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  ( 1st `  T ) )  e. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) }  <->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
5046, 49sylib 201 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
5150adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
522, 30, 44, 51, 8poimirlem1 32005 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  -.  E* n  e.  ( 1 ... N
) ( ( F `
 ( ( 2nd `  T )  -  1 ) ) `  n
)  =/=  ( ( F `  ( 2nd `  T ) ) `  n ) )
5352adantr 472 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  -.  E* n  e.  (
1 ... N ) ( ( F `  (
( 2nd `  T
)  -  1 ) ) `  n )  =/=  ( ( F `
 ( 2nd `  T
) ) `  n
) )
541ad3antrrr 744 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  ( 2nd `  z
)  =/=  ( 2nd `  T ) )  ->  N  e.  NN )
55 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  z  ->  ( 2nd `  t )  =  ( 2nd `  z
) )
5655breq2d 4407 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  =  z  ->  (
y  <  ( 2nd `  t )  <->  y  <  ( 2nd `  z ) ) )
5756ifbid 3894 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  z  ->  if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  =  if ( y  <  ( 2nd `  z
) ,  y ,  ( y  +  1 ) ) )
5857csbeq1d 3356 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  z  ->  [_ 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 `  z ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
59 fveq2 5879 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  z  ->  ( 1st `  t )  =  ( 1st `  z
) )
6059fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  =  z  ->  ( 1st `  ( 1st `  t
) )  =  ( 1st `  ( 1st `  z ) ) )
6159fveq2d 5883 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( t  =  z  ->  ( 2nd `  ( 1st `  t
) )  =  ( 2nd `  ( 1st `  z ) ) )
6261imaeq1d 5173 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  z  ->  (
( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  z ) )
" ( 1 ... j ) ) )
6362xpeq1d 4862 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  z  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  z ) ) "
( 1 ... j
) )  X.  {
1 } ) )
6461imaeq1d 5173 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( t  =  z  ->  (
( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) ) )
6564xpeq1d 4862 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  =  z  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  z ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )
6663, 65uneq12d 3580 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  =  z  ->  (
( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) )  =  ( ( ( ( 2nd `  ( 1st `  z ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )
6760, 66oveq12d 6326 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( t  =  z  ->  (
( 1st `  ( 1st `  t ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  t
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
6867csbeq2dv 3785 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  z  ->  [_ if ( y  <  ( 2nd `  z ) ,  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 `  z ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
6958, 68eqtrd 2505 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  z  ->  [_ 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 `  z ) ,  y ,  ( y  +  1 ) )  /  j ]_ (
( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
7069mpteq2dv 4483 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  z  ->  (
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 `  z
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
7170eqeq2d 2481 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  z  ->  ( 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 `  z
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) ) )
7271, 3elrab2 3186 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  S  <->  ( z  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 `  z
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) ) )
7372simprbi 471 . . . . . . . . . . . . . . . 16  |-  ( z  e.  S  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  z
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
7473ad2antlr 741 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  ( 2nd `  z
)  =/=  ( 2nd `  T ) )  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  z
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
75 elrabi 3181 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  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 } ) ) ) ) }  ->  z  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )
7675, 3eleq2s 2567 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  S  ->  z  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) ) )
77 xp1st 6842 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  ->  ( 1st `  z )  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
7876, 77syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  S  ->  ( 1st `  z )  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
79 xp1st 6842 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1st `  z )  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 1st `  ( 1st `  z ) )  e.  ( ( 0..^ K )  ^m  (
1 ... N ) ) )
8078, 79syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  S  ->  ( 1st `  ( 1st `  z
) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) ) )
81 elmapi 7511 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1st `  ( 1st `  z ) )  e.  ( ( 0..^ K )  ^m  ( 1 ... N ) )  ->  ( 1st `  ( 1st `  z ) ) : ( 1 ... N ) --> ( 0..^ K ) )
8280, 81syl 17 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  S  ->  ( 1st `  ( 1st `  z
) ) : ( 1 ... N ) --> ( 0..^ K ) )
83 fss 5749 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 1st `  ( 1st `  z ) ) : ( 1 ... N ) --> ( 0..^ K )  /\  (
0..^ K )  C_  ZZ )  ->  ( 1st `  ( 1st `  z
) ) : ( 1 ... N ) --> ZZ )
8482, 41, 83sylancl 675 . . . . . . . . . . . . . . . 16  |-  ( z  e.  S  ->  ( 1st `  ( 1st `  z
) ) : ( 1 ... N ) --> ZZ )
8584ad2antlr 741 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  ( 2nd `  z
)  =/=  ( 2nd `  T ) )  -> 
( 1st `  ( 1st `  z ) ) : ( 1 ... N ) --> ZZ )
86 xp2nd 6843 . . . . . . . . . . . . . . . . . 18  |-  ( ( 1st `  z )  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 2nd `  ( 1st `  z ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
8778, 86syl 17 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  S  ->  ( 2nd `  ( 1st `  z
) )  e.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )
88 fvex 5889 . . . . . . . . . . . . . . . . . 18  |-  ( 2nd `  ( 1st `  z
) )  e.  _V
89 f1oeq1 5818 . . . . . . . . . . . . . . . . . 18  |-  ( f  =  ( 2nd `  ( 1st `  z ) )  ->  ( f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  ( 1st `  z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
9088, 89elab 3173 . . . . . . . . . . . . . . . . 17  |-  ( ( 2nd `  ( 1st `  z ) )  e. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) }  <->  ( 2nd `  ( 1st `  z
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
9187, 90sylib 201 . . . . . . . . . . . . . . . 16  |-  ( z  e.  S  ->  ( 2nd `  ( 1st `  z
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
9291ad2antlr 741 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  ( 2nd `  z
)  =/=  ( 2nd `  T ) )  -> 
( 2nd `  ( 1st `  z ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
93 simpllr 777 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  ( 2nd `  z
)  =/=  ( 2nd `  T ) )  -> 
( 2nd `  T
)  e.  ( 1 ... ( N  - 
1 ) ) )
94 xp2nd 6843 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) )  ->  ( 2nd `  z )  e.  ( 0 ... N
) )
9576, 94syl 17 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  S  ->  ( 2nd `  z )  e.  ( 0 ... N
) )
9695adantl 473 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  ( 2nd `  z )  e.  ( 0 ... N
) )
97 eldifsn 4088 . . . . . . . . . . . . . . . . 17  |-  ( ( 2nd `  z )  e.  ( ( 0 ... N )  \  { ( 2nd `  T
) } )  <->  ( ( 2nd `  z )  e.  ( 0 ... N
)  /\  ( 2nd `  z )  =/=  ( 2nd `  T ) ) )
9897biimpri 211 . . . . . . . . . . . . . . . 16  |-  ( ( ( 2nd `  z
)  e.  ( 0 ... N )  /\  ( 2nd `  z )  =/=  ( 2nd `  T
) )  ->  ( 2nd `  z )  e.  ( ( 0 ... N )  \  {
( 2nd `  T
) } ) )
9996, 98sylan 479 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  ( 2nd `  z
)  =/=  ( 2nd `  T ) )  -> 
( 2nd `  z
)  e.  ( ( 0 ... N ) 
\  { ( 2nd `  T ) } ) )
10054, 74, 85, 92, 93, 99poimirlem2 32006 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  ( 2nd `  z
)  =/=  ( 2nd `  T ) )  ->  E* n  e.  (
1 ... N ) ( ( F `  (
( 2nd `  T
)  -  1 ) ) `  n )  =/=  ( ( F `
 ( 2nd `  T
) ) `  n
) )
101100ex 441 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  (
( 2nd `  z
)  =/=  ( 2nd `  T )  ->  E* n  e.  ( 1 ... N ) ( ( F `  (
( 2nd `  T
)  -  1 ) ) `  n )  =/=  ( ( F `
 ( 2nd `  T
) ) `  n
) ) )
102101necon1bd 2661 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  ( -.  E* n  e.  ( 1 ... N ) ( ( F `  ( ( 2nd `  T
)  -  1 ) ) `  n )  =/=  ( ( F `
 ( 2nd `  T
) ) `  n
)  ->  ( 2nd `  z )  =  ( 2nd `  T ) ) )
10353, 102mpd 15 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  ( 2nd `  z )  =  ( 2nd `  T
) )
104 eleq1 2537 . . . . . . . . . . . . . . . 16  |-  ( ( 2nd `  z )  =  ( 2nd `  T
)  ->  ( ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) )  <->  ( 2nd `  T
)  e.  ( 1 ... ( N  - 
1 ) ) ) )
105104biimparc 495 . . . . . . . . . . . . . . 15  |-  ( ( ( 2nd `  T
)  e.  ( 1 ... ( N  - 
1 ) )  /\  ( 2nd `  z )  =  ( 2nd `  T
) )  ->  ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) ) )
106105anim2i 579 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  /\  ( 2nd `  z )  =  ( 2nd `  T ) ) )  ->  ( ph  /\  ( 2nd `  z
)  e.  ( 1 ... ( N  - 
1 ) ) ) )
107106anassrs 660 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  ( 2nd `  z )  =  ( 2nd `  T
) )  ->  ( ph  /\  ( 2nd `  z
)  e.  ( 1 ... ( N  - 
1 ) ) ) )
10873adantl 473 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  F  =  ( y  e.  ( 0 ... ( N  -  1 ) )  |->  [_ if ( y  <  ( 2nd `  z
) ,  y ,  ( y  +  1 ) )  /  j ]_ ( ( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) ) )
109 breq1 4398 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  0  ->  (
y  <  ( 2nd `  z )  <->  0  <  ( 2nd `  z ) ) )
110 id 22 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  0  ->  y  =  0 )
111109, 110ifbieq1d 3895 . . . . . . . . . . . . . . . . 17  |-  ( y  =  0  ->  if ( y  <  ( 2nd `  z ) ,  y ,  ( y  +  1 ) )  =  if ( 0  <  ( 2nd `  z
) ,  0 ,  ( y  +  1 ) ) )
112 elfznn 11854 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) )  ->  ( 2nd `  z )  e.  NN )
113112nngt0d 10675 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) )  ->  0  <  ( 2nd `  z
) )
114113iftrued 3880 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) )  ->  if ( 0  <  ( 2nd `  z ) ,  0 ,  ( y  +  1 ) )  =  0 )
115114ad2antlr 741 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  if ( 0  <  ( 2nd `  z ) ,  0 ,  ( y  +  1 ) )  =  0 )
116111, 115sylan9eqr 2527 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  y  =  0
)  ->  if (
y  <  ( 2nd `  z ) ,  y ,  ( y  +  1 ) )  =  0 )
117116csbeq1d 3356 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  y  =  0
)  ->  [_ if ( y  <  ( 2nd `  z ) ,  y ,  ( y  +  1 ) )  / 
j ]_ ( ( 1st `  ( 1st `  z
) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  =  [_ 0  /  j ]_ (
( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
118 c0ex 9655 . . . . . . . . . . . . . . . . . 18  |-  0  e.  _V
119 oveq2 6316 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  0  ->  (
1 ... j )  =  ( 1 ... 0
) )
120 fz10 11846 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1 ... 0 )  =  (/)
121119, 120syl6eq 2521 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  0  ->  (
1 ... j )  =  (/) )
122121imaeq2d 5174 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  0  ->  (
( 2nd `  ( 1st `  z ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  z ) )
" (/) ) )
123122xpeq1d 4862 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  0  ->  (
( ( 2nd `  ( 1st `  z ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  z ) ) " (/) )  X.  { 1 } ) )
124 oveq1 6315 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  0  ->  (
j  +  1 )  =  ( 0  +  1 ) )
125 0p1e1 10743 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( 0  +  1 )  =  1
126124, 125syl6eq 2521 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  0  ->  (
j  +  1 )  =  1 )
127126oveq1d 6323 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  0  ->  (
( j  +  1 ) ... N )  =  ( 1 ... N ) )
128127imaeq2d 5174 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  0  ->  (
( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  z ) )
" ( 1 ... N ) ) )
129128xpeq1d 4862 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  0  ->  (
( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  z ) ) "
( 1 ... N
) )  X.  {
0 } ) )
130123, 129uneq12d 3580 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  0  ->  (
( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) )  =  ( ( ( ( 2nd `  ( 1st `  z ) )
" (/) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... N ) )  X.  { 0 } ) ) )
131 ima0 5189 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( 2nd `  ( 1st `  z ) ) " (/) )  =  (/)
132131xpeq1i 4859 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 2nd `  ( 1st `  z ) )
" (/) )  X.  {
1 } )  =  ( (/)  X.  { 1 } )
133 0xp 4920 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (/)  X. 
{ 1 } )  =  (/)
134132, 133eqtri 2493 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 2nd `  ( 1st `  z ) )
" (/) )  X.  {
1 } )  =  (/)
135134uneq1i 3575 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 2nd `  ( 1st `  z ) )
" (/) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... N ) )  X.  { 0 } ) )  =  (
(/)  u.  ( (
( 2nd `  ( 1st `  z ) )
" ( 1 ... N ) )  X. 
{ 0 } ) )
136 uncom 3569 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (/)  u.  ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... N ) )  X.  { 0 } ) )  =  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... N ) )  X.  { 0 } )  u.  (/) )
137 un0 3762 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 2nd `  ( 1st `  z ) )
" ( 1 ... N ) )  X. 
{ 0 } )  u.  (/) )  =  ( ( ( 2nd `  ( 1st `  z ) )
" ( 1 ... N ) )  X. 
{ 0 } )
138135, 136, 1373eqtri 2497 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 2nd `  ( 1st `  z ) )
" (/) )  X.  {
1 } )  u.  ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... N ) )  X.  { 0 } ) )  =  ( ( ( 2nd `  ( 1st `  z ) )
" ( 1 ... N ) )  X. 
{ 0 } )
139130, 138syl6eq 2521 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  0  ->  (
( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) )  =  ( ( ( 2nd `  ( 1st `  z ) )
" ( 1 ... N ) )  X. 
{ 0 } ) )
140139oveq2d 6324 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  0  ->  (
( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  z ) )  oF  +  ( ( ( 2nd `  ( 1st `  z ) )
" ( 1 ... N ) )  X. 
{ 0 } ) ) )
141118, 140csbie 3375 . . . . . . . . . . . . . . . . 17  |-  [_ 0  /  j ]_ (
( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  ( 1st `  z ) )  oF  +  ( ( ( 2nd `  ( 1st `  z ) )
" ( 1 ... N ) )  X. 
{ 0 } ) )
142 f1ofo 5835 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2nd `  ( 1st `  z ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  ( 1st `  z
) ) : ( 1 ... N )
-onto-> ( 1 ... N
) )
14391, 142syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  S  ->  ( 2nd `  ( 1st `  z
) ) : ( 1 ... N )
-onto-> ( 1 ... N
) )
144 foima 5811 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2nd `  ( 1st `  z ) ) : ( 1 ... N
) -onto-> ( 1 ... N )  ->  (
( 2nd `  ( 1st `  z ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
145143, 144syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  S  ->  (
( 2nd `  ( 1st `  z ) )
" ( 1 ... N ) )  =  ( 1 ... N
) )
146145xpeq1d 4862 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  S  ->  (
( ( 2nd `  ( 1st `  z ) )
" ( 1 ... N ) )  X. 
{ 0 } )  =  ( ( 1 ... N )  X. 
{ 0 } ) )
147146oveq2d 6324 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  S  ->  (
( 1st `  ( 1st `  z ) )  oF  +  ( ( ( 2nd `  ( 1st `  z ) )
" ( 1 ... N ) )  X. 
{ 0 } ) )  =  ( ( 1st `  ( 1st `  z ) )  oF  +  ( ( 1 ... N )  X.  { 0 } ) ) )
148 ovex 6336 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1 ... N )  e. 
_V
149148a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  S  ->  (
1 ... N )  e. 
_V )
150 ffn 5739 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 1st `  ( 1st `  z ) ) : ( 1 ... N
) --> ( 0..^ K )  ->  ( 1st `  ( 1st `  z
) )  Fn  (
1 ... N ) )
15182, 150syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  S  ->  ( 1st `  ( 1st `  z
) )  Fn  (
1 ... N ) )
152 fnconstg 5784 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  _V  ->  (
( 1 ... N
)  X.  { 0 } )  Fn  (
1 ... N ) )
153118, 152mp1i 13 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  S  ->  (
( 1 ... N
)  X.  { 0 } )  Fn  (
1 ... N ) )
154 eqidd 2472 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  e.  S  /\  n  e.  ( 1 ... N ) )  ->  ( ( 1st `  ( 1st `  z
) ) `  n
)  =  ( ( 1st `  ( 1st `  z ) ) `  n ) )
155118fvconst2 6136 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
0 } ) `  n )  =  0 )
156155adantl 473 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  e.  S  /\  n  e.  ( 1 ... N ) )  ->  ( ( ( 1 ... N )  X.  { 0 } ) `  n )  =  0 )
15782ffvelrnda 6037 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( z  e.  S  /\  n  e.  ( 1 ... N ) )  ->  ( ( 1st `  ( 1st `  z
) ) `  n
)  e.  ( 0..^ K ) )
158 elfzonn0 11988 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 1st `  ( 1st `  z ) ) `
 n )  e.  ( 0..^ K )  ->  ( ( 1st `  ( 1st `  z
) ) `  n
)  e.  NN0 )
159157, 158syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( z  e.  S  /\  n  e.  ( 1 ... N ) )  ->  ( ( 1st `  ( 1st `  z
) ) `  n
)  e.  NN0 )
160159nn0cnd 10951 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  S  /\  n  e.  ( 1 ... N ) )  ->  ( ( 1st `  ( 1st `  z
) ) `  n
)  e.  CC )
161160addid1d 9851 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  e.  S  /\  n  e.  ( 1 ... N ) )  ->  ( ( ( 1st `  ( 1st `  z ) ) `  n )  +  0 )  =  ( ( 1st `  ( 1st `  z ) ) `  n ) )
162149, 151, 153, 151, 154, 156, 161offveq 6571 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  S  ->  (
( 1st `  ( 1st `  z ) )  oF  +  ( ( 1 ... N
)  X.  { 0 } ) )  =  ( 1st `  ( 1st `  z ) ) )
163147, 162eqtrd 2505 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  S  ->  (
( 1st `  ( 1st `  z ) )  oF  +  ( ( ( 2nd `  ( 1st `  z ) )
" ( 1 ... N ) )  X. 
{ 0 } ) )  =  ( 1st `  ( 1st `  z
) ) )
164141, 163syl5eq 2517 . . . . . . . . . . . . . . . 16  |-  ( z  e.  S  ->  [_ 0  /  j ]_ (
( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( 1st `  ( 1st `  z ) ) )
165164ad2antlr 741 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  y  =  0
)  ->  [_ 0  /  j ]_ (
( 1st `  ( 1st `  z ) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z
) ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  =  ( 1st `  ( 1st `  z ) ) )
166117, 165eqtrd 2505 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  y  =  0
)  ->  [_ if ( y  <  ( 2nd `  z ) ,  y ,  ( y  +  1 ) )  / 
j ]_ ( ( 1st `  ( 1st `  z
) )  oF  +  ( ( ( ( 2nd `  ( 1st `  z ) )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  ( 1st `  z ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) ) )  =  ( 1st `  ( 1st `  z
) ) )
167 nnm1nn0 10935 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  NN0 )
1681, 167syl 17 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  -  1 )  e.  NN0 )
169 0elfz 11915 . . . . . . . . . . . . . . . 16  |-  ( ( N  -  1 )  e.  NN0  ->  0  e.  ( 0 ... ( N  -  1 ) ) )
170168, 169syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  e.  ( 0 ... ( N  - 
1 ) ) )
171170ad2antrr 740 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  0  e.  ( 0 ... ( N  -  1 ) ) )
172 fvex 5889 . . . . . . . . . . . . . . 15  |-  ( 1st `  ( 1st `  z
) )  e.  _V
173172a1i 11 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  ( 1st `  ( 1st `  z
) )  e.  _V )
174108, 166, 171, 173fvmptd 5969 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  ( F `  0 )  =  ( 1st `  ( 1st `  z ) ) )
175107, 174sylan 479 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  ( 2nd `  z )  =  ( 2nd `  T
) )  /\  z  e.  S )  ->  ( F `  0 )  =  ( 1st `  ( 1st `  z ) ) )
176175an32s 821 . . . . . . . . . . 11  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  ( 2nd `  z
)  =  ( 2nd `  T ) )  -> 
( F `  0
)  =  ( 1st `  ( 1st `  z
) ) )
177103, 176mpdan 681 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  ( F `  0 )  =  ( 1st `  ( 1st `  z ) ) )
178 fveq2 5879 . . . . . . . . . . . . . . . 16  |-  ( z  =  T  ->  ( 2nd `  z )  =  ( 2nd `  T
) )
179178eleq1d 2533 . . . . . . . . . . . . . . 15  |-  ( z  =  T  ->  (
( 2nd `  z
)  e.  ( 1 ... ( N  - 
1 ) )  <->  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) ) )
180179anbi2d 718 . . . . . . . . . . . . . 14  |-  ( z  =  T  ->  (
( ph  /\  ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) ) )  <->  ( ph  /\  ( 2nd `  T
)  e.  ( 1 ... ( N  - 
1 ) ) ) ) )
181 fveq2 5879 . . . . . . . . . . . . . . . 16  |-  ( z  =  T  ->  ( 1st `  z )  =  ( 1st `  T
) )
182181fveq2d 5883 . . . . . . . . . . . . . . 15  |-  ( z  =  T  ->  ( 1st `  ( 1st `  z
) )  =  ( 1st `  ( 1st `  T ) ) )
183182eqeq2d 2481 . . . . . . . . . . . . . 14  |-  ( z  =  T  ->  (
( F `  0
)  =  ( 1st `  ( 1st `  z
) )  <->  ( F `  0 )  =  ( 1st `  ( 1st `  T ) ) ) )
184180, 183imbi12d 327 . . . . . . . . . . . . 13  |-  ( z  =  T  ->  (
( ( ph  /\  ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) ) )  -> 
( F `  0
)  =  ( 1st `  ( 1st `  z
) ) )  <->  ( ( ph  /\  ( 2nd `  T
)  e.  ( 1 ... ( N  - 
1 ) ) )  ->  ( F ` 
0 )  =  ( 1st `  ( 1st `  T ) ) ) ) )
185174expcom 442 . . . . . . . . . . . . 13  |-  ( z  e.  S  ->  (
( ph  /\  ( 2nd `  z )  e.  ( 1 ... ( N  -  1 ) ) )  ->  ( F `  0 )  =  ( 1st `  ( 1st `  z ) ) ) )
186184, 185vtoclga 3099 . . . . . . . . . . . 12  |-  ( T  e.  S  ->  (
( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  ( F `  0 )  =  ( 1st `  ( 1st `  T ) ) ) )
1877, 186mpcom 36 . . . . . . . . . . 11  |-  ( (
ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  ( F `  0 )  =  ( 1st `  ( 1st `  T ) ) )
188187adantr 472 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  ( F `  0 )  =  ( 1st `  ( 1st `  T ) ) )
189177, 188eqtr3d 2507 . . . . . . . . 9  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  ( 1st `  ( 1st `  z
) )  =  ( 1st `  ( 1st `  T ) ) )
190189adantr 472 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  z  =/=  T
)  ->  ( 1st `  ( 1st `  z
) )  =  ( 1st `  ( 1st `  T ) ) )
1911ad3antrrr 744 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  z  =/=  T
)  ->  N  e.  NN )
1926ad3antrrr 744 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  z  =/=  T
)  ->  T  e.  S )
193 simpllr 777 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  z  =/=  T
)  ->  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )
194 simplr 770 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  z  =/=  T
)  ->  z  e.  S )
19535adantr 472 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  ( 1st `  T )  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
196 xpopth 6851 . . . . . . . . . . . . . 14  |-  ( ( ( 1st `  z
)  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  /\  ( 1st `  T )  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } ) )  ->  ( ( ( 1st `  ( 1st `  z ) )  =  ( 1st `  ( 1st `  T ) )  /\  ( 2nd `  ( 1st `  z ) )  =  ( 2nd `  ( 1st `  T ) ) )  <->  ( 1st `  z
)  =  ( 1st `  T ) ) )
19778, 195, 196syl2anr 486 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  (
( ( 1st `  ( 1st `  z ) )  =  ( 1st `  ( 1st `  T ) )  /\  ( 2nd `  ( 1st `  z ) )  =  ( 2nd `  ( 1st `  T ) ) )  <->  ( 1st `  z
)  =  ( 1st `  T ) ) )
19833adantr 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) ) )
199 xpopth 6851 . . . . . . . . . . . . . . . 16  |-  ( ( z  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  /\  T  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )  ->  ( (
( 1st `  z
)  =  ( 1st `  T )  /\  ( 2nd `  z )  =  ( 2nd `  T
) )  <->  z  =  T ) )
200199biimpd 212 . . . . . . . . . . . . . . 15  |-  ( ( z  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) )  /\  T  e.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )  ->  ( (
( 1st `  z
)  =  ( 1st `  T )  /\  ( 2nd `  z )  =  ( 2nd `  T
) )  ->  z  =  T ) )
20176, 198, 200syl2anr 486 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  (
( ( 1st `  z
)  =  ( 1st `  T )  /\  ( 2nd `  z )  =  ( 2nd `  T
) )  ->  z  =  T ) )
202103, 201mpan2d 688 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  (
( 1st `  z
)  =  ( 1st `  T )  ->  z  =  T ) )
203197, 202sylbid 223 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  (
( ( 1st `  ( 1st `  z ) )  =  ( 1st `  ( 1st `  T ) )  /\  ( 2nd `  ( 1st `  z ) )  =  ( 2nd `  ( 1st `  T ) ) )  ->  z  =  T ) )
204189, 203mpand 689 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  (
( 2nd `  ( 1st `  z ) )  =  ( 2nd `  ( 1st `  T ) )  ->  z  =  T ) )
205204necon3d 2664 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  (
z  =/=  T  -> 
( 2nd `  ( 1st `  z ) )  =/=  ( 2nd `  ( 1st `  T ) ) ) )
206205imp 436 . . . . . . . . 9  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  z  =/=  T
)  ->  ( 2nd `  ( 1st `  z
) )  =/=  ( 2nd `  ( 1st `  T
) ) )
207191, 3, 192, 193, 194, 206poimirlem9 32013 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  z  =/=  T
)  ->  ( 2nd `  ( 1st `  z
) )  =  ( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) ) )
208103adantr 472 . . . . . . . 8  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  z  =/=  T
)  ->  ( 2nd `  z )  =  ( 2nd `  T ) )
209190, 207, 208jca31 543 . . . . . . 7  |-  ( ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  /\  z  =/=  T
)  ->  ( (
( 1st `  ( 1st `  z ) )  =  ( 1st `  ( 1st `  T ) )  /\  ( 2nd `  ( 1st `  z ) )  =  ( ( 2nd `  ( 1st `  T
) )  o.  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) ) ) )  /\  ( 2nd `  z )  =  ( 2nd `  T
) ) )
210209ex 441 . . . . . 6  |-  ( ( ( ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  /\  z  e.  S )  ->  (
z  =/=  T  -> 
( ( ( 1st `  ( 1st `  z
) )  =  ( 1st `  ( 1st `  T ) )  /\  ( 2nd `  ( 1st `  z ) )  =  ( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) ) )  /\  ( 2nd `  z )  =  ( 2nd `  T ) ) ) )
211 simplr 770 . . . . . . . 8  |-  ( ( ( ( 1st `  ( 1st `  z ) )  =  ( 1st `  ( 1st `  T ) )  /\  ( 2nd `  ( 1st `  z ) )  =  ( ( 2nd `  ( 1st `  T
) )  o.  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) ) ) )  /\  ( 2nd `  z )  =  ( 2nd `  T
) )  ->  ( 2nd `  ( 1st `  z
) )  =  ( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) ) )
212 elfznn 11854 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  ->  ( 2nd `  T )  e.  NN )
213212nnred 10646 . . . . . . . . . . . . 13  |-  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  ->  ( 2nd `  T )  e.  RR )
214213ltp1d 10559 . . . . . . . . . . . . 13  |-  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  ->  ( 2nd `  T )  < 
( ( 2nd `  T
)  +  1 ) )
215213, 214ltned 9788 . . . . . . . . . . . 12  |-  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  ->  ( 2nd `  T )  =/=  ( ( 2nd `  T
)  +  1 ) )
216215adantl 473 . . . . . . . . . . 11  |-  ( (
ph  /\  ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) ) )  ->  ( 2nd `  T )  =/=  (
( 2nd `  T
)  +  1 ) )
217 fveq1 5878 . . . . . . . . . . . . 13  |-  ( ( 2nd `  ( 1st `  T ) )  =  ( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) )  ->  ( ( 2nd `  ( 1st `  T
) ) `  ( 2nd `  T ) )  =  ( ( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) ) `
 ( 2nd `  T
) ) )
218 id 22 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2nd `  T )  e.  RR  ->  ( 2nd `  T )  e.  RR )
219 ltp1 10465 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2nd `  T )  e.  RR  ->  ( 2nd `  T )  < 
( ( 2nd `  T
)  +  1 ) )
220218, 219ltned 9788 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2nd `  T )  e.  RR  ->  ( 2nd `  T )  =/=  ( ( 2nd `  T
)  +  1 ) )
221 fvex 5889 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 2nd `  T )  e.  _V
222 ovex 6336 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 2nd `  T )  +  1 )  e. 
_V
223221, 222, 222, 221fpr 6088 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2nd `  T )  =/=  ( ( 2nd `  T )  +  1 )  ->  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. } : {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } --> { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) } )
224220, 223syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 2nd `  T )  e.  RR  ->  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. } : {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } --> { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) } )
225 f1oi 5864 . . . . . . . . . . . . . . . . . . . . 21  |-  (  _I  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) : ( ( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) -1-1-onto-> ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
226 f1of 5828 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (  _I  |`  ( (
1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) : ( ( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) -1-1-onto-> ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  ->  (  _I  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) : ( ( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) --> ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) )
227225, 226ax-mp 5 . . . . . . . . . . . . . . . . . . . 20  |-  (  _I  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) : ( ( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) --> ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )
228 disjdif 3830 . . . . . . . . . . . . . . . . . . . . 21  |-  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  i^i  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  =  (/)
229 fun 5758 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. } : {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } --> { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) }  /\  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) : ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) --> ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  /\  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  i^i  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  =  (/) )  ->  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) : ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) --> ( { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) }  u.  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )
230228, 229mpan2 685 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } : { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } --> { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) }  /\  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) : ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) --> ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  ->  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) ) : ( { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) }  u.  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) --> ( { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) }  u.  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )
231224, 227, 230sylancl 675 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2nd `  T )  e.  RR  ->  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) ) : ( { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) }  u.  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) --> ( { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) }  u.  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )
232221prid1 4071 . . . . . . . . . . . . . . . . . . . 20  |-  ( 2nd `  T )  e.  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }
233 elun1 3592 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( 2nd `  T )  e.  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  ->  ( 2nd `  T )  e.  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  u.  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )
234232, 233ax-mp 5 . . . . . . . . . . . . . . . . . . 19  |-  ( 2nd `  T )  e.  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  u.  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )
235 fvco3 5957 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) : ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) --> ( { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) }  u.  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  /\  ( 2nd `  T )  e.  ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )  ->  ( ( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) ) `
 ( 2nd `  T
) )  =  ( ( 2nd `  ( 1st `  T ) ) `
 ( ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) ) `
 ( 2nd `  T
) ) ) )
236231, 234, 235sylancl 675 . . . . . . . . . . . . . . . . . 18  |-  ( ( 2nd `  T )  e.  RR  ->  (
( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) ) `
 ( 2nd `  T
) )  =  ( ( 2nd `  ( 1st `  T ) ) `
 ( ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) ) `
 ( 2nd `  T
) ) ) )
237 ffn 5739 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } : { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } --> { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) }  ->  {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  Fn  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
238224, 237syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 2nd `  T )  e.  RR  ->  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  Fn  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
239 fnresi 5703 . . . . . . . . . . . . . . . . . . . . . 22  |-  (  _I  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  Fn  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )
240228, 232pm3.2i 462 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  i^i  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  =  (/)  /\  ( 2nd `  T
)  e.  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) } )
241 fvun1 5951 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  Fn  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  /\  (  _I  |`  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) )  Fn  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  /\  ( ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  i^i  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  =  (/)  /\  ( 2nd `  T
)  e.  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) } ) )  ->  ( ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)