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 31967
Description: Lemma for poimir 31985, that the face in poimirlem22 31974 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 3195 . . . . . . 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 2549 . . . . . 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 6828 . . . . 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 6828 . . . . 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 6829 . . . . . . . 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 5880 . . . . . . . 8  |-  ( 2nd `  ( 1st `  T
) )  e.  _V
12 f1oeq1 5810 . . . . . . . 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 3187 . . . . . . 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 200 . . . . . 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 11835 . . . . . . . . . . . . 13  |-  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  ->  ( 2nd `  T )  e.  NN )
1715, 16syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2nd `  T
)  e.  NN )
1817nnred 10631 . . . . . . . . . . 11  |-  ( ph  ->  ( 2nd `  T
)  e.  RR )
1918ltp1d 10544 . . . . . . . . . . 11  |-  ( ph  ->  ( 2nd `  T
)  <  ( ( 2nd `  T )  +  1 ) )
2018, 19ltned 9776 . . . . . . . . . 10  |-  ( ph  ->  ( 2nd `  T
)  =/=  ( ( 2nd `  T )  +  1 ) )
2120necomd 2681 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  =/=  ( 2nd `  T
) )
22 fvex 5880 . . . . . . . . . . 11  |-  ( 2nd `  T )  e.  _V
23 ovex 6323 . . . . . . . . . . 11  |-  ( ( 2nd `  T )  +  1 )  e. 
_V
24 f1oprg 5860 . . . . . . . . . . 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 680 . . . . . . . . . 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 667 . . . . . . . . 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 4053 . . . . . . . . . 10  |-  { ( ( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) }  =  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }
28 f1oeq3 5812 . . . . . . . . . 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 200 . . . . . . . 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 5855 . . . . . . . 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 3841 . . . . . . . . 9  |-  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  i^i  ( ( 1 ... N )  \  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  =  (/)
33 f1oun 5838 . . . . . . . . 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 692 . . . . . . . 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 669 . . . . . . 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 10632 . . . . . . . . . . . . . 14  |-  ( ph  ->  N  e.  CC )
38 npcan1 10051 . . . . . . . . . . . . . 14  |-  ( N  e.  CC  ->  (
( N  -  1 )  +  1 )  =  N )
3937, 38syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( N  - 
1 )  +  1 )  =  N )
4036nnzd 11046 . . . . . . . . . . . . . . 15  |-  ( ph  ->  N  e.  ZZ )
41 peano2zm 10987 . . . . . . . . . . . . . . 15  |-  ( N  e.  ZZ  ->  ( N  -  1 )  e.  ZZ )
4240, 41syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( N  -  1 )  e.  ZZ )
43 uzid 11180 . . . . . . . . . . . . . 14  |-  ( ( N  -  1 )  e.  ZZ  ->  ( N  -  1 )  e.  ( ZZ>= `  ( N  -  1 ) ) )
44 peano2uz 11219 . . . . . . . . . . . . . 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 2532 . . . . . . . . . . . 12  |-  ( ph  ->  N  e.  ( ZZ>= `  ( N  -  1
) ) )
47 fzss2 11845 . . . . . . . . . . . 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 3435 . . . . . . . . . 10  |-  ( ph  ->  ( 2nd `  T
)  e.  ( 1 ... N ) )
5017peano2nnd 10633 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  e.  NN )
5142zred 11047 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  -  1 )  e.  RR )
5236nnred 10631 . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  RR )
53 elfzle2 11810 . . . . . . . . . . . . . 14  |-  ( ( 2nd `  T )  e.  ( 1 ... ( N  -  1 ) )  ->  ( 2nd `  T )  <_ 
( N  -  1 ) )
5415, 53syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2nd `  T
)  <_  ( N  -  1 ) )
5552ltm1d 10546 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N  -  1 )  <  N )
5618, 51, 52, 54, 55lelttrd 9798 . . . . . . . . . . . 12  |-  ( ph  ->  ( 2nd `  T
)  <  N )
5717nnzd 11046 . . . . . . . . . . . . 13  |-  ( ph  ->  ( 2nd `  T
)  e.  ZZ )
58 zltp1le 10993 . . . . . . . . . . . . 13  |-  ( ( ( 2nd `  T
)  e.  ZZ  /\  N  e.  ZZ )  ->  ( ( 2nd `  T
)  <  N  <->  ( ( 2nd `  T )  +  1 )  <_  N
) )
5957, 40, 58syl2anc 667 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( 2nd `  T
)  <  N  <->  ( ( 2nd `  T )  +  1 )  <_  N
) )
6056, 59mpbid 214 . . . . . . . . . . 11  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  <_  N )
61 fznn 11870 . . . . . . . . . . . 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 934 . . . . . . . . . 10  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... N ) )
64 prssi 4131 . . . . . . . . . 10  |-  ( ( ( 2nd `  T
)  e.  ( 1 ... N )  /\  ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... N ) )  ->  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } 
C_  ( 1 ... N ) )
6549, 63, 64syl2anc 667 . . . . . . . . 9  |-  ( ph  ->  { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } 
C_  ( 1 ... N ) )
66 undif 3850 . . . . . . . . 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 200 . . . . . . . 8  |-  ( ph  ->  ( { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) }  u.  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) )  =  ( 1 ... N
) )
68 f1oeq23 5813 . . . . . . . 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 667 . . . . . . 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 214 . . . . . 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 5841 . . . . . 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 667 . . . . 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 4645 . . . . . . . 8  |-  { <. ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. (
( 2nd `  T
)  +  1 ) ,  ( 2nd `  T
) >. }  e.  _V
74 ovex 6323 . . . . . . . . 9  |-  ( 1 ... N )  e. 
_V
75 difexg 4554 . . . . . . . . 9  |-  ( ( 1 ... N )  e.  _V  ->  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  e.  _V )
76 resiexg 6734 . . . . . . . . 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 6594 . . . . . . 7  |-  ( {
<. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. }  u.  (  _I  |`  ( ( 1 ... N ) 
\  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) ) )  e.  _V
7911, 78coex 6750 . . . . . 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 5810 . . . . . 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 3187 . . . . 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 216 . . . 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 4869 . . . 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 667 . . 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 11209 . . . . . 6  |-  1  e.  ( ZZ>= `  0 )
86 fzss1 11844 . . . . . 6  |-  ( 1  e.  ( ZZ>= `  0
)  ->  ( 1 ... N )  C_  ( 0 ... N
) )
8785, 86ax-mp 5 . . . . 5  |-  ( 1 ... N )  C_  ( 0 ... N
)
8848, 87syl6ss 3446 . . . 4  |-  ( ph  ->  ( 1 ... ( N  -  1 ) )  C_  ( 0 ... N ) )
8988, 15sseldd 3435 . . 3  |-  ( ph  ->  ( 2nd `  T
)  e.  ( 0 ... N ) )
90 opelxpi 4869 . . 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 667 . 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 5870 . . . . . . . . . . . 12  |-  ( t  =  T  ->  ( 2nd `  t )  =  ( 2nd `  T
) )
9392breq2d 4417 . . . . . . . . . . 11  |-  ( t  =  T  ->  (
y  <  ( 2nd `  t )  <->  y  <  ( 2nd `  T ) ) )
9493ifbid 3905 . . . . . . . . . 10  |-  ( t  =  T  ->  if ( y  <  ( 2nd `  t ) ,  y ,  ( y  +  1 ) )  =  if ( y  <  ( 2nd `  T
) ,  y ,  ( y  +  1 ) ) )
9594csbeq1d 3372 . . . . . . . . 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 5870 . . . . . . . . . . . 12  |-  ( t  =  T  ->  ( 1st `  t )  =  ( 1st `  T
) )
9796fveq2d 5874 . . . . . . . . . . 11  |-  ( t  =  T  ->  ( 1st `  ( 1st `  t
) )  =  ( 1st `  ( 1st `  T ) ) )
9896fveq2d 5874 . . . . . . . . . . . . . 14  |-  ( t  =  T  ->  ( 2nd `  ( 1st `  t
) )  =  ( 2nd `  ( 1st `  T ) ) )
9998imaeq1d 5170 . . . . . . . . . . . . 13  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( 1 ... j ) ) )
10099xpeq1d 4860 . . . . . . . . . . . 12  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( 1 ... j ) )  X. 
{ 1 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( 1 ... j
) )  X.  {
1 } ) )
10198imaeq1d 5170 . . . . . . . . . . . . 13  |-  ( t  =  T  ->  (
( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  =  ( ( 2nd `  ( 1st `  T ) )
" ( ( j  +  1 ) ... N ) ) )
102101xpeq1d 4860 . . . . . . . . . . . 12  |-  ( t  =  T  ->  (
( ( 2nd `  ( 1st `  t ) )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } )  =  ( ( ( 2nd `  ( 1st `  T ) ) "
( ( j  +  1 ) ... N
) )  X.  {
0 } ) )
103100, 102uneq12d 3591 . . . . . . . . . . 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 6313 . . . . . . . . . 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 3783 . . . . . . . . 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 2487 . . . . . . . 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 4493 . . . . . . 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 2463 . . . . . 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 3200 . . . . 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 466 . . . 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 5343 . . . . . . . . . 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 5820 . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . 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 3627 . . . . . . . . . . . . . . 15  |-  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  i^i  ( 1 ... y ) )  =  ( ( 1 ... y )  i^i  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
117 elfznn0 11894 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  NN0 )
118117nn0red 10933 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  RR )
119 ltnle 9718 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( y  e.  RR  /\  ( 2nd `  T )  e.  RR )  -> 
( y  <  ( 2nd `  T )  <->  -.  ( 2nd `  T )  <_ 
y ) )
120118, 18, 119syl2anr 481 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
y  <  ( 2nd `  T )  <->  -.  ( 2nd `  T )  <_ 
y ) )
121120biimpa 487 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  -.  ( 2nd `  T )  <_  y )
122 elfzle2 11810 . . . . . . . . . . . . . . . . . . 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 4034 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1 ... y
)  i^i  { ( 2nd `  T ) } )  =  (/)  <->  -.  ( 2nd `  T )  e.  ( 1 ... y
) )
125123, 124sylibr 216 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 1 ... y
)  i^i  { ( 2nd `  T ) } )  =  (/) )
126118ad2antlr 734 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  y  e.  RR )
12718ad2antrr 733 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( 2nd `  T )  e.  RR )
12850nnred 10631 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  e.  RR )
129128ad2antrr 733 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 2nd `  T
)  +  1 )  e.  RR )
130 simpr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  y  <  ( 2nd `  T
) )
13119ad2antrr 733 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( 2nd `  T )  < 
( ( 2nd `  T
)  +  1 ) )
132126, 127, 129, 130, 131lttrd 9801 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  y  <  ( ( 2nd `  T
)  +  1 ) )
133 ltnle 9718 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  RR  /\  ( ( 2nd `  T
)  +  1 )  e.  RR )  -> 
( y  <  (
( 2nd `  T
)  +  1 )  <->  -.  ( ( 2nd `  T
)  +  1 )  <_  y ) )
134118, 128, 133syl2anr 481 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
y  <  ( ( 2nd `  T )  +  1 )  <->  -.  (
( 2nd `  T
)  +  1 )  <_  y ) )
135134adantr 467 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
y  <  ( ( 2nd `  T )  +  1 )  <->  -.  (
( 2nd `  T
)  +  1 )  <_  y ) )
136132, 135mpbid 214 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  -.  ( ( 2nd `  T
)  +  1 )  <_  y )
137 elfzle2 11810 . . . . . . . . . . . . . . . . . . 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 4034 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1 ... y
)  i^i  { (
( 2nd `  T
)  +  1 ) } )  =  (/)  <->  -.  ( ( 2nd `  T
)  +  1 )  e.  ( 1 ... y ) )
140138, 139sylibr 216 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 1 ... y
)  i^i  { (
( 2nd `  T
)  +  1 ) } )  =  (/) )
141125, 140uneq12d 3591 . . . . . . . . . . . . . . . 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 3973 . . . . . . . . . . . . . . . . . 18  |-  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) }  =  ( { ( 2nd `  T
) }  u.  {
( ( 2nd `  T
)  +  1 ) } )
143142ineq2i 3633 . . . . . . . . . . . . . . . . 17  |-  ( ( 1 ... y )  i^i  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  =  ( ( 1 ... y
)  i^i  ( {
( 2nd `  T
) }  u.  {
( ( 2nd `  T
)  +  1 ) } ) )
144 indi 3691 . . . . . . . . . . . . . . . . 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 2476 . . . . . . . . . . . . . . . 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 3761 . . . . . . . . . . . . . . . 16  |-  ( (/)  u.  (/) )  =  (/)
147141, 145, 1463eqtr3g 2510 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 1 ... y
)  i^i  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  =  (/) )
148116, 147syl5eq 2499 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( { ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) }  i^i  ( 1 ... y ) )  =  (/) )
149 fnimadisj 5701 . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( { <. ( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) >. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T ) >. } "
( 1 ... y
) )  =  (/) )
15139adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  =  N )
152 elfzuz3 11804 . . . . . . . . . . . . . . . . . . . 20  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  ( N  -  1 )  e.  ( ZZ>= `  y
) )
153 peano2uz 11219 . . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( N  -  1 )  +  1 )  e.  ( ZZ>= `  y
) )
156151, 155eqeltrrd 2532 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ( ZZ>= `  y )
)
157 fzss2 11845 . . . . . . . . . . . . . . . . 17  |-  ( N  e.  ( ZZ>= `  y
)  ->  ( 1 ... y )  C_  ( 1 ... N
) )
158 reldisj 3810 . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
1 ... y )  C_  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )
162 resiima 5185 . . . . . . . . . . . . . 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 3591 . . . . . . . . . . . 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 5252 . . . . . . . . . . . 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 3580 . . . . . . . . . . . . 13  |-  ( (/)  u.  ( 1 ... y
) )  =  ( ( 1 ... y
)  u.  (/) )
167 un0 3761 . . . . . . . . . . . . 13  |-  ( ( 1 ... y )  u.  (/) )  =  ( 1 ... y )
168166, 167eqtr2i 2476 . . . . . . . . . . . 12  |-  ( 1 ... y )  =  ( (/)  u.  (
1 ... y ) )
169164, 165, 1683eqtr4g 2512 . . . . . . . . . . 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 5171 . . . . . . . . . 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 2499 . . . . . . . . 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 4860 . . . . . . . 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 5343 . . . . . . . . . 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 5252 . . . . . . . . . . . . 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 5182 . . . . . . . . . . . . . . . . 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 5699 . . . . . . . . . . . . . . . . . . 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 733 . . . . . . . . . . . . . . . . 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 11807 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  y  e.  ZZ )
181 zltp1le 10993 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( y  e.  ZZ  /\  ( 2nd `  T )  e.  ZZ )  -> 
( y  <  ( 2nd `  T )  <->  ( y  +  1 )  <_ 
( 2nd `  T
) ) )
182180, 57, 181syl2anr 481 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
y  <  ( 2nd `  T )  <->  ( y  +  1 )  <_ 
( 2nd `  T
) ) )
183182biimpa 487 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
y  +  1 )  <_  ( 2nd `  T
) )
18418, 52, 56ltled 9788 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( 2nd `  T
)  <_  N )
185184ad2antrr 733 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( 2nd `  T )  <_  N )
18657adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  ( 2nd `  T )  e.  ZZ )
187 nn0p1nn 10916 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  e.  NN0  ->  ( y  +  1 )  e.  NN )
188117, 187syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
y  +  1 )  e.  NN )
189188nnzd 11046 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
y  +  1 )  e.  ZZ )
190189adantl 468 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
y  +  1 )  e.  ZZ )
19140adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  N  e.  ZZ )
192 elfz 11797 . . . . . . . . . . . . . . . . . . . . . 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 1269 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  T
)  e.  ( ( y  +  1 ) ... N )  <->  ( (
y  +  1 )  <_  ( 2nd `  T
)  /\  ( 2nd `  T )  <_  N
) ) )
194193adantr 467 . . . . . . . . . . . . . . . . . . . 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 934 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  ( 2nd `  T )  e.  ( ( y  +  1 ) ... N
) )
196 1red 9663 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  1  e.  RR )
197 ltle 9727 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( y  e.  RR  /\  ( 2nd `  T )  e.  RR )  -> 
( y  <  ( 2nd `  T )  -> 
y  <_  ( 2nd `  T ) ) )
198118, 18, 197syl2anr 481 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
y  <  ( 2nd `  T )  ->  y  <_  ( 2nd `  T
) ) )
199198imp 431 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  y  <_  ( 2nd `  T
) )
200126, 127, 196, 199leadd1dd 10234 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
y  +  1 )  <_  ( ( 2nd `  T )  +  1 ) )
20160ad2antrr 733 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 2nd `  T
)  +  1 )  <_  N )
20257peano2zd 11050 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( 2nd `  T
)  +  1 )  e.  ZZ )
203202adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( 2nd `  T
)  +  1 )  e.  ZZ )
204 elfz 11797 . . . . . . . . . . . . . . . . . . . . . 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 1269 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  ->  (
( ( 2nd `  T
)  +  1 )  e.  ( ( y  +  1 ) ... N )  <->  ( (
y  +  1 )  <_  ( ( 2nd `  T )  +  1 )  /\  ( ( 2nd `  T )  +  1 )  <_  N ) ) )
206205adantr 467 . . . . . . . . . . . . . . . . . . . 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 934 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  (
( 2nd `  T
)  +  1 )  e.  ( ( y  +  1 ) ... N ) )
208 prssi 4131 . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  y  e.  ( 0 ... ( N  -  1 ) ) )  /\  y  <  ( 2nd `  T
) )  ->  { ( 2nd `  T ) ,  ( ( 2nd `  T )  +  1 ) }  C_  (
( y  +  1 ) ... N ) )
210 imass2 5207 . . . . . . . . . . . . . . . . . 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 3469 . . . . . . . . . . . . . . . 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 3451 . . . . . . . . . . . . . . 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 5826 . . . . . . . . . . . . . . . . . 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 5801 . . . . . . . . . . . . . . . . . 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 2503 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ran  { <. ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 )
>. ,  <. ( ( 2nd `  T )  +  1 ) ,  ( 2nd `  T
) >. }  =  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )
218217ad2antrr 733 . . . . . . . . . . . . . . 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 2487 . . . . . . . . . . . . . 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 3850 . . . . . . . . . . . . . . . . 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 200 . . . . . . . . . . . . . . . 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 5171 . . . . . . . . . . . . . . 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 5698 . . . . . . . . . . . . . . . . . . 19  |-  (  _I  |`  ( ( 1 ... N )  \  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } ) )  Fn  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )
224 incom 3627 . . . . . . . . . . . . . . . . . . . 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 2475 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  i^i  {
( 2nd `  T
) ,  ( ( 2nd `  T )  +  1 ) } )  =  (/)
226 fnimadisj 5701 . . . . . . . . . . . . . . . . . . 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 679 . . . . . . . . . . . . . . . . . 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 11201 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN  =  ( ZZ>= `  1 )
230188, 229syl6eleq 2541 . . . . . . . . . . . . . . . . . . . . 21  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
y  +  1 )  e.  ( ZZ>= `  1
) )
231 fzss1 11844 . . . . . . . . . . . . . . . . . . . . 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 3571 . . . . . . . . . . . . . . . . . . 19  |-  ( y  e.  ( 0 ... ( N  -  1 ) )  ->  (
( ( y  +  1 ) ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } )  C_  (
( 1 ... N
)  \  { ( 2nd `  T ) ,  ( ( 2nd `  T
)  +  1 ) } ) )
234 resiima 5185 . . . . . . . . . . . . . . . . . . 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 ) } )