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

Theorem poimirlem3 31857
Description: Lemma for poimir 31887 to add an interior point to an admissible face on the back face of the cube. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0  |-  ( ph  ->  N  e.  NN )
poimirlem4.1  |-  ( ph  ->  K  e.  NN )
poimirlem4.2  |-  ( ph  ->  M  e.  NN0 )
poimirlem4.3  |-  ( ph  ->  M  <  N )
poimirlem3.4  |-  ( ph  ->  T : ( 1 ... M ) --> ( 0..^ K ) )
poimirlem3.5  |-  ( ph  ->  U : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
Assertion
Ref Expression
poimirlem3  |-  ( ph  ->  ( A. i  e.  ( 0 ... M
) E. j  e.  ( 0 ... M
) i  =  [_ ( ( T  oF  +  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B  ->  ( <. ( T  u.  {
<. ( M  +  1 ) ,  0 >. } ) ,  ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
>.  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( M  +  1 ) ) )  X.  {
f  |  f : ( 1 ... ( M  +  1 ) ) -1-1-onto-> ( 1 ... ( M  +  1 ) ) } )  /\  ( A. i  e.  ( 0 ... M ) E. j  e.  ( 0 ... M ) i  =  [_ (
( ( T  u.  {
<. ( M  +  1 ) ,  0 >. } )  oF  +  ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X. 
{ 0 } ) )  /  p ]_ B  /\  ( ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 ( M  + 
1 ) )  =  0  /\  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) `
 ( M  + 
1 ) )  =  ( M  +  1 ) ) ) ) )
Distinct variable groups:    f, i,
j, p    ph, j    j, M    j, N    T, j    U, j    ph, i, p    B, f, i, j    f, K, i, j, p    f, M, i, p    f, N, i, p    T, f, i, p    U, f, i, p
Allowed substitution hints:    ph( f)    B( p)

Proof of Theorem poimirlem3
Dummy variable  n is distinct from all other variables.
StepHypRef Expression
1 poimirlem3.4 . . . . . . . . . . . . . . 15  |-  ( ph  ->  T : ( 1 ... M ) --> ( 0..^ K ) )
2 ffn 5743 . . . . . . . . . . . . . . 15  |-  ( T : ( 1 ... M ) --> ( 0..^ K )  ->  T  Fn  ( 1 ... M
) )
31, 2syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  T  Fn  ( 1 ... M ) )
43adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  T  Fn  ( 1 ... M
) )
5 1ex 9639 . . . . . . . . . . . . . . . . 17  |-  1  e.  _V
6 fnconstg 5785 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  _V  ->  (
( U " (
1 ... j ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... j ) ) )
75, 6ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( ( U " ( 1 ... j ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... j ) )
8 c0ex 9638 . . . . . . . . . . . . . . . . 17  |-  0  e.  _V
9 fnconstg 5785 . . . . . . . . . . . . . . . . 17  |-  ( 0  e.  _V  ->  (
( U " (
( j  +  1 ) ... M ) )  X.  { 0 } )  Fn  ( U " ( ( j  +  1 ) ... M ) ) )
108, 9ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( ( U " ( ( j  +  1 ) ... M ) )  X.  { 0 } )  Fn  ( U
" ( ( j  +  1 ) ... M ) )
117, 10pm3.2i 456 . . . . . . . . . . . . . . 15  |-  ( ( ( U " (
1 ... j ) )  X.  { 1 } )  Fn  ( U
" ( 1 ... j ) )  /\  ( ( U "
( ( j  +  1 ) ... M
) )  X.  {
0 } )  Fn  ( U " (
( j  +  1 ) ... M ) ) )
12 poimirlem3.5 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  U : ( 1 ... M ) -1-1-onto-> ( 1 ... M ) )
13 dff1o3 5834 . . . . . . . . . . . . . . . . . 18  |-  ( U : ( 1 ... M ) -1-1-onto-> ( 1 ... M
)  <->  ( U :
( 1 ... M
) -onto-> ( 1 ... M )  /\  Fun  `' U ) )
1413simprbi 465 . . . . . . . . . . . . . . . . 17  |-  ( U : ( 1 ... M ) -1-1-onto-> ( 1 ... M
)  ->  Fun  `' U
)
15 imain 5674 . . . . . . . . . . . . . . . . 17  |-  ( Fun  `' U  ->  ( U
" ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... M
) ) )  =  ( ( U "
( 1 ... j
) )  i^i  ( U " ( ( j  +  1 ) ... M ) ) ) )
1612, 14, 153syl 18 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( U " (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... M ) ) )  =  ( ( U " ( 1 ... j ) )  i^i  ( U "
( ( j  +  1 ) ... M
) ) ) )
17 elfznn0 11888 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... M )  ->  j  e.  NN0 )
1817nn0red 10927 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... M )  ->  j  e.  RR )
1918ltp1d 10538 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... M )  ->  j  <  ( j  +  1 ) )
20 fzdisj 11827 . . . . . . . . . . . . . . . . . . 19  |-  ( j  <  ( j  +  1 )  ->  (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... M ) )  =  (/) )
2119, 20syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... M )  ->  (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... M ) )  =  (/) )
2221imaeq2d 5184 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... M )  ->  ( U " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... M
) ) )  =  ( U " (/) ) )
23 ima0 5199 . . . . . . . . . . . . . . . . 17  |-  ( U
" (/) )  =  (/)
2422, 23syl6eq 2479 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  ( U " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... M
) ) )  =  (/) )
2516, 24sylan9req 2484 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( U " (
1 ... j ) )  i^i  ( U "
( ( j  +  1 ) ... M
) ) )  =  (/) )
26 fnun 5697 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  Fn  ( U "
( 1 ... j
) )  /\  (
( U " (
( j  +  1 ) ... M ) )  X.  { 0 } )  Fn  ( U " ( ( j  +  1 ) ... M ) ) )  /\  ( ( U
" ( 1 ... j ) )  i^i  ( U " (
( j  +  1 ) ... M ) ) )  =  (/) )  ->  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) )  Fn  (
( U " (
1 ... j ) )  u.  ( U "
( ( j  +  1 ) ... M
) ) ) )
2711, 25, 26sylancr 667 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... M
) )  X.  {
0 } ) )  Fn  ( ( U
" ( 1 ... j ) )  u.  ( U " (
( j  +  1 ) ... M ) ) ) )
28 imaundi 5264 . . . . . . . . . . . . . . . 16  |-  ( U
" ( ( 1 ... j )  u.  ( ( j  +  1 ) ... M
) ) )  =  ( ( U "
( 1 ... j
) )  u.  ( U " ( ( j  +  1 ) ... M ) ) )
29 nn0p1nn 10910 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  NN0  ->  ( j  +  1 )  e.  NN )
30 nnuz 11195 . . . . . . . . . . . . . . . . . . . . . 22  |-  NN  =  ( ZZ>= `  1 )
3129, 30syl6eleq 2520 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  NN0  ->  ( j  +  1 )  e.  ( ZZ>= `  1 )
)
3217, 31syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... M )  ->  (
j  +  1 )  e.  ( ZZ>= `  1
) )
33 elfzuz3 11798 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... M )  ->  M  e.  ( ZZ>= `  j )
)
34 fzsplit2 11825 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( j  +  1 )  e.  ( ZZ>= ` 
1 )  /\  M  e.  ( ZZ>= `  j )
)  ->  ( 1 ... M )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... M ) ) )
3532, 33, 34syl2anc 665 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... M )  ->  (
1 ... M )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... M ) ) )
3635eqcomd 2430 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... M )  ->  (
( 1 ... j
)  u.  ( ( j  +  1 ) ... M ) )  =  ( 1 ... M ) )
3736imaeq2d 5184 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... M )  ->  ( U " ( ( 1 ... j )  u.  ( ( j  +  1 ) ... M
) ) )  =  ( U " (
1 ... M ) ) )
38 f1ofo 5835 . . . . . . . . . . . . . . . . . 18  |-  ( U : ( 1 ... M ) -1-1-onto-> ( 1 ... M
)  ->  U :
( 1 ... M
) -onto-> ( 1 ... M ) )
39 foima 5812 . . . . . . . . . . . . . . . . . 18  |-  ( U : ( 1 ... M ) -onto-> ( 1 ... M )  -> 
( U " (
1 ... M ) )  =  ( 1 ... M ) )
4012, 38, 393syl 18 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( U " (
1 ... M ) )  =  ( 1 ... M ) )
4137, 40sylan9eqr 2485 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( U " ( ( 1 ... j )  u.  ( ( j  +  1 ) ... M
) ) )  =  ( 1 ... M
) )
4228, 41syl5eqr 2477 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( U " (
1 ... j ) )  u.  ( U "
( ( j  +  1 ) ... M
) ) )  =  ( 1 ... M
) )
4342fneq2d 5682 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... M ) )  X. 
{ 0 } ) )  Fn  ( ( U " ( 1 ... j ) )  u.  ( U "
( ( j  +  1 ) ... M
) ) )  <->  ( (
( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) )  Fn  (
1 ... M ) ) )
4427, 43mpbid 213 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... M
) )  X.  {
0 } ) )  Fn  ( 1 ... M ) )
45 ovex 6330 . . . . . . . . . . . . . 14  |-  ( 1 ... M )  e. 
_V
4645a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
1 ... M )  e. 
_V )
47 inidm 3671 . . . . . . . . . . . . 13  |-  ( ( 1 ... M )  i^i  ( 1 ... M ) )  =  ( 1 ... M
)
48 eqidd 2423 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  n  e.  ( 1 ... M
) )  ->  ( T `  n )  =  ( T `  n ) )
49 eqidd 2423 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  n  e.  ( 1 ... M
) )  ->  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... M ) )  X. 
{ 0 } ) ) `  n )  =  ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) `  n
) )
504, 44, 46, 46, 47, 48, 49offval 6549 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( T  oF  +  ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... M
) )  X.  {
0 } ) ) )  =  ( n  e.  ( 1 ... M )  |->  ( ( T `  n )  +  ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) `  n
) ) ) )
51 poimirlem4.2 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  e.  NN0 )
52 nn0p1nn 10910 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  NN0  ->  ( M  +  1 )  e.  NN )
5351, 52syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( M  +  1 )  e.  NN )
5453nnzd 11040 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( M  +  1 )  e.  ZZ )
55 uzid 11174 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  +  1 )  e.  ZZ  ->  ( M  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
56 peano2uz 11213 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) )  ->  ( ( M  +  1 )  +  1 )  e.  ( ZZ>= `  ( M  +  1 ) ) )
5754, 55, 563syl 18 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( M  + 
1 )  +  1 )  e.  ( ZZ>= `  ( M  +  1
) ) )
58 poimirlem4.3 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  M  <  N )
5951nn0zd 11039 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  M  e.  ZZ )
60 poimir.0 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  N  e.  NN )
6160nnzd 11040 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  ZZ )
62 zltp1le 10987 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  <  N  <->  ( M  +  1 )  <_  N ) )
63 peano2z 10979 . . . . . . . . . . . . . . . . . . . . 21  |-  ( M  e.  ZZ  ->  ( M  +  1 )  e.  ZZ )
64 eluz 11173 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( M  +  1 )  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  ( M  + 
1 ) )  <->  ( M  +  1 )  <_  N ) )
6563, 64sylan 473 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( N  e.  (
ZZ>= `  ( M  + 
1 ) )  <->  ( M  +  1 )  <_  N ) )
6662, 65bitr4d 259 . . . . . . . . . . . . . . . . . . 19  |-  ( ( M  e.  ZZ  /\  N  e.  ZZ )  ->  ( M  <  N  <->  N  e.  ( ZZ>= `  ( M  +  1 ) ) ) )
6759, 61, 66syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( M  <  N  <->  N  e.  ( ZZ>= `  ( M  +  1 ) ) ) )
6858, 67mpbid 213 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  N  e.  ( ZZ>= `  ( M  +  1
) ) )
69 fzsplit2 11825 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( M  + 
1 )  +  1 )  e.  ( ZZ>= `  ( M  +  1
) )  /\  N  e.  ( ZZ>= `  ( M  +  1 ) ) )  ->  ( ( M  +  1 ) ... N )  =  ( ( ( M  +  1 ) ... ( M  +  1 ) )  u.  (
( ( M  + 
1 )  +  1 ) ... N ) ) )
7057, 68, 69syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( M  + 
1 ) ... N
)  =  ( ( ( M  +  1 ) ... ( M  +  1 ) )  u.  ( ( ( M  +  1 )  +  1 ) ... N ) ) )
71 fzsn 11841 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  +  1 )  e.  ZZ  ->  (
( M  +  1 ) ... ( M  +  1 ) )  =  { ( M  +  1 ) } )
7254, 71syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( M  + 
1 ) ... ( M  +  1 ) )  =  { ( M  +  1 ) } )
7372uneq1d 3619 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( ( M  +  1 ) ... ( M  +  1 ) )  u.  (
( ( M  + 
1 )  +  1 ) ... N ) )  =  ( { ( M  +  1 ) }  u.  (
( ( M  + 
1 )  +  1 ) ... N ) ) )
7470, 73eqtrd 2463 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( M  + 
1 ) ... N
)  =  ( { ( M  +  1 ) }  u.  (
( ( M  + 
1 )  +  1 ) ... N ) ) )
7574xpeq1d 4873 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( ( M  +  1 ) ... N )  X.  {
0 } )  =  ( ( { ( M  +  1 ) }  u.  ( ( ( M  +  1 )  +  1 ) ... N ) )  X.  { 0 } ) )
76 xpundir 4904 . . . . . . . . . . . . . . 15  |-  ( ( { ( M  + 
1 ) }  u.  ( ( ( M  +  1 )  +  1 ) ... N
) )  X.  {
0 } )  =  ( ( { ( M  +  1 ) }  X.  { 0 } )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )
77 ovex 6330 . . . . . . . . . . . . . . . . 17  |-  ( M  +  1 )  e. 
_V
7877, 8xpsn 6078 . . . . . . . . . . . . . . . 16  |-  ( { ( M  +  1 ) }  X.  {
0 } )  =  { <. ( M  + 
1 ) ,  0
>. }
7978uneq1i 3616 . . . . . . . . . . . . . . 15  |-  ( ( { ( M  + 
1 ) }  X.  { 0 } )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X. 
{ 0 } ) )  =  ( {
<. ( M  +  1 ) ,  0 >. }  u.  ( (
( ( M  + 
1 )  +  1 ) ... N )  X.  { 0 } ) )
8076, 79eqtri 2451 . . . . . . . . . . . . . 14  |-  ( ( { ( M  + 
1 ) }  u.  ( ( ( M  +  1 )  +  1 ) ... N
) )  X.  {
0 } )  =  ( { <. ( M  +  1 ) ,  0 >. }  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) )
8175, 80syl6eq 2479 . . . . . . . . . . . . 13  |-  ( ph  ->  ( ( ( M  +  1 ) ... N )  X.  {
0 } )  =  ( { <. ( M  +  1 ) ,  0 >. }  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) ) )
8281adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( M  + 
1 ) ... N
)  X.  { 0 } )  =  ( { <. ( M  + 
1 ) ,  0
>. }  u.  ( ( ( ( M  + 
1 )  +  1 ) ... N )  X.  { 0 } ) ) )
8350, 82uneq12d 3621 . . . . . . . . . . 11  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  =  ( ( n  e.  ( 1 ... M )  |->  ( ( T `  n )  +  ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) `  n
) ) )  u.  ( { <. ( M  +  1 ) ,  0 >. }  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) ) ) )
84 unass 3623 . . . . . . . . . . 11  |-  ( ( ( n  e.  ( 1 ... M ) 
|->  ( ( T `  n )  +  ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( U
" ( ( j  +  1 ) ... M ) )  X. 
{ 0 } ) ) `  n ) ) )  u.  { <. ( M  +  1 ) ,  0 >. } )  u.  (
( ( ( M  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  =  ( ( n  e.  ( 1 ... M
)  |->  ( ( T `
 n )  +  ( ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) `  n
) ) )  u.  ( { <. ( M  +  1 ) ,  0 >. }  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X.  {
0 } ) ) )
8583, 84syl6eqr 2481 . . . . . . . . . 10  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( T  oF  +  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( U " ( ( j  +  1 ) ... M ) )  X.  { 0 } ) ) )  u.  ( ( ( M  +  1 ) ... N )  X.  {
0 } ) )  =  ( ( ( n  e.  ( 1 ... M )  |->  ( ( T `  n
)  +  ( ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( U "
( ( j  +  1 ) ... M
) )  X.  {
0 } ) ) `
 n ) ) )  u.  { <. ( M  +  1 ) ,  0 >. } )  u.  ( ( ( ( M  +  1 )  +  1 ) ... N )  X. 
{ 0 } ) ) )
8651nn0red 10927 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  M  e.  RR )
8786ltp1d 10538 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  M  <  ( M  +  1 ) )
8853nnred 10625 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  ( M  +  1 )  e.  RR )
8986, 88ltnled 9783 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( M  <  ( M  +  1 )  <->  -.  ( M  +  1 )  <_  M )
)
9087, 89mpbid 213 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  -.  ( M  + 
1 )  <_  M
)
91 elfzle2 11804 . . . . . . . . . . . . . . . . . . 19  |-  ( ( M  +  1 )  e.  ( 1 ... M )  ->  ( M  +  1 )  <_  M )
9290, 91nsyl 124 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  -.  ( M  + 
1 )  e.  ( 1 ... M ) )
93 disjsn 4057 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( 1 ... M
)  i^i  { ( M  +  1 ) } )  =  (/)  <->  -.  ( M  +  1
)  e.  ( 1 ... M ) )
9492, 93sylibr 215 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 1 ... M )  i^i  {
( M  +  1 ) } )  =  (/) )
95 eqid 2422 . . . . . . . . . . . . . . . . . . 19  |-  { <. ( M  +  1 ) ,  0 >. }  =  { <. ( M  + 
1 ) ,  0
>. }
9677, 8fsn 6073 . . . . . . . . . . . . . . . . . . 19  |-  ( {
<. ( M  +  1 ) ,  0 >. } : { ( M  +  1 ) } --> { 0 }  <->  { <. ( M  +  1 ) ,  0 >. }  =  { <. ( M  + 
1 ) ,  0
>. } )
9795, 96mpbir 212 . . . . . . . . . . . . . . . . . 18  |-  { <. ( M  +  1 ) ,  0 >. } : { ( M  + 
1 ) } --> { 0 }
98 fun 5760 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( T : ( 1 ... M ) --> ( 0..^ K )  /\  { <. ( M  +  1 ) ,  0 >. } : { ( M  + 
1 ) } --> { 0 } )  /\  (
( 1 ... M
)  i^i  { ( M  +  1 ) } )  =  (/) )  ->  ( T  u.  {
<. ( M  +  1 ) ,  0 >. } ) : ( ( 1 ... M
)  u.  { ( M  +  1 ) } ) --> ( ( 0..^ K )  u. 
{ 0 } ) )
9997, 98mpanl2 685 . . . . . . . . . . . . . . . . 17  |-  ( ( T : ( 1 ... M ) --> ( 0..^ K )  /\  ( ( 1 ... M )  i^i  {
( M  +  1 ) } )  =  (/) )  ->  ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) : ( ( 1 ... M )  u. 
{ ( M  + 
1 ) } ) --> ( ( 0..^ K )  u.  { 0 } ) )
1001, 94, 99syl2anc 665 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) : ( ( 1 ... M
)  u.  { ( M  +  1 ) } ) --> ( ( 0..^ K )  u. 
{ 0 } ) )
101 1z 10968 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  ZZ
102 nn0uz 11194 . . . . . . . . . . . . . . . . . . . . 21  |-  NN0  =  ( ZZ>= `  0 )
103 1m1e0 10679 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1  -  1 )  =  0
104103fveq2i 5881 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ZZ>= `  ( 1  -  1 ) )  =  (
ZZ>= `  0 )
105102, 104eqtr4i 2454 . . . . . . . . . . . . . . . . . . . 20  |-  NN0  =  ( ZZ>= `  ( 1  -  1 ) )
10651, 105syl6eleq 2520 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  M  e.  ( ZZ>= `  ( 1  -  1 ) ) )
107 fzsuc2 11854 . . . . . . . . . . . . . . . . . . 19  |-  ( ( 1  e.  ZZ  /\  M  e.  ( ZZ>= `  ( 1  -  1 ) ) )  -> 
( 1 ... ( M  +  1 ) )  =  ( ( 1 ... M )  u.  { ( M  +  1 ) } ) )
108101, 106, 107sylancr 667 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( 1 ... ( M  +  1 ) )  =  ( ( 1 ... M )  u.  { ( M  +  1 ) } ) )
109108eqcomd 2430 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 1 ... M )  u.  {
( M  +  1 ) } )  =  ( 1 ... ( M  +  1 ) ) )
110 poimirlem4.1 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  K  e.  NN )
111 lbfzo0 11956 . . . . . . . . . . . . . . . . . . . 20  |-  ( 0  e.  ( 0..^ K )  <->  K  e.  NN )
112110, 111sylibr 215 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  0  e.  ( 0..^ K ) )
113112snssd 4142 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  { 0 }  C_  ( 0..^ K ) )
114 ssequn2 3639 . . . . . . . . . . . . . . . . . 18  |-  ( { 0 }  C_  (
0..^ K )  <->  ( (
0..^ K )  u. 
{ 0 } )  =  ( 0..^ K ) )
115113, 114sylib 199 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( 0..^ K )  u.  { 0 } )  =  ( 0..^ K ) )
116109, 115feq23d 5738 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( T  u.  {
<. ( M  +  1 ) ,  0 >. } ) : ( ( 1 ... M
)  u.  { ( M  +  1 ) } ) --> ( ( 0..^ K )  u. 
{ 0 } )  <-> 
( T  u.  { <. ( M  +  1 ) ,  0 >. } ) : ( 1 ... ( M  +  1 ) ) --> ( 0..^ K ) ) )
117100, 116mpbid 213 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) : ( 1 ... ( M  +  1 ) ) --> ( 0..^ K ) )
118 ffn 5743 . . . . . . . . . . . . . . 15  |-  ( ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) : ( 1 ... ( M  +  1 ) ) --> ( 0..^ K )  ->  ( T  u.  { <. ( M  +  1 ) ,  0 >. } )  Fn  ( 1 ... ( M  +  1 ) ) )
119117, 118syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( T  u.  { <. ( M  +  1 ) ,  0 >. } )  Fn  (
1 ... ( M  + 
1 ) ) )
120119adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( T  u.  { <. ( M  +  1 ) ,  0 >. } )  Fn  ( 1 ... ( M  +  1 ) ) )
121 fnconstg 5785 . . . . . . . . . . . . . . . . 17  |-  ( 1  e.  _V  ->  (
( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  Fn  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) ) )
1225, 121ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  Fn  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )
123 fnconstg 5785 . . . . . . . . . . . . . . . . 17  |-  ( 0  e.  _V  ->  (
( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } )  Fn  (
( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) ) )
1248, 123ax-mp 5 . . . . . . . . . . . . . . . 16  |-  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } )  Fn  (
( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )
125122, 124pm3.2i 456 . . . . . . . . . . . . . . 15  |-  ( ( ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  Fn  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  /\  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } )  Fn  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) ) )
12677, 77f1osn 5865 . . . . . . . . . . . . . . . . . . 19  |-  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } : { ( M  + 
1 ) } -1-1-onto-> { ( M  + 
1 ) }
127 f1oun 5847 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( U : ( 1 ... M ) -1-1-onto-> ( 1 ... M )  /\  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } : { ( M  + 
1 ) } -1-1-onto-> { ( M  + 
1 ) } )  /\  ( ( ( 1 ... M )  i^i  { ( M  +  1 ) } )  =  (/)  /\  (
( 1 ... M
)  i^i  { ( M  +  1 ) } )  =  (/) ) )  ->  ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) : ( ( 1 ... M )  u. 
{ ( M  + 
1 ) } ) -1-1-onto-> ( ( 1 ... M
)  u.  { ( M  +  1 ) } ) )
128126, 127mpanl2 685 . . . . . . . . . . . . . . . . . 18  |-  ( ( U : ( 1 ... M ) -1-1-onto-> ( 1 ... M )  /\  ( ( ( 1 ... M )  i^i 
{ ( M  + 
1 ) } )  =  (/)  /\  (
( 1 ... M
)  i^i  { ( M  +  1 ) } )  =  (/) ) )  ->  ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) : ( ( 1 ... M )  u. 
{ ( M  + 
1 ) } ) -1-1-onto-> ( ( 1 ... M
)  u.  { ( M  +  1 ) } ) )
12912, 94, 94, 128syl12anc 1262 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) : ( ( 1 ... M
)  u.  { ( M  +  1 ) } ) -1-1-onto-> ( ( 1 ... M )  u.  {
( M  +  1 ) } ) )
130 dff1o3 5834 . . . . . . . . . . . . . . . . . 18  |-  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) : ( ( 1 ... M )  u. 
{ ( M  + 
1 ) } ) -1-1-onto-> ( ( 1 ... M
)  u.  { ( M  +  1 ) } )  <->  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) : ( ( 1 ... M )  u. 
{ ( M  + 
1 ) } )
-onto-> ( ( 1 ... M )  u.  {
( M  +  1 ) } )  /\  Fun  `' ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) ) )
131130simprbi 465 . . . . . . . . . . . . . . . . 17  |-  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) : ( ( 1 ... M )  u. 
{ ( M  + 
1 ) } ) -1-1-onto-> ( ( 1 ... M
)  u.  { ( M  +  1 ) } )  ->  Fun  `' ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) )
132 imain 5674 . . . . . . . . . . . . . . . . 17  |-  ( Fun  `' ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } )  ->  (
( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... ( M  + 
1 ) ) ) )  =  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  i^i  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) ) ) )
133129, 131, 1323syl 18 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... ( M  + 
1 ) ) ) )  =  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  i^i  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) ) ) )
134 fzdisj 11827 . . . . . . . . . . . . . . . . . . 19  |-  ( j  <  ( j  +  1 )  ->  (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... ( M  + 
1 ) ) )  =  (/) )
13519, 134syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... M )  ->  (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... ( M  + 
1 ) ) )  =  (/) )
136135imaeq2d 5184 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... M )  ->  (
( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... ( M  + 
1 ) ) ) )  =  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" (/) ) )
137 ima0 5199 . . . . . . . . . . . . . . . . 17  |-  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" (/) )  =  (/)
138136, 137syl6eq 2479 . . . . . . . . . . . . . . . 16  |-  ( j  e.  ( 0 ... M )  ->  (
( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... ( M  + 
1 ) ) ) )  =  (/) )
139133, 138sylan9req 2484 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  i^i  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) ) )  =  (/) )
140 fnun 5697 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  Fn  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  /\  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } )  Fn  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) ) )  /\  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  i^i  ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) ) )  =  (/) )  ->  ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) )  Fn  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  u.  ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) ) ) )
141125, 139, 140sylancr 667 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) )  Fn  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  u.  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) ) ) )
142 f1ofo 5835 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) : ( ( 1 ... M )  u. 
{ ( M  + 
1 ) } ) -1-1-onto-> ( ( 1 ... M
)  u.  { ( M  +  1 ) } )  ->  ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) : ( ( 1 ... M )  u. 
{ ( M  + 
1 ) } )
-onto-> ( ( 1 ... M )  u.  {
( M  +  1 ) } ) )
143 foima 5812 . . . . . . . . . . . . . . . . . . 19  |-  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } ) : ( ( 1 ... M )  u. 
{ ( M  + 
1 ) } )
-onto-> ( ( 1 ... M )  u.  {
( M  +  1 ) } )  -> 
( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( 1 ... M
)  u.  { ( M  +  1 ) } ) )  =  ( ( 1 ... M )  u.  {
( M  +  1 ) } ) )
144129, 142, 1433syl 18 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( 1 ... M
)  u.  { ( M  +  1 ) } ) )  =  ( ( 1 ... M )  u.  {
( M  +  1 ) } ) )
145108imaeq2d 5184 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... ( M  + 
1 ) ) )  =  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( 1 ... M )  u. 
{ ( M  + 
1 ) } ) ) )
146144, 145, 1083eqtr4d 2473 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... ( M  + 
1 ) ) )  =  ( 1 ... ( M  +  1 ) ) )
147 peano2uz 11213 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  e.  ( ZZ>= `  j
)  ->  ( M  +  1 )  e.  ( ZZ>= `  j )
)
14833, 147syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... M )  ->  ( M  +  1 )  e.  ( ZZ>= `  j
) )
149 fzsplit2 11825 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( j  +  1 )  e.  ( ZZ>= ` 
1 )  /\  ( M  +  1 )  e.  ( ZZ>= `  j
) )  ->  (
1 ... ( M  + 
1 ) )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... ( M  +  1 ) ) ) )
15032, 148, 149syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... M )  ->  (
1 ... ( M  + 
1 ) )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... ( M  +  1 ) ) ) )
151150imaeq2d 5184 . . . . . . . . . . . . . . . . 17  |-  ( j  e.  ( 0 ... M )  ->  (
( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... ( M  + 
1 ) ) )  =  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( 1 ... j )  u.  ( ( j  +  1 ) ... ( M  +  1 ) ) ) ) )
152146, 151sylan9req 2484 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
1 ... ( M  + 
1 ) )  =  ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( 1 ... j
)  u.  ( ( j  +  1 ) ... ( M  + 
1 ) ) ) ) )
153 imaundi 5264 . . . . . . . . . . . . . . . 16  |-  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( 1 ... j )  u.  ( ( j  +  1 ) ... ( M  +  1 ) ) ) )  =  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  u.  ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) ) )
154152, 153syl6eq 2479 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
1 ... ( M  + 
1 ) )  =  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  u.  ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) ) ) )
155154fneq2d 5682 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) )  Fn  ( 1 ... ( M  + 
1 ) )  <->  ( (
( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) )  Fn  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  u.  ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) ) ) ) )
156141, 155mpbird 235 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) )  Fn  ( 1 ... ( M  + 
1 ) ) )
157 ovex 6330 . . . . . . . . . . . . . 14  |-  ( 1 ... ( M  + 
1 ) )  e. 
_V
158157a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
1 ... ( M  + 
1 ) )  e. 
_V )
159 inidm 3671 . . . . . . . . . . . . 13  |-  ( ( 1 ... ( M  +  1 ) )  i^i  ( 1 ... ( M  +  1 ) ) )  =  ( 1 ... ( M  +  1 ) )
160 eqidd 2423 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  n  e.  ( 1 ... ( M  +  1 ) ) )  ->  (
( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `  n
)  =  ( ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 n ) )
161 eqidd 2423 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  n  e.  ( 1 ... ( M  +  1 ) ) )  ->  (
( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) `  n )  =  ( ( ( ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) ) `  n ) )
162120, 156, 158, 158, 159, 160, 161offval 6549 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( T  u.  { <. ( M  +  1 ) ,  0 >. } )  oF  +  ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) ) )  =  ( n  e.  ( 1 ... ( M  +  1 ) )  |->  ( ( ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 n )  +  ( ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) ) `  n ) ) ) )
16377a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( M  +  1 )  e.  _V )
1648a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  0  e.  _V )
165109adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( 1 ... M
)  u.  { ( M  +  1 ) } )  =  ( 1 ... ( M  +  1 ) ) )
166 fveq2 5878 . . . . . . . . . . . . . . . . 17  |-  ( n  =  ( M  + 
1 )  ->  (
( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `  n
)  =  ( ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 ( M  + 
1 ) ) )
16777snid 4024 . . . . . . . . . . . . . . . . . . . 20  |-  ( M  +  1 )  e. 
{ ( M  + 
1 ) }
16877, 8fnsn 5651 . . . . . . . . . . . . . . . . . . . . 21  |-  { <. ( M  +  1 ) ,  0 >. }  Fn  { ( M  +  1 ) }
169 fvun2 5950 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( T  Fn  ( 1 ... M )  /\  {
<. ( M  +  1 ) ,  0 >. }  Fn  { ( M  +  1 ) }  /\  ( ( ( 1 ... M
)  i^i  { ( M  +  1 ) } )  =  (/)  /\  ( M  +  1 )  e.  { ( M  +  1 ) } ) )  -> 
( ( T  u.  {
<. ( M  +  1 ) ,  0 >. } ) `  ( M  +  1 ) )  =  ( {
<. ( M  +  1 ) ,  0 >. } `  ( M  +  1 ) ) )
170168, 169mp3an2 1348 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T  Fn  ( 1 ... M )  /\  ( ( ( 1 ... M )  i^i 
{ ( M  + 
1 ) } )  =  (/)  /\  ( M  +  1 )  e.  { ( M  +  1 ) } ) )  ->  (
( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `  ( M  +  1 ) )  =  ( {
<. ( M  +  1 ) ,  0 >. } `  ( M  +  1 ) ) )
171167, 170mpanr2 688 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T  Fn  ( 1 ... M )  /\  ( ( 1 ... M )  i^i  {
( M  +  1 ) } )  =  (/) )  ->  ( ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 ( M  + 
1 ) )  =  ( { <. ( M  +  1 ) ,  0 >. } `  ( M  +  1
) ) )
1723, 94, 171syl2anc 665 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( T  u.  {
<. ( M  +  1 ) ,  0 >. } ) `  ( M  +  1 ) )  =  ( {
<. ( M  +  1 ) ,  0 >. } `  ( M  +  1 ) ) )
17377, 8fvsn 6109 . . . . . . . . . . . . . . . . . 18  |-  ( {
<. ( M  +  1 ) ,  0 >. } `  ( M  +  1 ) )  =  0
174172, 173syl6eq 2479 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( T  u.  {
<. ( M  +  1 ) ,  0 >. } ) `  ( M  +  1 ) )  =  0 )
175166, 174sylan9eqr 2485 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  =  ( M  +  1
) )  ->  (
( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `  n
)  =  0 )
176175adantlr 719 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  n  =  ( M  + 
1 ) )  -> 
( ( T  u.  {
<. ( M  +  1 ) ,  0 >. } ) `  n
)  =  0 )
177 fveq2 5878 . . . . . . . . . . . . . . . 16  |-  ( n  =  ( M  + 
1 )  ->  (
( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) `  n )  =  ( ( ( ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) ) `  ( M  +  1
) ) )
178 imadmrn 5194 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( { ( M  + 
1 ) }  X.  { ( M  + 
1 ) } )
" dom  ( {
( M  +  1 ) }  X.  {
( M  +  1 ) } ) )  =  ran  ( { ( M  +  1 ) }  X.  {
( M  +  1 ) } )
17977, 77xpsn 6078 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( { ( M  +  1 ) }  X.  {
( M  +  1 ) } )  =  { <. ( M  + 
1 ) ,  ( M  +  1 )
>. }
180179imaeq1i 5181 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( { ( M  + 
1 ) }  X.  { ( M  + 
1 ) } )
" dom  ( {
( M  +  1 ) }  X.  {
( M  +  1 ) } ) )  =  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } " dom  ( { ( M  +  1 ) }  X.  { ( M  +  1 ) } ) )
181 dmxpid 5070 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  dom  ( { ( M  + 
1 ) }  X.  { ( M  + 
1 ) } )  =  { ( M  +  1 ) }
182181imaeq2i 5182 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } " dom  ( { ( M  +  1 ) }  X.  {
( M  +  1 ) } ) )  =  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } " { ( M  + 
1 ) } )
183180, 182eqtri 2451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( { ( M  + 
1 ) }  X.  { ( M  + 
1 ) } )
" dom  ( {
( M  +  1 ) }  X.  {
( M  +  1 ) } ) )  =  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } " { ( M  + 
1 ) } )
184 rnxpid 5286 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ran  ( { ( M  + 
1 ) }  X.  { ( M  + 
1 ) } )  =  { ( M  +  1 ) }
185178, 183, 1843eqtr3ri 2460 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { ( M  +  1 ) }  =  ( {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } " { ( M  +  1 ) } )
186 eluzp1p1 11185 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( M  e.  ( ZZ>= `  j
)  ->  ( M  +  1 )  e.  ( ZZ>= `  ( j  +  1 ) ) )
187 eluzfz2 11808 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( M  +  1 )  e.  ( ZZ>= `  (
j  +  1 ) )  ->  ( M  +  1 )  e.  ( ( j  +  1 ) ... ( M  +  1 ) ) )
18833, 186, 1873syl 18 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  e.  ( 0 ... M )  ->  ( M  +  1 )  e.  ( ( j  +  1 ) ... ( M  +  1 ) ) )
189188snssd 4142 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  e.  ( 0 ... M )  ->  { ( M  +  1 ) }  C_  ( (
j  +  1 ) ... ( M  + 
1 ) ) )
190 imass2 5220 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( { ( M  +  1 ) }  C_  (
( j  +  1 ) ... ( M  +  1 ) )  ->  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } " { ( M  + 
1 ) } ) 
C_  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( ( j  +  1 ) ... ( M  +  1 ) ) ) )
191189, 190syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  e.  ( 0 ... M )  ->  ( { <. ( M  + 
1 ) ,  ( M  +  1 )
>. } " { ( M  +  1 ) } )  C_  ( { <. ( M  + 
1 ) ,  ( M  +  1 )
>. } " ( ( j  +  1 ) ... ( M  + 
1 ) ) ) )
192185, 191syl5eqss 3508 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  e.  ( 0 ... M )  ->  { ( M  +  1 ) }  C_  ( { <. ( M  +  1 ) ,  ( M  +  1 ) >. } " ( ( j  +  1 ) ... ( M  +  1 ) ) ) )
193 ssel 3458 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( { ( M  +  1 ) }  C_  ( { <. ( M  + 
1 ) ,  ( M  +  1 )
>. } " ( ( j  +  1 ) ... ( M  + 
1 ) ) )  ->  ( ( M  +  1 )  e. 
{ ( M  + 
1 ) }  ->  ( M  +  1 )  e.  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( ( j  +  1 ) ... ( M  +  1 ) ) ) ) )
194192, 167, 193mpisyl 22 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  e.  ( 0 ... M )  ->  ( M  +  1 )  e.  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( ( j  +  1 ) ... ( M  +  1 ) ) ) )
195 elun2 3634 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( M  +  1 )  e.  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( ( j  +  1 ) ... ( M  +  1 ) ) )  ->  ( M  +  1 )  e.  ( ( U
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  u.  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( ( j  +  1 ) ... ( M  +  1 ) ) ) ) )
196194, 195syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  e.  ( 0 ... M )  ->  ( M  +  1 )  e.  ( ( U
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  u.  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( ( j  +  1 ) ... ( M  +  1 ) ) ) ) )
197 imaundir 5265 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  =  ( ( U "
( ( j  +  1 ) ... ( M  +  1 ) ) )  u.  ( { <. ( M  + 
1 ) ,  ( M  +  1 )
>. } " ( ( j  +  1 ) ... ( M  + 
1 ) ) ) )
198196, 197syl6eleqr 2521 . . . . . . . . . . . . . . . . . . 19  |-  ( j  e.  ( 0 ... M )  ->  ( M  +  1 )  e.  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) ) )
199198adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  ( M  +  1 )  e.  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) ) )
200 fvun2 5950 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  Fn  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  /\  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } )  Fn  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  /\  ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  i^i  ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) ) )  =  (/)  /\  ( M  +  1 )  e.  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) ) ) )  ->  ( (
( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) `  ( M  +  1 ) )  =  ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) `  ( M  +  1 ) ) )
201122, 124, 200mp3an12 1350 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  i^i  ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) ) )  =  (/)  /\  ( M  +  1 )  e.  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) ) )  ->  ( ( ( ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) ) `  ( M  +  1
) )  =  ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) `
 ( M  + 
1 ) ) )
202139, 199, 201syl2anc 665 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) `  ( M  +  1 ) )  =  ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) `  ( M  +  1 ) ) )
2038fvconst2 6132 . . . . . . . . . . . . . . . . . . 19  |-  ( ( M  +  1 )  e.  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  -> 
( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) `
 ( M  + 
1 ) )  =  0 )
204198, 203syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( j  e.  ( 0 ... M )  ->  (
( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) `
 ( M  + 
1 ) )  =  0 )
205204adantl 467 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) `
 ( M  + 
1 ) )  =  0 )
206202, 205eqtrd 2463 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) `  ( M  +  1 ) )  =  0 )
207177, 206sylan9eqr 2485 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  n  =  ( M  + 
1 ) )  -> 
( ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) ) `  n )  =  0 )
208176, 207oveq12d 6320 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  n  =  ( M  + 
1 ) )  -> 
( ( ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 n )  +  ( ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) ) `  n ) )  =  ( 0  +  0 ) )
209 00id 9809 . . . . . . . . . . . . . 14  |-  ( 0  +  0 )  =  0
210208, 209syl6eq 2479 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  n  =  ( M  + 
1 ) )  -> 
( ( ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 n )  +  ( ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) ) `  n ) )  =  0 )
211163, 164, 165, 210fmptapd 6100 . . . . . . . . . . . 12  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( n  e.  ( 1 ... M ) 
|->  ( ( ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 n )  +  ( ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) ) `  n ) ) )  u.  { <. ( M  +  1 ) ,  0 >. } )  =  ( n  e.  ( 1 ... ( M  +  1 ) )  |->  ( ( ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 n )  +  ( ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) ) `  n ) ) ) )
2123, 94jca 534 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( T  Fn  (
1 ... M )  /\  ( ( 1 ... M )  i^i  {
( M  +  1 ) } )  =  (/) ) )
213 fvun1 5949 . . . . . . . . . . . . . . . . . . 19  |-  ( ( T  Fn  ( 1 ... M )  /\  {
<. ( M  +  1 ) ,  0 >. }  Fn  { ( M  +  1 ) }  /\  ( ( ( 1 ... M
)  i^i  { ( M  +  1 ) } )  =  (/)  /\  n  e.  ( 1 ... M ) ) )  ->  ( ( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `
 n )  =  ( T `  n
) )
214168, 213mp3an2 1348 . . . . . . . . . . . . . . . . . 18  |-  ( ( T  Fn  ( 1 ... M )  /\  ( ( ( 1 ... M )  i^i 
{ ( M  + 
1 ) } )  =  (/)  /\  n  e.  ( 1 ... M
) ) )  -> 
( ( T  u.  {
<. ( M  +  1 ) ,  0 >. } ) `  n
)  =  ( T `
 n ) )
215214anassrs 652 . . . . . . . . . . . . . . . . 17  |-  ( ( ( T  Fn  (
1 ... M )  /\  ( ( 1 ... M )  i^i  {
( M  +  1 ) } )  =  (/) )  /\  n  e.  ( 1 ... M
) )  ->  (
( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `  n
)  =  ( T `
 n ) )
216212, 215sylan 473 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  n  e.  ( 1 ... M
) )  ->  (
( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `  n
)  =  ( T `
 n ) )
217216adantlr 719 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  j  e.  ( 0 ... M
) )  /\  n  e.  ( 1 ... M
) )  ->  (
( T  u.  { <. ( M  +  1 ) ,  0 >. } ) `  n
)  =  ( T `
 n ) )
218 fvres 5892 . . . . . . . . . . . . . . . . 17  |-  ( n  e.  ( 1 ... M )  ->  (
( ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } ) )  |`  ( 1 ... M
) ) `  n
)  =  ( ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) `  n ) )
219218eqcomd 2430 . . . . . . . . . . . . . . . 16  |-  ( n  e.  ( 1 ... M )  ->  (
( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) ) `  n )  =  ( ( ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) )  |`  ( 1 ... M ) ) `
 n ) )
220 resundir 5135 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( ( j  +  1 ) ... ( M  +  1 ) ) )  X. 
{ 0 } ) )  |`  ( 1 ... M ) )  =  ( ( ( ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  |`  ( 1 ... M ) )  u.  ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
( j  +  1 ) ... ( M  +  1 ) ) )  X.  { 0 } )  |`  (
1 ... M ) ) )
221 relxp 4958 . . . . . . . . . . . . . . . . . . . . . . 23  |-  Rel  (
( U " (
1 ... j ) )  X.  { 1 } )
222 dmxpss 5284 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  dom  (
( U " (
1 ... j ) )  X.  { 1 } )  C_  ( U " ( 1 ... j
) )
223 imassrn 5195 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( U
" ( 1 ... j ) )  C_  ran  U
224222, 223sstri 3473 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  dom  (
( U " (
1 ... j ) )  X.  { 1 } )  C_  ran  U
225 f1of 5828 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( U : ( 1 ... M ) -1-1-onto-> ( 1 ... M
)  ->  U :
( 1 ... M
) --> ( 1 ... M ) )
226 frn 5749 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( U : ( 1 ... M ) --> ( 1 ... M )  ->  ran  U  C_  ( 1 ... M ) )
22712, 225, 2263syl 18 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ran  U  C_  (
1 ... M ) )
228224, 227syl5ss 3475 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  dom  ( ( U
" ( 1 ... j ) )  X. 
{ 1 } ) 
C_  ( 1 ... M ) )
229 relssres 5158 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( Rel  ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  /\  dom  ( ( U " ( 1 ... j ) )  X.  { 1 } )  C_  ( 1 ... M ) )  ->  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  |`  ( 1 ... M ) )  =  ( ( U
" ( 1 ... j ) )  X. 
{ 1 } ) )
230221, 228, 229sylancr 667 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  |`  ( 1 ... M
) )  =  ( ( U " (
1 ... j ) )  X.  { 1 } ) )
231230adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( U "
( 1 ... j
) )  X.  {
1 } )  |`  ( 1 ... M
) )  =  ( ( U " (
1 ... j ) )  X.  { 1 } ) )
232 imassrn 5195 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } " ( 1 ... j ) )  C_  ran  { <. ( M  + 
1 ) ,  ( M  +  1 )
>. }
23377rnsnop 5333 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ran  { <. ( M  +  1 ) ,  ( M  +  1 ) >. }  =  { ( M  +  1 ) }
234232, 233sseqtri 3496 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } " ( 1 ... j ) )  C_  { ( M  +  1 ) }
235 ssrin 3687 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( { <. ( M  + 
1 ) ,  ( M  +  1 )
>. } " ( 1 ... j ) ) 
C_  { ( M  +  1 ) }  ->  ( ( {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } " ( 1 ... j ) )  i^i  ( 1 ... M
) )  C_  ( { ( M  + 
1 ) }  i^i  ( 1 ... M
) ) )
236234, 235ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( { <. ( M  + 
1 ) ,  ( M  +  1 )
>. } " ( 1 ... j ) )  i^i  ( 1 ... M ) )  C_  ( { ( M  + 
1 ) }  i^i  ( 1 ... M
) )
237 incom 3655 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( { ( M  +  1 ) }  i^i  (
1 ... M ) )  =  ( ( 1 ... M )  i^i 
{ ( M  + 
1 ) } )
238237, 94syl5eq 2475 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  ( { ( M  +  1 ) }  i^i  ( 1 ... M ) )  =  (/) )
239236, 238syl5sseq 3512 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) )  i^i  (
1 ... M ) ) 
C_  (/) )
240 ss0 3793 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) )  i^i  (
1 ... M ) ) 
C_  (/)  ->  ( ( { <. ( M  + 
1 ) ,  ( M  +  1 )
>. } " ( 1 ... j ) )  i^i  ( 1 ... M ) )  =  (/) )
241239, 240syl 17 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) )  i^i  (
1 ... M ) )  =  (/) )
242 fnconstg 5785 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1  e.  _V  ->  (
( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) )  X.  {
1 } )  Fn  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) ) )
243 fnresdisj 5701 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) )  X.  {
1 } )  Fn  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) )  ->  (
( ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) )  i^i  (
1 ... M ) )  =  (/)  <->  ( ( ( { <. ( M  + 
1 ) ,  ( M  +  1 )
>. } " ( 1 ... j ) )  X.  { 1 } )  |`  ( 1 ... M ) )  =  (/) ) )
2445, 242, 243mp2b 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) )  i^i  (
1 ... M ) )  =  (/)  <->  ( ( ( { <. ( M  + 
1 ) ,  ( M  +  1 )
>. } " ( 1 ... j ) )  X.  { 1 } )  |`  ( 1 ... M ) )  =  (/) )
245241, 244sylib 199 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ph  ->  ( ( ( {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } " ( 1 ... j ) )  X. 
{ 1 } )  |`  ( 1 ... M
) )  =  (/) )
246245adantr 466 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) )  X.  {
1 } )  |`  ( 1 ... M
) )  =  (/) )
247231, 246uneq12d 3621 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  |`  ( 1 ... M
) )  u.  (
( ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) )  X.  {
1 } )  |`  ( 1 ... M
) ) )  =  ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  u.  (/) ) )
248 imaundir 5265 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  =  ( ( U "
( 1 ... j
) )  u.  ( { <. ( M  + 
1 ) ,  ( M  +  1 )
>. } " ( 1 ... j ) ) )
249248xpeq1i 4870 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  =  ( ( ( U " (
1 ... j ) )  u.  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) ) )  X. 
{ 1 } )
250 xpundir 4904 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( U " (
1 ... j ) )  u.  ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) ) )  X. 
{ 1 } )  =  ( ( ( U " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( { <. ( M  + 
1 ) ,  ( M  +  1 )
>. } " ( 1 ... j ) )  X.  { 1 } ) )
251249, 250eqtri 2451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  =  ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( { <. ( M  + 
1 ) ,  ( M  +  1 )
>. } " ( 1 ... j ) )  X.  { 1 } ) )
252251reseq1i 5117 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( U  u.  {
<. ( M  +  1 ) ,  ( M  +  1 ) >. } ) " (
1 ... j ) )  X.  { 1 } )  |`  ( 1 ... M ) )  =  ( ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  ( ( { <. ( M  + 
1 ) ,  ( M  +  1 )
>. } " ( 1 ... j ) )  X.  { 1 } ) )  |`  (
1 ... M ) )
253 resundir 5135 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  u.  ( ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) )  X.  {
1 } ) )  |`  ( 1 ... M
) )  =  ( ( ( ( U
" ( 1 ... j ) )  X. 
{ 1 } )  |`  ( 1 ... M
) )  u.  (
( ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) )  X.  {
1 } )  |`  ( 1 ... M
) ) )
254252, 253eqtr2i 2452 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( U "
( 1 ... j
) )  X.  {
1 } )  |`  ( 1 ... M
) )  u.  (
( ( { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } "
( 1 ... j
) )  X.  {
1 } )  |`  ( 1 ... M
) ) )  =  ( ( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  |`  ( 1 ... M
) )
255 un0 3787 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( U " (
1 ... j ) )  X.  { 1 } )  u.  (/) )  =  ( ( U "
( 1 ... j
) )  X.  {
1 } )
256247, 254, 2553eqtr3g 2486 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  j  e.  ( 0 ... M
) )  ->  (
( ( ( U  u.  { <. ( M  +  1 ) ,  ( M  + 
1 ) >. } )
" ( 1 ... j ) )  X. 
{ 1 } )  |`  ( 1 ... M
) )  =  ( ( U " (
1 ... j ) )  X.  { 1 } ) )
257 f1odm 5832 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( U : ( 1 ... M ) -1-1-onto-> ( 1 ... M
)  ->  dom  U  =  ( 1 ... M
) )
25812, 257syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  dom  U  =  ( 1 ... M ) )
259258ineq2d 3664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( ( ( j  +  1 ) ... ( M  +  1 ) )  i^i  dom  U )  =  ( ( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( 1 ... M ) ) )
260259reseq2d 5121 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( U  |`  (
( ( j  +  1 ) ... ( M  +  1 ) )  i^i  dom  U
) )  =  ( U  |`  ( (
( j  +  1 ) ... ( M  +  1 ) )  i^i  ( 1 ... M ) ) ) )
261 f1orel 5831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( U : ( 1 ... M ) -1-1-onto-> ( 1 ... M
)  ->  Rel  U )
262 resindm 5165 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( Rel 
U  ->  ( U  |`  ( ( ( j  +  1 ) ... ( M  +  1 ) )  i^i  dom  U ) )  =  ( U  |`  ( (
j  +  1 ) ... ( M  + 
1 ) ) ) )
26312, 261, 2623syl 18 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ph  ->  ( U  |`  (
( ( j  +  1 ) ... ( M  +  1 ) )  i^i  dom  U
) )  =  ( U  |`  ( (
j  +  1 ) ... ( M  + 
1 ) ) ) )
264260, 263eqtr3d 2465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ph  ->  ( U  |`  (
( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( 1 ... M ) ) )  =  ( U  |`  ( ( j  +  1 ) ... ( M  +  1 ) ) ) )
26535ineq2d 3664 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  e.  ( 0 ... M )  ->  (
( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( 1 ... M ) )  =  ( ( ( j  +  1 ) ... ( M  + 
1 ) )  i^i  ( ( 1 ... j )  u.  (
( j  +  1 ) ... M ) ) ) )
266 fzssp1 11842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( j  +  1 ) ... M )  C_  ( ( j  +  1 ) ... ( M  +  1 ) )
267 dfss1 3667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( j  +  1 ) ... M ) 
C_  ( ( j  +  1 ) ... ( M  +  1 ) )  <->  ( (
( j  +  1 ) ... ( M  +  1 ) )  i^i  ( ( j  +  1 ) ... M ) )  =  ( ( j  +  1 ) ... M
) )
268266, 267mpbi 211 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( ( j  +  1 ) ... M ) )  =  ( ( j  +  1 ) ... M
)
269268a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  e.  ( 0 ... M )  ->  (
( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( ( j  +  1 ) ... M ) )  =  ( ( j  +  1 ) ... M ) )
270 incom 3655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( 1 ... j ) )  =  ( ( 1 ... j )  i^i  (
( j  +  1 ) ... ( M  +  1 ) ) )
271270, 135syl5eq 2475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  e.  ( 0 ... M )  ->  (
( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( 1 ... j ) )  =  (/) )
272269, 271uneq12d 3621 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  e.  ( 0 ... M )  ->  (
( ( ( j  +  1 ) ... ( M  +  1 ) )  i^i  (
( j  +  1 ) ... M ) )  u.  ( ( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( 1 ... j ) ) )  =  ( ( ( j  +  1 ) ... M )  u.  (/) ) )
273 uncom 3610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( ( j  +  1 ) ... M ) )  u.  ( ( ( j  +  1 ) ... ( M  + 
1 ) )  i^i  ( 1 ... j
) ) )  =  ( ( ( ( j  +  1 ) ... ( M  + 
1 ) )  i^i  ( 1 ... j
) )  u.  (
( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( ( j  +  1 ) ... M ) ) )
274 indi 3719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( ( 1 ... j )  u.  ( ( j  +  1 ) ... M
) ) )  =  ( ( ( ( j  +  1 ) ... ( M  + 
1 ) )  i^i  ( 1 ... j
) )  u.  (
( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( ( j  +  1 ) ... M ) ) )
275273, 274eqtr4i 2454 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( ( j  +  1 ) ... M ) )  u.  ( ( ( j  +  1 ) ... ( M  + 
1 ) )  i^i  ( 1 ... j
) ) )  =  ( ( ( j  +  1 ) ... ( M  +  1 ) )  i^i  (
( 1 ... j
)  u.  ( ( j  +  1 ) ... M ) ) )
276 un0 3787 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( j  +  1 ) ... M )  u.  (/) )  =  ( ( j  +  1 ) ... M )
277272, 275, 2763eqtr3g 2486 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  e.  ( 0 ... M )  ->  (
( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( ( 1 ... j )  u.  ( ( j  +  1 ) ... M ) ) )  =  ( ( j  +  1 ) ... M ) )
278265, 277eqtrd 2463 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  e.  ( 0 ... M )  ->  (
( ( j  +  1 ) ... ( M  +  1 ) )  i^i  ( 1 ... M ) )  =  ( ( j  +  1 ) ... M ) )
279278reseq2d 5121 . . . . . . . . . . . . . . . . . . . . . . . . . . 27