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

Theorem poimirlem15 32019
Description: Lemma for poimir 32037, that the face in poimirlem22 32026 is a face. (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 )
poimirlem15.3  |-  ( ph  ->  ( 2nd `  T
)  e.  ( 1 ... ( N  - 
1 ) ) )
Assertion
Ref Expression
poimirlem15  |-  ( ph  -> 
<. <. ( 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
)
Distinct variable groups:    f, j,
t, y    ph, j, y   
j, F, y    j, N, y    T, j, y    ph, t    f, K, j, t    f, N, t    T, f    f, F, t   
t, T    S, j,
t, y
Allowed substitution hints:    ph( f)    S( f)    K( y)

Proof of Theorem poimirlem15
StepHypRef Expression
1 poimirlem22.2 . . . . . 6  |-  ( ph  ->  T  e.  S )
2 elrabi 3181 . . . . . . 7  |-  ( 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 ) ) )
3 poimirlem22.s . . . . . . 7  |-  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 } ) ) ) ) }
42, 3eleq2s 2567 . . . . . 6  |-  ( T  e.  S  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  X.  ( 0 ... N
) ) )
51, 4syl 17 . . . . 5  |-  ( ph  ->  T  e.  ( ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )
6 xp1st 6842 . . . . 5  |-  ( 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 ) } ) )
7 xp1st 6842 . . . . 5  |-  ( ( 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 ) ) )
85, 6, 73syl 18 . . . 4  |-  ( ph  ->  ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  (
1 ... N ) ) )
9 xp2nd 6843 . . . . . . . 8  |-  ( ( 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 ) } )
105, 6, 93syl 18 . . . . . . 7  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
11 fvex 5889 . . . . . . . 8  |-  ( 2nd `  ( 1st `  T
) )  e.  _V
12 f1oeq1 5818 . . . . . . . 8  |-  ( f  =  ( 2nd `  ( 1st `  T ) )  ->  ( f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
1311, 12elab 3173 . . . . . . 7  |-  ( ( 2nd `  ( 1st `  T ) )  e. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) }  <->  ( 2nd `  ( 1st `  T
) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
1410, 13sylib 201 . . . . . 6  |-  ( ph  ->  ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
15 poimirlem15.3 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2nd `  T
)  e.  ( 1 ... ( N  - 
1 ) ) )
16 elfznn 11854 . . . . . . . . . . . . 13  |-  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  ->  ( 2nd `  T )  e.  NN )
1715, 16syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2nd `  T
)  e.  NN )
1817nnred 10646 . . . . . . . . . . 11  |-  ( ph  ->  ( 2nd `  T
)  e.  RR )
1918ltp1d 10559 . . . . . . . . . . 11  |-  ( ph  ->  ( 2nd `  T
)  <  ( ( 2nd `  T )  +  1 ) )
2018, 19ltned 9788 . . . . . . . . . 10  |-  ( ph  ->  ( 2nd `  T
)  =/=  ( ( 2nd `  T )  +  1 ) )
2120necomd 2698 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  =/=  ( 2nd `  T
) )
22 fvex 5889 . . . . . . . . . . 11  |-  ( 2nd `  T )  e.  _V
23 ovex 6336 . . . . . . . . . . 11  |-  ( ( 2nd `  T )  +  1 )  e. 
_V
24 f1oprg 5869 . . . . . . . . . . 11  |-  ( ( ( ( 2nd `  T
)  e.  _V  /\  ( ( 2nd `  T
)  +  1 )  e.  _V )  /\  ( ( ( 2nd `  T )  +  1 )  e.  _V  /\  ( 2nd `  T )  e.  _V ) )  ->  ( ( ( 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 ) } -1-1-onto-> { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) } ) )
2522, 23, 23, 22, 24mp4an 687 . . . . . . . . . 10  |-  ( ( ( 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 ) } -1-1-onto-> { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) } )
2620, 21, 25syl2anc 673 . . . . . . . . 9  |-  ( ph  ->  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } : { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } -1-1-onto-> { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) } )
27 prcom 4041 . . . . . . . . . 10  |-  { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) }  =  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }
28 f1oeq3 5820 . . . . . . . . . 10  |-  ( { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) }  =  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  ->  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. } : {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } -1-1-onto-> { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) }  <->  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. } : {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } -1-1-onto-> { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )
2927, 28ax-mp 5 . . . . . . . . 9  |-  ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } : { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } -1-1-onto-> { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) }  <->  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. } : {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } -1-1-onto-> { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
3026, 29sylib 201 . . . . . . . 8  |-  ( ph  ->  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } : { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } -1-1-onto-> { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
31 f1oi 5864 . . . . . . . 8  |-  (  _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 ) } )
32 disjdif 3830 . . . . . . . . 9  |-  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  i^i  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  =  (/)
33 f1oun 5847 . . . . . . . . 9  |-  ( ( ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. } : {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } -1-1-onto-> { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  /\  (  _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 ) } ) )  /\  (
( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  i^i  ( ( 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 ) } ) ) -1-1-onto-> ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  u.  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )
3432, 32, 33mpanr12 699 . . . . . . . 8  |-  ( ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } : { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } -1-1-onto-> { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  /\  (  _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 ) } ) )  ->  ( { <. ( 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 ) } ) ) -1-1-onto-> ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  u.  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )
3530, 31, 34sylancl 675 . . . . . . 7  |-  ( ph  ->  ( { <. ( 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 ) } ) ) -1-1-onto-> ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  u.  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )
36 poimir.0 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  NN )
3736nncnd 10647 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  CC )
38 npcan1 10065 . . . . . . . . . . . . . 14  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
3937, 38syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
4036nnzd 11062 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  ZZ )
41 peano2zm 11004 . . . . . . . . . . . . . . 15  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
4240, 41syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  -  1 )  e.  ZZ )
43 uzid 11197 . . . . . . . . . . . . . 14  |-  ( ( N  -  1 )  e.  ZZ  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
44 peano2uz 11235 . . . . . . . . . . . . . 14  |-  ( ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
4542, 43, 443syl 18 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  e.  ( ZZ>= `  ( N  -  1
) ) )
4639, 45eqeltrrd 2550 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ( ZZ>= `  ( N  -  1
) ) )
47 fzss2 11864 . . . . . . . . . . . 12  |-  ( N  e.  ( ZZ>= `  ( N  -  1 ) )  ->  ( 1 ... ( N  - 
1 ) )  C_  ( 1 ... N
) )
4846, 47syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( 1 ... ( N  -  1 ) )  C_  ( 1 ... N ) )
4948, 15sseldd 3419 . . . . . . . . . 10  |-  ( ph  ->  ( 2nd `  T
)  e.  ( 1 ... N ) )
5017peano2nnd 10648 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  e.  NN )
5142zred 11063 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  -  1 )  e.  RR )
5236nnred 10646 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  RR )
53 elfzle2 11829 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  ->  ( 2nd `  T )  <_ 
( N  -  1 ) )
5415, 53syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2nd `  T
)  <_  ( N  -  1 ) )
5552ltm1d 10561 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  -  1 )  <  N )
5618, 51, 52, 54, 55lelttrd 9810 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2nd `  T
)  <  N )
5717nnzd 11062 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2nd `  T
)  e.  ZZ )
58 zltp1le 11010 . . . . . . . . . . . . 13  |-  ( ( ( 2nd `  T
)  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( 2nd `  T
)  <  N  <->  ( ( 2nd `  T )  +  1 )  <_  N
) )
5957, 40, 58syl2anc 673 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 2nd `  T
)  <  N  <->  ( ( 2nd `  T )  +  1 )  <_  N
) )
6056, 59mpbid 215 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  <_  N )
61 fznn 11889 . . . . . . . . . . . 12  |-  ( N  e.  ZZ  ->  (
( ( 2nd `  T
)  +  1 )  e.  ( 1 ... N )  <->  ( (
( 2nd `  T
)  +  1 )  e.  NN  /\  (
( 2nd `  T
)  +  1 )  <_  N ) ) )
6240, 61syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( ( ( 2nd `  T )  +  1 )  e.  ( 1 ... N )  <->  ( (
( 2nd `  T
)  +  1 )  e.  NN  /\  (
( 2nd `  T
)  +  1 )  <_  N ) ) )
6350, 60, 62mpbir2and 936 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... N ) )
64 prssi 4119 . . . . . . . . . 10  |-  ( ( ( 2nd `  T
)  e.  ( 1 ... N )  /\  ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... N ) )  ->  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } 
C_  ( 1 ... N ) )
6549, 63, 64syl2anc 673 . . . . . . . . 9  |-  ( ph  ->  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } 
C_  ( 1 ... N ) )
66 undif 3839 . . . . . . . . 9  |-  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } 
C_  ( 1 ... N )  <->  ( {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  u.  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  =  ( 1 ... N ) )
6765, 66sylib 201 . . . . . . . 8  |-  ( ph  ->  ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) )  =  ( 1 ... N
) )
68 f1oeq23 5821 . . . . . . . 8  |-  ( ( ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) )  =  ( 1 ... N
)  /\  ( {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  u.  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  =  ( 1 ... N ) )  ->  ( ( { <. ( 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 ) } ) ) -1-1-onto-> ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  u.  ( ( 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 ) } ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
6967, 67, 68syl2anc 673 . . . . . . 7  |-  ( ph  ->  ( ( { <. ( 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 ) } ) ) -1-1-onto-> ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  u.  ( ( 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 ) } ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) ) )
7035, 69mpbid 215 . . . . . 6  |-  ( ph  ->  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) )
71 f1oco 5850 . . . . . 6  |-  ( ( ( 2nd `  ( 1st `  T ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  /\  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )  ->  (
( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
7214, 70, 71syl2anc 673 . . . . 5  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
73 prex 4642 . . . . . . . 8  |-  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  e.  _V
74 ovex 6336 . . . . . . . . 9  |-  ( 1 ... N )  e. 
_V
75 difexg 4545 . . . . . . . . 9  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  e.  _V )
76 resiexg 6748 . . . . . . . . 9  |-  ( ( ( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  e.  _V  ->  (  _I  |`  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) )  e. 
_V )
7774, 75, 76mp2b 10 . . . . . . . 8  |-  (  _I  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  e.  _V
7873, 77unex 6608 . . . . . . 7  |-  ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )  e.  _V
7911, 78coex 6764 . . . . . 6  |-  ( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) )  e.  _V
80 f1oeq1 5818 . . . . . 6  |-  ( f  =  ( ( 2nd `  ( 1st `  T
) )  o.  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) ) )  ->  ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( ( 2nd `  ( 1st `  T
) )  o.  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
8179, 80elab 3173 . . . . 5  |-  ( ( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  <-> 
( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) )
8272, 81sylibr 217 . . . 4  |-  ( ph  ->  ( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
83 opelxpi 4871 . . . 4  |-  ( ( ( 1st `  ( 1st `  T ) )  e.  ( ( 0..^ K )  ^m  (
1 ... N ) )  /\  ( ( 2nd `  ( 1st `  T
) )  o.  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) ) )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  ->  <. ( 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 ) } ) ) ) )
>.  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } ) )
848, 82, 83syl2anc 673 . . 3  |-  ( ph  -> 
<. ( 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 ) } ) ) ) ) >.  e.  (
( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
85 1eluzge0 11226 . . . . . 6  |-  1  e.  ( ZZ>= `  0 )
86 fzss1 11863 . . . . . 6  |-  ( 1  e.  ( ZZ>= `  0
)  ->  ( 1 ... N )  C_  ( 0 ... N
) )
8785, 86ax-mp 5 . . . . 5  |-  ( 1 ... N )  C_  ( 0 ... N
)
8848, 87syl6ss 3430 . . . 4  |-  ( ph  ->  ( 1 ... ( N  -  1 ) )  C_  ( 0 ... N ) )
8988, 15sseldd 3419 . . 3  |-  ( ph  ->  ( 2nd `  T
)  e.  ( 0 ... N ) )
90 opelxpi 4871 . . 3  |-  ( (
<. ( 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 ) } ) ) ) ) >.  e.  (
( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  /\  ( 2nd `  T )  e.  ( 0 ... N ) )  ->  <. <. ( 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.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )
9184, 89, 90syl2anc 673 . 2  |-  ( ph  -> 
<. <. ( 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.  ( ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  X.  ( 0 ... N ) ) )
92 fveq2 5879 . . . . . . . . . . . 12  |-  ( t  =  T  ->  ( 2nd `  t )  =  ( 2nd `  T
) )
9392breq2d 4407 . . . . . . . . . . 11  |-  ( t  =  T  ->  (
y  <  ( 2nd `  t )  <->  y  <  ( 2nd `  T ) ) )
9493ifbid 3894 . . . . . . . . . 10  |-  ( t  =  T  ->  if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  =  if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) ) )
9594csbeq1d 3356 . . . . . . . . 9  |-  ( 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 } ) ) ) )
96 fveq2 5879 . . . . . . . . . . . 12  |-  ( t  =  T  ->  ( 1st `  t )  =  ( 1st `  T
) )
9796fveq2d 5883 . . . . . . . . . . 11  |-  ( t  =  T  ->  ( 1st `  ( 1st `  t
) )  =  ( 1st `  ( 1st `  T ) ) )
9896fveq2d 5883 . . . . . . . . . . . . . 14  |-  ( t  =  T  ->  ( 2nd `  ( 1st `  t
) )  =  ( 2nd `  ( 1st `  T ) ) )
9998imaeq1d 5173 . . . . . . . . . . . . 13  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) ) )
10099xpeq1d 4862 . . . . . . . . . . . 12  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... j
) )  X.  {
1 } ) )
10198imaeq1d 5173 . . . . . . . . . . . . 13  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) ) )
102101xpeq1d 4862 . . . . . . . . . . . 12  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )
103100, 102uneq12d 3580 . . . . . . . . . . 11  |-  ( 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 } ) ) )
10497, 103oveq12d 6326 . . . . . . . . . 10  |-  ( 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 } ) ) ) )
105104csbeq2dv 3785 . . . . . . . . 9  |-  ( 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 } ) ) ) )
10695, 105eqtrd 2505 . . . . . . . 8  |-  ( 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 } ) ) ) )
107106mpteq2dv 4483 . . . . . . 7  |-  ( 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 } ) ) ) ) )
108107eqeq2d 2481 . . . . . 6  |-  ( 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 } ) ) ) ) ) )
109108, 3elrab2 3186 . . . . 5  |-  ( 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 } ) ) ) ) ) )
110109simprbi 471 . . . 4  |-  ( 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 } ) ) ) ) )
1111, 110syl 17 . . 3  |-  ( 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 } ) ) ) ) )
112 imaco 5347 . . . . . . . . . 10  |-  ( ( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) )
" ( 1 ... y ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )
" ( 1 ... y ) ) )
113 f1ofn 5829 . . . . . . . . . . . . . . . 16  |-  ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } : { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } -1-1-onto-> { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) }  ->  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  Fn  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
11426, 113syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  Fn  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
115114ad2antrr 740 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  Fn  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
116 incom 3616 . . . . . . . . . . . . . . 15  |-  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  i^i  ( 1 ... y ) )  =  ( ( 1 ... y )  i^i  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
117 elfznn0 11913 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  NN0 )
118117nn0red 10950 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  RR )
119 ltnle 9731 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  RR  /\  ( 2nd `  T )  e.  RR )  -> 
( y  <  ( 2nd `  T )  <->  -.  ( 2nd `  T )  <_ 
y ) )
120118, 18, 119syl2anr 486 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
y  <  ( 2nd `  T )  <->  -.  ( 2nd `  T )  <_ 
y ) )
121120biimpa 492 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  -.  ( 2nd `  T )  <_  y )
122 elfzle2 11829 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 2nd `  T )  e.  ( 1 ... y )  ->  ( 2nd `  T )  <_ 
y )
123121, 122nsyl 125 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  -.  ( 2nd `  T )  e.  ( 1 ... y ) )
124 disjsn 4023 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1 ... y
)  i^i  { ( 2nd `  T ) } )  =  (/)  <->  -.  ( 2nd `  T )  e.  ( 1 ... y
) )
125123, 124sylibr 217 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 1 ... y
)  i^i  { ( 2nd `  T ) } )  =  (/) )
126118ad2antlr 741 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  y  e.  RR )
12718ad2antrr 740 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( 2nd `  T )  e.  RR )
12850nnred 10646 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  e.  RR )
129128ad2antrr 740 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 2nd `  T
)  +  1 )  e.  RR )
130 simpr 468 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  y  <  ( 2nd `  T
) )
13119ad2antrr 740 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( 2nd `  T )  < 
( ( 2nd `  T
)  +  1 ) )
132126, 127, 129, 130, 131lttrd 9813 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  y  <  ( ( 2nd `  T
)  +  1 ) )
133 ltnle 9731 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  RR  /\  ( ( 2nd `  T
)  +  1 )  e.  RR )  -> 
( y  <  (
( 2nd `  T
)  +  1 )  <->  -.  ( ( 2nd `  T
)  +  1 )  <_  y ) )
134118, 128, 133syl2anr 486 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
y  <  ( ( 2nd `  T )  +  1 )  <->  -.  (
( 2nd `  T
)  +  1 )  <_  y ) )
135134adantr 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
y  <  ( ( 2nd `  T )  +  1 )  <->  -.  (
( 2nd `  T
)  +  1 )  <_  y ) )
136132, 135mpbid 215 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  -.  ( ( 2nd `  T
)  +  1 )  <_  y )
137 elfzle2 11829 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... y )  ->  (
( 2nd `  T
)  +  1 )  <_  y )
138136, 137nsyl 125 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  -.  ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... y ) )
139 disjsn 4023 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1 ... y
)  i^i  { (
( 2nd `  T
)  +  1 ) } )  =  (/)  <->  -.  ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... y ) )
140138, 139sylibr 217 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 1 ... y
)  i^i  { (
( 2nd `  T
)  +  1 ) } )  =  (/) )
141125, 140uneq12d 3580 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( ( 1 ... y )  i^i  {
( 2nd `  T
) } )  u.  ( ( 1 ... y )  i^i  {
( ( 2nd `  T
)  +  1 ) } ) )  =  ( (/)  u.  (/) ) )
142 df-pr 3962 . . . . . . . . . . . . . . . . . 18  |-  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) }  =  ( { ( 2nd `  T
) }  u.  {
( ( 2nd `  T
)  +  1 ) } )
143142ineq2i 3622 . . . . . . . . . . . . . . . . 17  |-  ( ( 1 ... y )  i^i  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  =  ( ( 1 ... y
)  i^i  ( {
( 2nd `  T
) }  u.  {
( ( 2nd `  T
)  +  1 ) } ) )
144 indi 3680 . . . . . . . . . . . . . . . . 17  |-  ( ( 1 ... y )  i^i  ( { ( 2nd `  T ) }  u.  { ( ( 2nd `  T
)  +  1 ) } ) )  =  ( ( ( 1 ... y )  i^i 
{ ( 2nd `  T
) } )  u.  ( ( 1 ... y )  i^i  {
( ( 2nd `  T
)  +  1 ) } ) )
145143, 144eqtr2i 2494 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1 ... y
)  i^i  { ( 2nd `  T ) } )  u.  ( ( 1 ... y )  i^i  { ( ( 2nd `  T )  +  1 ) } ) )  =  ( ( 1 ... y
)  i^i  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )
146 un0 3762 . . . . . . . . . . . . . . . 16  |-  ( (/)  u.  (/) )  =  (/)
147141, 145, 1463eqtr3g 2528 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 1 ... y
)  i^i  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  =  (/) )
148116, 147syl5eq 2517 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  i^i  ( 1 ... y ) )  =  (/) )
149 fnimadisj 5706 . . . . . . . . . . . . . 14  |-  ( ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  Fn  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  /\  ( { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) }  i^i  (
1 ... y ) )  =  (/) )  ->  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } "
( 1 ... y
) )  =  (/) )
150115, 148, 149syl2anc 673 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } "
( 1 ... y
) )  =  (/) )
15139adantr 472 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  =  N )
152 elfzuz3 11823 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  ( N  -  1 )  e.  ( ZZ>= `  y
) )
153 peano2uz 11235 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( N  -  1 )  e.  ( ZZ>= `  y
)  ->  ( ( N  -  1 )  +  1 )  e.  ( ZZ>= `  y )
)
154152, 153syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
( N  -  1 )  +  1 )  e.  ( ZZ>= `  y
) )
155154adantl 473 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  e.  ( ZZ>= `  y
) )
156151, 155eqeltrrd 2550 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  y )
)
157 fzss2 11864 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  ( ZZ>= `  y
)  ->  ( 1 ... y )  C_  ( 1 ... N
) )
158 reldisj 3812 . . . . . . . . . . . . . . . . 17  |-  ( ( 1 ... y ) 
C_  ( 1 ... N )  ->  (
( ( 1 ... y )  i^i  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  (/)  <->  ( 1 ... y )  C_  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )
159156, 157, 1583syl 18 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( 1 ... y )  i^i  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  (/)  <->  ( 1 ... y )  C_  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )
160159adantr 472 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( ( 1 ... y )  i^i  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  (/)  <->  ( 1 ... y )  C_  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) )
161147, 160mpbid 215 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
1 ... y )  C_  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )
162 resiima 5188 . . . . . . . . . . . . . 14  |-  ( ( 1 ... y ) 
C_  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  ->  ( (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) " (
1 ... y ) )  =  ( 1 ... y ) )
163161, 162syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
(  _I  |`  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) "
( 1 ... y
) )  =  ( 1 ... y ) )
164150, 163uneq12d 3580 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. } " (
1 ... y ) )  u.  ( (  _I  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) " (
1 ... y ) ) )  =  ( (/)  u.  ( 1 ... y
) ) )
165 imaundir 5255 . . . . . . . . . . . 12  |-  ( ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )
" ( 1 ... y ) )  =  ( ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. } " (
1 ... y ) )  u.  ( (  _I  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) " (
1 ... y ) ) )
166 uncom 3569 . . . . . . . . . . . . 13  |-  ( (/)  u.  ( 1 ... y
) )  =  ( ( 1 ... y
)  u.  (/) )
167 un0 3762 . . . . . . . . . . . . 13  |-  ( ( 1 ... y )  u.  (/) )  =  ( 1 ... y )
168166, 167eqtr2i 2494 . . . . . . . . . . . 12  |-  ( 1 ... y )  =  ( (/)  u.  (
1 ... y ) )
169164, 165, 1683eqtr4g 2530 . . . . . . . . . . 11  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) "
( 1 ... y
) )  =  ( 1 ... y ) )
170169imaeq2d 5174 . . . . . . . . . 10  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 2nd `  ( 1st `  T ) )
" ( ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )
" ( 1 ... y ) ) )  =  ( ( 2nd `  ( 1st `  T
) ) " (
1 ... y ) ) )
171112, 170syl5eq 2517 . . . . . . . . 9  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 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 ) } ) ) ) )
" ( 1 ... y ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) ) )
172171xpeq1d 4862 . . . . . . . 8  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 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 ) } ) ) ) ) " ( 1 ... y ) )  X.  { 1 } )  =  ( ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... y ) )  X. 
{ 1 } ) )
173 imaco 5347 . . . . . . . . . 10  |-  ( ( ( 2nd `  ( 1st `  T ) )  o.  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  u.  (  _I  |`  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) ) )
" ( ( y  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )
" ( ( y  +  1 ) ... N ) ) )
174 imaundir 5255 . . . . . . . . . . . . 13  |-  ( ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )
" ( ( y  +  1 ) ... N ) )  =  ( ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. } " (
( y  +  1 ) ... N ) )  u.  ( (  _I  |`  ( (
1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) " (
( y  +  1 ) ... N ) ) )
175 imassrn 5185 . . . . . . . . . . . . . . . . 17  |-  ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } "
( ( y  +  1 ) ... N
) )  C_  ran  {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }
176175a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } "
( ( y  +  1 ) ... N
) )  C_  ran  {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } )
177 fnima 5704 . . . . . . . . . . . . . . . . . . 19  |-  ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  Fn  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  ->  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. } " {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  ran  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } )
17826, 113, 1773syl 18 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. } " {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  ran  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } )
179178ad2antrr 740 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } " { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  ran  { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } )
180 elfzelz 11826 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  ZZ )
181 zltp1le 11010 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  ZZ  /\  ( 2nd `  T )  e.  ZZ )  -> 
( y  <  ( 2nd `  T )  <->  ( y  +  1 )  <_ 
( 2nd `  T
) ) )
182180, 57, 181syl2anr 486 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
y  <  ( 2nd `  T )  <->  ( y  +  1 )  <_ 
( 2nd `  T
) ) )
183182biimpa 492 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
y  +  1 )  <_  ( 2nd `  T
) )
18418, 52, 56ltled 9800 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( 2nd `  T
)  <_  N )
185184ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( 2nd `  T )  <_  N )
18657adantr 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( 2nd `  T )  e.  ZZ )
187 nn0p1nn 10933 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  NN0  ->  ( y  +  1 )  e.  NN )
188117, 187syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
y  +  1 )  e.  NN )
189188nnzd 11062 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
y  +  1 )  e.  ZZ )
190189adantl 473 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
y  +  1 )  e.  ZZ )
19140adantr 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ZZ )
192 elfz 11816 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( 2nd `  T
)  e.  ZZ  /\  ( y  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( 2nd `  T
)  e.  ( ( y  +  1 ) ... N )  <->  ( (
y  +  1 )  <_  ( 2nd `  T
)  /\  ( 2nd `  T )  <_  N
) ) )
193186, 190, 191, 192syl3anc 1292 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  T
)  e.  ( ( y  +  1 ) ... N )  <->  ( (
y  +  1 )  <_  ( 2nd `  T
)  /\  ( 2nd `  T )  <_  N
) ) )
194193adantr 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 2nd `  T
)  e.  ( ( y  +  1 ) ... N )  <->  ( (
y  +  1 )  <_  ( 2nd `  T
)  /\  ( 2nd `  T )  <_  N
) ) )
195183, 185, 194mpbir2and 936 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( 2nd `  T )  e.  ( ( y  +  1 ) ... N
) )
196 1red 9676 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  1  e.  RR )
197 ltle 9740 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  RR  /\  ( 2nd `  T )  e.  RR )  -> 
( y  <  ( 2nd `  T )  -> 
y  <_  ( 2nd `  T ) ) )
198118, 18, 197syl2anr 486 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
y  <  ( 2nd `  T )  ->  y  <_  ( 2nd `  T
) ) )
199198imp 436 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  y  <_  ( 2nd `  T
) )
200126, 127, 196, 199leadd1dd 10248 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
y  +  1 )  <_  ( ( 2nd `  T )  +  1 ) )
20160ad2antrr 740 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 2nd `  T
)  +  1 )  <_  N )
20257peano2zd 11066 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  e.  ZZ )
203202adantr 472 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  T
)  +  1 )  e.  ZZ )
204 elfz 11816 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 2nd `  T
)  +  1 )  e.  ZZ  /\  (
y  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  (
( ( 2nd `  T
)  +  1 )  e.  ( ( y  +  1 ) ... N )  <->  ( (
y  +  1 )  <_  ( ( 2nd `  T )  +  1 )  /\  ( ( 2nd `  T )  +  1 )  <_  N ) ) )
205203, 190, 191, 204syl3anc 1292 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( 2nd `  T
)  +  1 )  e.  ( ( y  +  1 ) ... N )  <->  ( (
y  +  1 )  <_  ( ( 2nd `  T )  +  1 )  /\  ( ( 2nd `  T )  +  1 )  <_  N ) ) )
206205adantr 472 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( ( 2nd `  T
)  +  1 )  e.  ( ( y  +  1 ) ... N )  <->  ( (
y  +  1 )  <_  ( ( 2nd `  T )  +  1 )  /\  ( ( 2nd `  T )  +  1 )  <_  N ) ) )
207200, 201, 206mpbir2and 936 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 2nd `  T
)  +  1 )  e.  ( ( y  +  1 ) ... N ) )
208 prssi 4119 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 2nd `  T
)  e.  ( ( y  +  1 ) ... N )  /\  ( ( 2nd `  T
)  +  1 )  e.  ( ( y  +  1 ) ... N ) )  ->  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } 
C_  ( ( y  +  1 ) ... N ) )
209195, 207, 208syl2anc 673 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) }  C_  (
( y  +  1 ) ... N ) )
210 imass2 5210 . . . . . . . . . . . . . . . . . 18  |-  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } 
C_  ( ( y  +  1 ) ... N )  ->  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } " { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  C_  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } "
( ( y  +  1 ) ... N
) ) )
211209, 210syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } " { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  C_  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } "
( ( y  +  1 ) ... N
) ) )
212179, 211eqsstr3d 3453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ran  {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  C_  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } "
( ( y  +  1 ) ... N
) ) )
213176, 212eqssd 3435 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } "
( ( y  +  1 ) ... N
) )  =  ran  {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } )
214 f1ofo 5835 . . . . . . . . . . . . . . . . . 18  |-  ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } : { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } -1-1-onto-> { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) }  ->  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. } : {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }
-onto-> { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) } )
215 forn 5809 . . . . . . . . . . . . . . . . . 18  |-  ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } : { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }
-onto-> { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) }  ->  ran 
{ <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  =  { ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) } )
21626, 214, 2153syl 18 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ran  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. }  =  {
( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) } )
217216, 27syl6eq 2521 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ran  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. }  =  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
218217ad2antrr 740 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ran  {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  =  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
219213, 218eqtrd 2505 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } "
( ( y  +  1 ) ... N
) )  =  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
220 undif 3839 . . . . . . . . . . . . . . . . 17  |-  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } 
C_  ( ( y  +  1 ) ... N )  <->  ( {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  u.  ( ( ( y  +  1 ) ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  =  ( ( y  +  1 ) ... N ) )
221209, 220sylib 201 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  u.  ( ( ( y  +  1 ) ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  =  ( ( y  +  1 ) ... N ) )
222221imaeq2d 5174 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
(  _I  |`  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) "
( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( ( y  +  1 ) ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )  =  ( (  _I  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) " (
( y  +  1 ) ... N ) ) )
223 fnresi 5703 . . . . . . . . . . . . . . . . . . 19  |-  (  _I  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  Fn  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )
224 incom 3616 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  i^i  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  i^i  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )
225224, 32eqtri 2493 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  i^i  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  (/)
226 fnimadisj 5706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( (  _I  |`  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) )  Fn  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  /\  ( ( ( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  i^i  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  (/) )  -> 
( (  _I  |`  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) " { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  (/) )
227223, 225, 226mp2an 686 . . . . . . . . . . . . . . . . . 18  |-  ( (  _I  |`  ( (
1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) ) " {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  (/)
228227a1i 11 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
(  _I  |`  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) " { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  (/) )
229 nnuz 11218 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN  =  ( ZZ>= `  1 )
230188, 229syl6eleq 2559 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
y  +  1 )  e.  ( ZZ>= `  1
) )
231 fzss1 11863 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  +  1 )  e.  ( ZZ>= `  1
)  ->  ( (
y  +  1 ) ... N )  C_  ( 1 ... N
) )
232230, 231syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
( y  +  1 ) ... N ) 
C_  ( 1 ... N ) )
233232ssdifd 3558 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
( ( y  +  1 ) ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  C_  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) )
234 resiima 5188 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( y  +  1 ) ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  C_  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  ->  (
(  _I  |`  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )