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

Theorem poimirlem25 31879
Description: Lemma for poimir 31887 stating that for a given simplex such that no vertex maps to  N, the number of admissible faces is even. (Contributed by Brendan Leahy, 21-Aug-2020.)
Hypotheses
Ref Expression
poimir.0  |-  ( ph  ->  N  e.  NN )
poimirlem28.1  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  ->  B  =  C )
poimirlem28.2  |-  ( (
ph  /\  p :
( 1 ... N
) --> ( 0 ... K ) )  ->  B  e.  ( 0 ... N ) )
poimirlem25.3  |-  ( ph  ->  T : ( 1 ... N ) --> ( 0..^ K ) )
poimirlem25.4  |-  ( ph  ->  U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
poimirlem25.5  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  N  =/=  [_ <. T ,  U >.  /  s ]_ C
)
Assertion
Ref Expression
poimirlem25  |-  ( ph  ->  2  ||  ( # `  { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C } ) )
Distinct variable groups:    i, j, p, s, y, ph    j, N, y    T, j, y    U, j, y    ph, i, p, s    B, i, j, s   
i, K, j, p, s    i, N, p, s    T, i, p    U, i, p    T, s    y, B    C, i, p, y   
y, K    U, s
Allowed substitution hints:    B( p)    C( j, s)

Proof of Theorem poimirlem25
Dummy variables  f 
t  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 neq0 3772 . . 3  |-  ( -. 
{ y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  =  (/)  <->  E. t 
t  e.  { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }
)
2 2z 10970 . . . . . . . 8  |-  2  e.  ZZ
3 iddvds 14304 . . . . . . . 8  |-  ( 2  e.  ZZ  ->  2  ||  2 )
42, 3ax-mp 5 . . . . . . 7  |-  2  ||  2
5 df-2 10669 . . . . . . . 8  |-  2  =  ( 1  +  1 )
6 vex 3084 . . . . . . . . . 10  |-  t  e. 
_V
7 hashsng 12549 . . . . . . . . . 10  |-  ( t  e.  _V  ->  ( # `
 { t } )  =  1 )
86, 7ax-mp 5 . . . . . . . . 9  |-  ( # `  { t } )  =  1
98oveq2i 6313 . . . . . . . 8  |-  ( 1  +  ( # `  {
t } ) )  =  ( 1  +  1 )
105, 9eqtr4i 2454 . . . . . . 7  |-  2  =  ( 1  +  ( # `  {
t } ) )
114, 10breqtri 4444 . . . . . 6  |-  2  ||  ( 1  +  (
# `  { t } ) )
12 fzfi 12185 . . . . . . . . . . . 12  |-  ( 0 ... N )  e. 
Fin
13 rabfi 7799 . . . . . . . . . . . 12  |-  ( ( 0 ... N )  e.  Fin  ->  { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  e.  Fin )
1412, 13ax-mp 5 . . . . . . . . . . 11  |-  { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  e.  Fin
15 diffi 7806 . . . . . . . . . . 11  |-  ( { y  e.  ( 0 ... N )  | 
A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ <. T ,  U >.  /  s ]_ C }  e.  Fin  ->  ( { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  \  { t } )  e.  Fin )
1614, 15ax-mp 5 . . . . . . . . . 10  |-  ( { y  e.  ( 0 ... N )  | 
A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ <. T ,  U >.  /  s ]_ C }  \  { t } )  e.  Fin
17 snfi 7654 . . . . . . . . . 10  |-  { t }  e.  Fin
18 incom 3655 . . . . . . . . . . 11  |-  ( ( { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  \  { t } )  i^i  {
t } )  =  ( { t }  i^i  ( { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  \  { t } ) )
19 disjdif 3867 . . . . . . . . . . 11  |-  ( { t }  i^i  ( { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  \  { t } ) )  =  (/)
2018, 19eqtri 2451 . . . . . . . . . 10  |-  ( ( { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  \  { t } )  i^i  {
t } )  =  (/)
21 hashun 12561 . . . . . . . . . 10  |-  ( ( ( { y  e.  ( 0 ... N
)  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  \  { t } )  e.  Fin  /\ 
{ t }  e.  Fin  /\  ( ( { y  e.  ( 0 ... N )  | 
A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ <. T ,  U >.  /  s ]_ C }  \  { t } )  i^i  { t } )  =  (/) )  ->  ( # `  (
( { y  e.  ( 0 ... N
)  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  \  { t } )  u.  {
t } ) )  =  ( ( # `  ( { y  e.  ( 0 ... N
)  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  \  { t } ) )  +  ( # `  {
t } ) ) )
2216, 17, 20, 21mp3an 1360 . . . . . . . . 9  |-  ( # `  ( ( { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  \  { t } )  u.  { t } ) )  =  ( ( # `  ( { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  \  { t } ) )  +  ( # `  {
t } ) )
23 difsnid 4143 . . . . . . . . . 10  |-  ( t  e.  { y  e.  ( 0 ... N
)  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  ->  ( ( { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  \  { t } )  u.  {
t } )  =  { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C } )
2423fveq2d 5882 . . . . . . . . 9  |-  ( t  e.  { y  e.  ( 0 ... N
)  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  ->  ( # `  ( ( { y  e.  ( 0 ... N )  |  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  \  { t } )  u.  { t } ) )  =  (
# `  { y  e.  ( 0 ... N
)  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C } ) )
2522, 24syl5eqr 2477 . . . . . . . 8  |-  ( t  e.  { y  e.  ( 0 ... N
)  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  ->  ( (
# `  ( {
y  e.  ( 0 ... N )  | 
A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ <. T ,  U >.  /  s ]_ C }  \  { t } ) )  +  (
# `  { t } ) )  =  ( # `  {
y  e.  ( 0 ... N )  | 
A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ <. T ,  U >.  /  s ]_ C } ) )
2625adantl 467 . . . . . . 7  |-  ( (
ph  /\  t  e.  { y  e.  ( 0 ... N )  | 
A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ <. T ,  U >.  /  s ]_ C } )  ->  (
( # `  ( { y  e.  ( 0 ... N )  | 
A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ <. T ,  U >.  /  s ]_ C }  \  { t } ) )  +  (
# `  { t } ) )  =  ( # `  {
y  e.  ( 0 ... N )  | 
A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { y } ) i  = 
[_ <. T ,  U >.  /  s ]_ C } ) )
27 sneq 4006 . . . . . . . . . . . . 13  |-  ( y  =  t  ->  { y }  =  { t } )
2827difeq2d 3583 . . . . . . . . . . . 12  |-  ( y  =  t  ->  (
( 0 ... N
)  \  { y } )  =  ( ( 0 ... N
)  \  { t } ) )
2928rexeqdv 3032 . . . . . . . . . . 11  |-  ( y  =  t  ->  ( E. j  e.  (
( 0 ... N
)  \  { y } ) i  = 
[_ <. T ,  U >.  /  s ]_ C  <->  E. j  e.  ( ( 0 ... N ) 
\  { t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
3029ralbidv 2864 . . . . . . . . . 10  |-  ( y  =  t  ->  ( A. i  e.  (
0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { y } ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
3130elrab 3229 . . . . . . . . 9  |-  ( t  e.  { y  e.  ( 0 ... N
)  |  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
y } ) i  =  [_ <. T ,  U >.  /  s ]_ C }  <->  ( t  e.  ( 0 ... N
)  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
32 poimirlem25.5 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  N  =/=  [_ <. T ,  U >.  /  s ]_ C
)
3332ralrimiva 2839 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. j  e.  ( 0 ... N ) N  =/=  [_ <. T ,  U >.  /  s ]_ C )
34 nfcv 2584 . . . . . . . . . . . . . . . . . 18  |-  F/_ j N
35 nfcsb1v 3411 . . . . . . . . . . . . . . . . . 18  |-  F/_ j [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
3634, 35nfne 2756 . . . . . . . . . . . . . . . . 17  |-  F/ j  N  =/=  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
37 csbeq1a 3404 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  t  ->  [_ <. T ,  U >.  /  s ]_ C  =  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C )
3837neeq2d 2702 . . . . . . . . . . . . . . . . 17  |-  ( j  =  t  ->  ( N  =/=  [_ <. T ,  U >.  /  s ]_ C  <->  N  =/=  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
) )
3936, 38rspc 3176 . . . . . . . . . . . . . . . 16  |-  ( t  e.  ( 0 ... N )  ->  ( A. j  e.  (
0 ... N ) N  =/=  [_ <. T ,  U >.  /  s ]_ C  ->  N  =/=  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C ) )
4033, 39mpan9 471 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  N  =/=  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
)
41 nesym 2696 . . . . . . . . . . . . . . 15  |-  ( N  =/=  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  <->  -. 
[_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  N )
4240, 41sylib 199 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  -.  [_ t  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  =  N )
43 nfv 1751 . . . . . . . . . . . . . . . . . 18  |-  F/ j ( ph  /\  t  e.  ( 0 ... N
) )
4435nfel1 2600 . . . . . . . . . . . . . . . . . 18  |-  F/ j
[_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
)
4543, 44nfim 1976 . . . . . . . . . . . . . . . . 17  |-  F/ j ( ( ph  /\  t  e.  ( 0 ... N ) )  ->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
) )
46 eleq1 2494 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  t  ->  (
j  e.  ( 0 ... N )  <->  t  e.  ( 0 ... N
) ) )
4746anbi2d 708 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  t  ->  (
( ph  /\  j  e.  ( 0 ... N
) )  <->  ( ph  /\  t  e.  ( 0 ... N ) ) ) )
4837eleq1d 2491 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  t  ->  ( [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
)  <->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
) ) )
4947, 48imbi12d 321 . . . . . . . . . . . . . . . . 17  |-  ( j  =  t  ->  (
( ( ph  /\  j  e.  ( 0 ... N ) )  ->  [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
) )  <->  ( ( ph  /\  t  e.  ( 0 ... N ) )  ->  [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N ) ) ) )
50 poimirlem25.3 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  T : ( 1 ... N ) --> ( 0..^ K ) )
51 ovex 6330 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0..^ K )  e.  _V
52 ovex 6330 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1 ... N )  e. 
_V
5351, 52elmap 7505 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T  e.  ( ( 0..^ K )  ^m  (
1 ... N ) )  <-> 
T : ( 1 ... N ) --> ( 0..^ K ) )
5450, 53sylibr 215 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  T  e.  ( ( 0..^ K )  ^m  ( 1 ... N
) ) )
55 poimirlem25.4 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
56 fzfi 12185 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1 ... N )  e. 
Fin
57 f1oexrnex 6753 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N )  /\  ( 1 ... N
)  e.  Fin )  ->  U  e.  _V )
5856, 57mpan2 675 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  U  e.  _V )
59 f1oeq1 5819 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  U  ->  (
f : ( 1 ... N ) -1-1-onto-> ( 1 ... N )  <->  U :
( 1 ... N
)
-1-1-onto-> ( 1 ... N
) ) )
6059elabg 3219 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( U  e.  _V  ->  ( U  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  <->  U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
6158, 60syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  ( U  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) }  <->  U :
( 1 ... N
)
-1-1-onto-> ( 1 ... N
) ) )
6261ibir 245 . . . . . . . . . . . . . . . . . . . . 21  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  U  e.  { f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )
6355, 62syl 17 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  U  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
64 opelxpi 4882 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( T  e.  ( ( 0..^ K )  ^m  ( 1 ... N
) )  /\  U  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  ->  <. T ,  U >.  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
6554, 63, 64syl2anc 665 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  -> 
<. T ,  U >.  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
6665adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  <. T ,  U >.  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )
67 nfcv 2584 . . . . . . . . . . . . . . . . . . 19  |-  F/_ s <. T ,  U >.
68 nfv 1751 . . . . . . . . . . . . . . . . . . . 20  |-  F/ s ( ph  /\  j  e.  ( 0 ... N
) )
69 nfcsb1v 3411 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ s [_ <. T ,  U >.  /  s ]_ C
7069nfel1 2600 . . . . . . . . . . . . . . . . . . . 20  |-  F/ s
[_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
)
7168, 70nfim 1976 . . . . . . . . . . . . . . . . . . 19  |-  F/ s ( ( ph  /\  j  e.  ( 0 ... N ) )  ->  [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
) )
72 csbeq1a 3404 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  <. T ,  U >.  ->  C  =  [_ <. T ,  U >.  /  s ]_ C )
7372eleq1d 2491 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  <. T ,  U >.  ->  ( C  e.  ( 0 ... N
)  <->  [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
) ) )
7473imbi2d 317 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  <. T ,  U >.  ->  ( ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  C  e.  ( 0 ... N
) )  <->  ( ( ph  /\  j  e.  ( 0 ... N ) )  ->  [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N ) ) ) )
75 elun 3606 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  e.  ( { 1 }  u.  { 0 } )  <->  ( p  e.  { 1 }  \/  p  e.  { 0 } ) )
76 fzofzp1 12008 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  e.  ( 0..^ K )  ->  ( i  +  1 )  e.  ( 0 ... K
) )
77 elsni 4021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( p  e.  { 1 }  ->  p  =  1 )
7877oveq2d 6318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( p  e.  { 1 }  ->  ( i  +  p )  =  ( i  +  1 ) )
7978eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( p  e.  { 1 }  ->  ( ( i  +  p )  e.  ( 0 ... K
)  <->  ( i  +  1 )  e.  ( 0 ... K ) ) )
8076, 79syl5ibrcom 225 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( 0..^ K )  ->  ( p  e.  { 1 }  ->  ( i  +  p )  e.  ( 0 ... K ) ) )
81 elfzonn0 11961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  e.  ( 0..^ K )  ->  i  e.  NN0 )
8281nn0cnd 10928 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  e.  ( 0..^ K )  ->  i  e.  CC )
8382addid1d 9834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  e.  ( 0..^ K )  ->  ( i  +  0 )  =  i )
84 elfzofz 11936 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  e.  ( 0..^ K )  ->  i  e.  ( 0 ... K
) )
8583, 84eqeltrd 2510 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  e.  ( 0..^ K )  ->  ( i  +  0 )  e.  ( 0 ... K
) )
86 elsni 4021 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( p  e.  { 0 }  ->  p  =  0 )
8786oveq2d 6318 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( p  e.  { 0 }  ->  ( i  +  p )  =  ( i  +  0 ) )
8887eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( p  e.  { 0 }  ->  ( ( i  +  p )  e.  ( 0 ... K
)  <->  ( i  +  0 )  e.  ( 0 ... K ) ) )
8985, 88syl5ibrcom 225 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( 0..^ K )  ->  ( p  e.  { 0 }  ->  ( i  +  p )  e.  ( 0 ... K ) ) )
9080, 89jaod 381 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( 0..^ K )  ->  ( (
p  e.  { 1 }  \/  p  e. 
{ 0 } )  ->  ( i  +  p )  e.  ( 0 ... K ) ) )
9175, 90syl5bi 220 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  ( 0..^ K )  ->  ( p  e.  ( { 1 }  u.  { 0 } )  ->  ( i  +  p )  e.  ( 0 ... K ) ) )
9291imp 430 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  ( 0..^ K )  /\  p  e.  ( { 1 }  u.  { 0 } ) )  ->  (
i  +  p )  e.  ( 0 ... K ) )
9392adantl 467 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  /\  j  e.  ( 0 ... N
) )  /\  (
i  e.  ( 0..^ K )  /\  p  e.  ( { 1 }  u.  { 0 } ) ) )  -> 
( i  +  p
)  e.  ( 0 ... K ) )
94 xp1st 6834 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 1st `  s
)  e.  ( ( 0..^ K )  ^m  ( 1 ... N
) ) )
95 elmapi 7498 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 1st `  s )  e.  ( ( 0..^ K )  ^m  (
1 ... N ) )  ->  ( 1st `  s
) : ( 1 ... N ) --> ( 0..^ K ) )
9694, 95syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 1st `  s
) : ( 1 ... N ) --> ( 0..^ K ) )
9796adantr 466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  /\  j  e.  ( 0 ... N ) )  ->  ( 1st `  s
) : ( 1 ... N ) --> ( 0..^ K ) )
98 xp2nd 6835 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 2nd `  s
)  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
99 fvex 5888 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 2nd `  s )  e.  _V
100 f1oeq1 5819 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  =  ( 2nd `  s
)  ->  ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  s
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
10199, 100elab 3218 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 2nd `  s )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  <-> 
( 2nd `  s
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
10298, 101sylib 199 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( 2nd `  s
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
103 1ex 9639 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  1  e.  _V
104103fconst 5783 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } ) : ( ( 2nd `  s )
" ( 1 ... j ) ) --> { 1 }
105 c0ex 9638 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  e.  _V
106105fconst 5783 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) : ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) ) --> { 0 }
107104, 106pm3.2i 456 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } ) : ( ( 2nd `  s )
" ( 1 ... j ) ) --> { 1 }  /\  (
( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) : ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) ) --> { 0 } )
108 dff1o3 5834 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 2nd `  s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( ( 2nd `  s ) : ( 1 ... N )
-onto-> ( 1 ... N
)  /\  Fun  `' ( 2nd `  s ) ) )
109108simprbi 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 2nd `  s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  Fun  `' ( 2nd `  s ) )
110 imain 5674 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( Fun  `' ( 2nd `  s
)  ->  ( ( 2nd `  s ) "
( ( 1 ... j )  i^i  (
( j  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  s
) " ( 1 ... j ) )  i^i  ( ( 2nd `  s ) " (
( j  +  1 ) ... N ) ) ) )
111109, 110syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 2nd `  s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  ( ( 2nd `  s ) "
( ( 1 ... j )  i^i  (
( j  +  1 ) ... N ) ) )  =  ( ( ( 2nd `  s
) " ( 1 ... j ) )  i^i  ( ( 2nd `  s ) " (
( j  +  1 ) ... N ) ) ) )
112 elfznn0 11888 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  e.  ( 0 ... N )  ->  j  e.  NN0 )
113112nn0red 10927 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  e.  ( 0 ... N )  ->  j  e.  RR )
114113ltp1d 10538 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  e.  ( 0 ... N )  ->  j  <  ( j  +  1 ) )
115 fzdisj 11827 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  <  ( j  +  1 )  ->  (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... N ) )  =  (/) )
116114, 115syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  e.  ( 0 ... N )  ->  (
( 1 ... j
)  i^i  ( (
j  +  1 ) ... N ) )  =  (/) )
117116imaeq2d 5184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  e.  ( 0 ... N )  ->  (
( 2nd `  s
) " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N ) ) )  =  ( ( 2nd `  s ) " (/) ) )
118 ima0 5199 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 2nd `  s )
" (/) )  =  (/)
119117, 118syl6eq 2479 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  e.  ( 0 ... N )  ->  (
( 2nd `  s
) " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N ) ) )  =  (/) )
120111, 119sylan9req 2484 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 2nd `  s
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N )  /\  j  e.  ( 0 ... N ) )  ->  ( ( ( 2nd `  s )
" ( 1 ... j ) )  i^i  ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) ) )  =  (/) )
121 fun 5760 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } ) : ( ( 2nd `  s ) " (
1 ... j ) ) --> { 1 }  /\  ( ( ( 2nd `  s ) " (
( j  +  1 ) ... N ) )  X.  { 0 } ) : ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) ) --> { 0 } )  /\  ( ( ( 2nd `  s )
" ( 1 ... j ) )  i^i  ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) ) )  =  (/) )  -> 
( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) : ( ( ( 2nd `  s
) " ( 1 ... j ) )  u.  ( ( 2nd `  s ) " (
( j  +  1 ) ... N ) ) ) --> ( { 1 }  u.  {
0 } ) )
122107, 120, 121sylancr 667 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 2nd `  s
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N )  /\  j  e.  ( 0 ... N ) )  ->  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) : ( ( ( 2nd `  s
) " ( 1 ... j ) )  u.  ( ( 2nd `  s ) " (
( j  +  1 ) ... N ) ) ) --> ( { 1 }  u.  {
0 } ) )
123 nn0p1nn 10910 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  e.  NN0  ->  ( j  +  1 )  e.  NN )
124112, 123syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  NN )
125 nnuz 11195 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  NN  =  ( ZZ>= `  1 )
126124, 125syl6eleq 2520 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  ( ZZ>= `  1
) )
127 elfzuz3 11798 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  e.  ( 0 ... N )  ->  N  e.  ( ZZ>= `  j )
)
128 fzsplit2 11825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( j  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ( ZZ>= `  j )
)  ->  ( 1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
129126, 127, 128syl2anc 665 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  e.  ( 0 ... N )  ->  (
1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
130129imaeq2d 5184 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  e.  ( 0 ... N )  ->  (
( 2nd `  s
) " ( 1 ... N ) )  =  ( ( 2nd `  s ) " (
( 1 ... j
)  u.  ( ( j  +  1 ) ... N ) ) ) )
131 imaundi 5264 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 2nd `  s )
" ( ( 1 ... j )  u.  ( ( j  +  1 ) ... N
) ) )  =  ( ( ( 2nd `  s ) " (
1 ... j ) )  u.  ( ( 2nd `  s ) " (
( j  +  1 ) ... N ) ) )
132130, 131syl6req 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  e.  ( 0 ... N )  ->  (
( ( 2nd `  s
) " ( 1 ... j ) )  u.  ( ( 2nd `  s ) " (
( j  +  1 ) ... N ) ) )  =  ( ( 2nd `  s
) " ( 1 ... N ) ) )
133 f1ofo 5835 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 2nd `  s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  s ) : ( 1 ... N )
-onto-> ( 1 ... N
) )
134 foima 5812 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 2nd `  s ) : ( 1 ... N ) -onto-> ( 1 ... N )  -> 
( ( 2nd `  s
) " ( 1 ... N ) )  =  ( 1 ... N ) )
135133, 134syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( 2nd `  s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  ( ( 2nd `  s ) "
( 1 ... N
) )  =  ( 1 ... N ) )
136132, 135sylan9eqr 2485 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 2nd `  s
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N )  /\  j  e.  ( 0 ... N ) )  ->  ( ( ( 2nd `  s )
" ( 1 ... j ) )  u.  ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) ) )  =  ( 1 ... N ) )
137136feq2d 5730 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( 2nd `  s
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N )  /\  j  e.  ( 0 ... N ) )  ->  ( ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) : ( ( ( 2nd `  s
) " ( 1 ... j ) )  u.  ( ( 2nd `  s ) " (
( j  +  1 ) ... N ) ) ) --> ( { 1 }  u.  {
0 } )  <->  ( (
( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) : ( 1 ... N ) --> ( { 1 }  u.  { 0 } ) ) )
138122, 137mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 2nd `  s
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N )  /\  j  e.  ( 0 ... N ) )  ->  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) : ( 1 ... N ) --> ( { 1 }  u.  { 0 } ) )
139102, 138sylan 473 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  /\  j  e.  ( 0 ... N ) )  ->  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) : ( 1 ... N ) --> ( { 1 }  u.  { 0 } ) )
140 fzfid 12186 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  /\  j  e.  ( 0 ... N ) )  ->  ( 1 ... N )  e.  Fin )
141 inidm 3671 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
14293, 97, 139, 140, 140, 141off 6557 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  /\  j  e.  ( 0 ... N ) )  ->  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) )
143 ovex 6330 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  e. 
_V
144 feq1 5725 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  -> 
( p : ( 1 ... N ) --> ( 0 ... K
)  <->  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) ) )
145144anbi2d 708 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  -> 
( ( ph  /\  p : ( 1 ... N ) --> ( 0 ... K ) )  <-> 
( ph  /\  (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) : ( 1 ... N ) --> ( 0 ... K
) ) ) )
146 poimirlem28.1 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  ->  B  =  C )
147146eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  -> 
( B  e.  ( 0 ... N )  <-> 
C  e.  ( 0 ... N ) ) )
148145, 147imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( p  =  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  -> 
( ( ( ph  /\  p : ( 1 ... N ) --> ( 0 ... K ) )  ->  B  e.  ( 0 ... N
) )  <->  ( ( ph  /\  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) )  ->  C  e.  ( 0 ... N ) ) ) )
149 poimirlem28.2 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (
ph  /\  p :
( 1 ... N
) --> ( 0 ... K ) )  ->  B  e.  ( 0 ... N ) )
150143, 148, 149vtocl 3133 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (
ph  /\  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) ) : ( 1 ... N
) --> ( 0 ... K ) )  ->  C  e.  ( 0 ... N ) )
151142, 150sylan2 476 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  ( s  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  /\  j  e.  ( 0 ... N
) ) )  ->  C  e.  ( 0 ... N ) )
152151an12s 808 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  /\  ( ph  /\  j  e.  ( 0 ... N
) ) )  ->  C  e.  ( 0 ... N ) )
153152ex 435 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N
) )  X.  {
f  |  f : ( 1 ... N
)
-1-1-onto-> ( 1 ... N
) } )  -> 
( ( ph  /\  j  e.  ( 0 ... N ) )  ->  C  e.  ( 0 ... N ) ) )
15467, 71, 74, 153vtoclgaf 3144 . . . . . . . . . . . . . . . . . 18  |-  ( <. T ,  U >.  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  ->  ( ( ph  /\  j  e.  ( 0 ... N ) )  ->  [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N ) ) )
15566, 154mpcom 37 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... N ) )
15645, 49, 155chvar 2067 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... N ) )
157 poimir.0 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  N  e.  NN )
158157nnnn0d 10926 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  NN0 )
159 nn0uz 11194 . . . . . . . . . . . . . . . . . . 19  |-  NN0  =  ( ZZ>= `  0 )
160158, 159syl6eleq 2520 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
161 fzm1 11875 . . . . . . . . . . . . . . . . . 18  |-  ( N  e.  ( ZZ>= `  0
)  ->  ( [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... N )  <->  ( [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) )  \/ 
[_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  N ) ) )
162160, 161syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N )  <->  ( [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) )  \/ 
[_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  N ) ) )
163162adantr 466 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  ( [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
)  <->  ( [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) )  \/ 
[_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  N ) ) )
164156, 163mpbid 213 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  ( [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) )  \/  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  N
) )
165164ord 378 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  ( -.  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) )  ->  [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  =  N )
)
16642, 165mt3d 128 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) ) )
167166adantrr 721 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( t  e.  ( 0 ... N
)  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )  ->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) ) )
168 fzfi 12185 . . . . . . . . . . . . . . 15  |-  ( 0 ... ( N  - 
1 ) )  e. 
Fin
169157nncnd 10626 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  CC )
170 1cnd 9660 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  1  e.  CC )
171169, 170, 170addsubd 10008 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( N  + 
1 )  -  1 )  =  ( ( N  -  1 )  +  1 ) )
172 hashfz0 12602 . . . . . . . . . . . . . . . . . . . 20  |-  ( N  e.  NN0  ->  ( # `  ( 0 ... N
) )  =  ( N  +  1 ) )
173158, 172syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( # `  (
0 ... N ) )  =  ( N  + 
1 ) )
1746, 7mp1i 13 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( # `  {
t } )  =  1 )
175173, 174oveq12d 6320 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( # `  (
0 ... N ) )  -  ( # `  {
t } ) )  =  ( ( N  +  1 )  - 
1 ) )
176 nnm1nn0 10912 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  NN0 )
177 hashfz0 12602 . . . . . . . . . . . . . . . . . . 19  |-  ( ( N  -  1 )  e.  NN0  ->  ( # `  ( 0 ... ( N  -  1 ) ) )  =  ( ( N  -  1 )  +  1 ) )
178157, 176, 1773syl 18 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( # `  (
0 ... ( N  - 
1 ) ) )  =  ( ( N  -  1 )  +  1 ) )
179171, 175, 1783eqtr4rd 2474 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( # `  (
0 ... ( N  - 
1 ) ) )  =  ( ( # `  ( 0 ... N
) )  -  ( # `
 { t } ) ) )
180 snssi 4141 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  ( 0 ... N )  ->  { t }  C_  ( 0 ... N ) )
181 hashssdif 12587 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 0 ... N
)  e.  Fin  /\  { t }  C_  (
0 ... N ) )  ->  ( # `  (
( 0 ... N
)  \  { t } ) )  =  ( ( # `  (
0 ... N ) )  -  ( # `  {
t } ) ) )
18212, 180, 181sylancr 667 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  ( 0 ... N )  ->  ( # `
 ( ( 0 ... N )  \  { t } ) )  =  ( (
# `  ( 0 ... N ) )  -  ( # `  { t } ) ) )
183182eqcomd 2430 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  ( 0 ... N )  ->  (
( # `  ( 0 ... N ) )  -  ( # `  {
t } ) )  =  ( # `  (
( 0 ... N
)  \  { t } ) ) )
184179, 183sylan9eq 2483 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  ( # `
 ( 0 ... ( N  -  1 ) ) )  =  ( # `  (
( 0 ... N
)  \  { t } ) ) )
185 diffi 7806 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0 ... N )  e.  Fin  ->  (
( 0 ... N
)  \  { t } )  e.  Fin )
18612, 185ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( ( 0 ... N ) 
\  { t } )  e.  Fin
187 hashen 12530 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 0 ... ( N  -  1 ) )  e.  Fin  /\  ( ( 0 ... N )  \  {
t } )  e. 
Fin )  ->  (
( # `  ( 0 ... ( N  - 
1 ) ) )  =  ( # `  (
( 0 ... N
)  \  { t } ) )  <->  ( 0 ... ( N  - 
1 ) )  ~~  ( ( 0 ... N )  \  {
t } ) ) )
188168, 186, 187mp2an 676 . . . . . . . . . . . . . . . 16  |-  ( (
# `  ( 0 ... ( N  -  1 ) ) )  =  ( # `  (
( 0 ... N
)  \  { t } ) )  <->  ( 0 ... ( N  - 
1 ) )  ~~  ( ( 0 ... N )  \  {
t } ) )
189184, 188sylib 199 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  (
0 ... ( N  - 
1 ) )  ~~  ( ( 0 ... N )  \  {
t } ) )
190 phpreu 31843 . . . . . . . . . . . . . . 15  |-  ( ( ( 0 ... ( N  -  1 ) )  e.  Fin  /\  ( 0 ... ( N  -  1 ) )  ~~  ( ( 0 ... N ) 
\  { t } ) )  ->  ( A. i  e.  (
0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { t } ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  A. i  e.  ( 0 ... ( N  -  1 ) ) E! j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
191168, 189, 190sylancr 667 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  ( A. i  e.  (
0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { t } ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  A. i  e.  ( 0 ... ( N  -  1 ) ) E! j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
192191biimpd 210 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  ( A. i  e.  (
0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { t } ) i  =  [_ <. T ,  U >.  /  s ]_ C  ->  A. i  e.  (
0 ... ( N  - 
1 ) ) E! j  e.  ( ( 0 ... N ) 
\  { t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
193192impr 623 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( t  e.  ( 0 ... N
)  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )  ->  A. i  e.  (
0 ... ( N  - 
1 ) ) E! j  e.  ( ( 0 ... N ) 
\  { t } ) i  =  [_ <. T ,  U >.  /  s ]_ C )
194 nfv 1751 . . . . . . . . . . . . . . 15  |-  F/ z  i  =  [_ <. T ,  U >.  /  s ]_ C
195 nfcsb1v 3411 . . . . . . . . . . . . . . . 16  |-  F/_ j [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
196195nfeq2 2601 . . . . . . . . . . . . . . 15  |-  F/ j  i  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
197 csbeq1a 3404 . . . . . . . . . . . . . . . 16  |-  ( j  =  z  ->  [_ <. T ,  U >.  /  s ]_ C  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C )
198197eqeq2d 2436 . . . . . . . . . . . . . . 15  |-  ( j  =  z  ->  (
i  =  [_ <. T ,  U >.  /  s ]_ C  <->  i  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C ) )
199194, 196, 198cbvreu 3053 . . . . . . . . . . . . . 14  |-  ( E! j  e.  ( ( 0 ... N ) 
\  { t } ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  E! z  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ z  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C )
200 eqeq1 2426 . . . . . . . . . . . . . . 15  |-  ( i  =  [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  ->  ( i  = 
[_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  <->  [_ t  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  = 
[_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
) )
201200reubidv 3013 . . . . . . . . . . . . . 14  |-  ( i  =  [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  ->  ( E! z  e.  ( ( 0 ... N )  \  { t } ) i  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  <->  E! z  e.  ( ( 0 ... N
)  \  { t } ) [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C ) )
202199, 201syl5bb 260 . . . . . . . . . . . . 13  |-  ( i  =  [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  ->  ( E! j  e.  ( ( 0 ... N )  \  { t } ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  E! z  e.  ( ( 0 ... N
)  \  { t } ) [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C ) )
203202rspcv 3178 . . . . . . . . . . . 12  |-  ( [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) )  -> 
( A. i  e.  ( 0 ... ( N  -  1 ) ) E! j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C  ->  E! z  e.  ( ( 0 ... N )  \  {
t } ) [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C ) )
204167, 193, 203sylc 62 . . . . . . . . . . 11  |-  ( (
ph  /\  ( t  e.  ( 0 ... N
)  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )  ->  E! z  e.  (
( 0 ... N
)  \  { t } ) [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C )
205 an32 805 . . . . . . . . . . . . . . . 16  |-  ( ( ( t  e.  ( 0 ... N )  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C )  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  <-> 
( ( t  e.  ( 0 ... N
)  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
206205biimpi 197 . . . . . . . . . . . . . . 15  |-  ( ( ( t  e.  ( 0 ... N )  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C )  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  ->  ( ( t  e.  ( 0 ... N )  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
207206adantll 718 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  (
t  e.  ( 0 ... N )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  ->  ( ( t  e.  ( 0 ... N )  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
208 eqeq2 2437 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  ->  ( i  =  [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C 
<->  i  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C ) )
209 rexsns 4029 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. j  e.  { t } i  =  [_ <. T ,  U >.  /  s ]_ C  <->  [. t  / 
j ]. i  =  [_ <. T ,  U >.  /  s ]_ C )
21035nfeq2 2601 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ j  i  =  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
21137eqeq2d 2436 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  t  ->  (
i  =  [_ <. T ,  U >.  /  s ]_ C  <->  i  =  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C ) )
212210, 211sbciegf 3331 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( t  e.  _V  ->  ( [. t  /  j ]. i  =  [_ <. T ,  U >.  /  s ]_ C  <->  i  =  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C ) )
2136, 212ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( [. t  /  j ]. i  =  [_ <. T ,  U >.  /  s ]_ C  <->  i  =  [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C )
214209, 213bitri 252 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E. j  e.  { t } i  =  [_ <. T ,  U >.  /  s ]_ C  <->  i  =  [_ t  /  j ]_ [_
<. T ,  U >.  /  s ]_ C )
215 rexsns 4029 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. j  e.  { z } i  =  [_ <. T ,  U >.  /  s ]_ C  <->  [. z  / 
j ]. i  =  [_ <. T ,  U >.  /  s ]_ C )
216 vex 3084 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  z  e. 
_V
217196, 198sbciegf 3331 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  e.  _V  ->  ( [. z  /  j ]. i  =  [_ <. T ,  U >.  /  s ]_ C  <->  i  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C ) )
218216, 217ax-mp 5 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( [. z  /  j ]. i  =  [_ <. T ,  U >.  /  s ]_ C  <->  i  =  [_ z  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C )
219215, 218bitri 252 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E. j  e.  { z } i  =  [_ <. T ,  U >.  /  s ]_ C  <->  i  =  [_ z  /  j ]_ [_
<. T ,  U >.  /  s ]_ C )
220208, 214, 2193bitr4g 291 . . . . . . . . . . . . . . . . . . . . 21  |-  ( [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  ->  ( E. j  e.  { t } i  =  [_ <. T ,  U >.  /  s ]_ C  <->  E. j  e.  { z } i  =  [_ <. T ,  U >.  /  s ]_ C ) )
221220orbi1d 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  ->  ( ( E. j  e.  {
t } i  = 
[_ <. T ,  U >.  /  s ]_ C  \/  E. j  e.  ( ( ( 0 ... N )  \  {
t } )  \  { z } ) i  =  [_ <. T ,  U >.  /  s ]_ C )  <->  ( E. j  e.  { z } i  =  [_ <. T ,  U >.  /  s ]_ C  \/  E. j  e.  ( ( ( 0 ... N
)  \  { t } )  \  {
z } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) ) )
222 rexun 3646 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. j  e.  ( { t }  u.  (
( ( 0 ... N )  \  {
t } )  \  { z } ) ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  ( E. j  e.  { t } i  =  [_ <. T ,  U >.  /  s ]_ C  \/  E. j  e.  ( ( ( 0 ... N
)  \  { t } )  \  {
z } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
223 rexun 3646 . . . . . . . . . . . . . . . . . . . 20  |-  ( E. j  e.  ( { z }  u.  (
( ( 0 ... N )  \  {
t } )  \  { z } ) ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  ( E. j  e.  { z } i  =  [_ <. T ,  U >.  /  s ]_ C  \/  E. j  e.  ( ( ( 0 ... N
)  \  { t } )  \  {
z } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
224221, 222, 2233bitr4g 291 . . . . . . . . . . . . . . . . . . 19  |-  ( [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  ->  ( E. j  e.  ( { t }  u.  (
( ( 0 ... N )  \  {
t } )  \  { z } ) ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  E. j  e.  ( { z }  u.  ( ( ( 0 ... N ) 
\  { t } )  \  { z } ) ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
225224adantl 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( t  e.  ( 0 ... N )  /\  z  e.  ( ( 0 ... N
)  \  { t } ) )  /\  [_ t  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  = 
[_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
)  ->  ( E. j  e.  ( {
t }  u.  (
( ( 0 ... N )  \  {
t } )  \  { z } ) ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  E. j  e.  ( { z }  u.  ( ( ( 0 ... N ) 
\  { t } )  \  { z } ) ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
226 eldifsni 4123 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  ( ( 0 ... N )  \  { t } )  ->  z  =/=  t
)
227226necomd 2695 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  ( ( 0 ... N )  \  { t } )  ->  t  =/=  z
)
228 dif32 3736 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 0 ... N
)  \  { t } )  \  {
z } )  =  ( ( ( 0 ... N )  \  { z } ) 
\  { t } )
229228uneq2i 3617 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( { t }  u.  (
( ( 0 ... N )  \  {
t } )  \  { z } ) )  =  ( { t }  u.  (
( ( 0 ... N )  \  {
z } )  \  { t } ) )
230 snssi 4141 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  e.  ( ( 0 ... N )  \  { z } )  ->  { t } 
C_  ( ( 0 ... N )  \  { z } ) )
231 eldifsn 4122 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  e.  ( ( 0 ... N )  \  { z } )  <-> 
( t  e.  ( 0 ... N )  /\  t  =/=  z
) )
232 undif 3876 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( { t }  C_  (
( 0 ... N
)  \  { z } )  <->  ( {
t }  u.  (
( ( 0 ... N )  \  {
z } )  \  { t } ) )  =  ( ( 0 ... N ) 
\  { z } ) )
233230, 231, 2323imtr3i 268 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( t  e.  ( 0 ... N )  /\  t  =/=  z )  -> 
( { t }  u.  ( ( ( 0 ... N ) 
\  { z } )  \  { t } ) )  =  ( ( 0 ... N )  \  {
z } ) )
234229, 233syl5eq 2475 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( t  e.  ( 0 ... N )  /\  t  =/=  z )  -> 
( { t }  u.  ( ( ( 0 ... N ) 
\  { t } )  \  { z } ) )  =  ( ( 0 ... N )  \  {
z } ) )
235227, 234sylan2 476 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( t  e.  ( 0 ... N )  /\  z  e.  ( (
0 ... N )  \  { t } ) )  ->  ( {
t }  u.  (
( ( 0 ... N )  \  {
t } )  \  { z } ) )  =  ( ( 0 ... N ) 
\  { z } ) )
236235rexeqdv 3032 . . . . . . . . . . . . . . . . . . 19  |-  ( ( t  e.  ( 0 ... N )  /\  z  e.  ( (
0 ... N )  \  { t } ) )  ->  ( E. j  e.  ( {
t }  u.  (
( ( 0 ... N )  \  {
t } )  \  { z } ) ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  E. j  e.  ( ( 0 ... N )  \  {
z } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
237236adantr 466 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( t  e.  ( 0 ... N )  /\  z  e.  ( ( 0 ... N
)  \  { t } ) )  /\  [_ t  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  = 
[_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
)  ->  ( E. j  e.  ( {
t }  u.  (
( ( 0 ... N )  \  {
t } )  \  { z } ) ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  E. j  e.  ( ( 0 ... N )  \  {
z } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
238 snssi 4141 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  ( ( 0 ... N )  \  { t } )  ->  { z } 
C_  ( ( 0 ... N )  \  { t } ) )
239 undif 3876 . . . . . . . . . . . . . . . . . . . . 21  |-  ( { z }  C_  (
( 0 ... N
)  \  { t } )  <->  ( {
z }  u.  (
( ( 0 ... N )  \  {
t } )  \  { z } ) )  =  ( ( 0 ... N ) 
\  { t } ) )
240238, 239sylib 199 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  ( ( 0 ... N )  \  { t } )  ->  ( { z }  u.  ( ( ( 0 ... N
)  \  { t } )  \  {
z } ) )  =  ( ( 0 ... N )  \  { t } ) )
241240rexeqdv 3032 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  ( ( 0 ... N )  \  { t } )  ->  ( E. j  e.  ( { z }  u.  ( ( ( 0 ... N ) 
\  { t } )  \  { z } ) ) i  =  [_ <. T ,  U >.  /  s ]_ C 
<->  E. j  e.  ( ( 0 ... N
)  \  { t } ) i  = 
[_ <. T ,  U >.  /  s ]_ C
) )
242241ad2antlr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( t  e.  ( 0 ... N )  /\  z  e.  ( ( 0 ... N
)  \  { t } ) )  /\  [_ t  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  = 
[_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
)  ->  ( E. j  e.  ( {
z }  u.  (
( ( 0 ... N )  \  {
t } )  \  { z } ) ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
243225, 237, 2423bitr3d 286 . . . . . . . . . . . . . . . . 17  |-  ( ( ( t  e.  ( 0 ... N )  /\  z  e.  ( ( 0 ... N
)  \  { t } ) )  /\  [_ t  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  = 
[_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
)  ->  ( E. j  e.  ( (
0 ... N )  \  { z } ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  E. j  e.  ( ( 0 ... N
)  \  { t } ) i  = 
[_ <. T ,  U >.  /  s ]_ C
) )
244243ralbidv 2864 . . . . . . . . . . . . . . . 16  |-  ( ( ( t  e.  ( 0 ... N )  /\  z  e.  ( ( 0 ... N
)  \  { t } ) )  /\  [_ t  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  = 
[_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
)  ->  ( A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { z } ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
245244biimpar 487 . . . . . . . . . . . . . . 15  |-  ( ( ( ( t  e.  ( 0 ... N
)  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  /\  [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ z  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { t } ) i  =  [_ <. T ,  U >.  /  s ]_ C )  ->  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N
)  \  { z } ) i  = 
[_ <. T ,  U >.  /  s ]_ C
)
246245an32s 811 . . . . . . . . . . . . . 14  |-  ( ( ( ( t  e.  ( 0 ... N
)  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C )  /\  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C )  ->  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
z } ) i  =  [_ <. T ,  U >.  /  s ]_ C )
247207, 246sylan 473 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( t  e.  ( 0 ... N )  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )  /\  z  e.  ( (
0 ... N )  \  { t } ) )  /\  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C )  ->  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
z } ) i  =  [_ <. T ,  U >.  /  s ]_ C )
248 simpl 458 . . . . . . . . . . . . . . . . . 18  |-  ( ( t  e.  ( 0 ... N )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { t } ) i  =  [_ <. T ,  U >.  /  s ]_ C )  ->  t  e.  ( 0 ... N ) )
249248anim2i 571 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( t  e.  ( 0 ... N
)  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
t } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )  -> 
( ph  /\  t  e.  ( 0 ... N
) ) )
250 necom 2693 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =/=  t  <->  t  =/=  z )
251250biimpi 197 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =/=  t  ->  t  =/=  z )
252251adantl 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( z  e.  ( 0 ... N )  /\  z  =/=  t )  -> 
t  =/=  z )
253252anim2i 571 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( t  e.  ( 0 ... N )  /\  ( z  e.  ( 0 ... N )  /\  z  =/=  t
) )  ->  (
t  e.  ( 0 ... N )  /\  t  =/=  z ) )
254 eldifsn 4122 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  e.  ( ( 0 ... N )  \  { t } )  <-> 
( z  e.  ( 0 ... N )  /\  z  =/=  t
) )
255254anbi2i 698 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( t  e.  ( 0 ... N )  /\  z  e.  ( (
0 ... N )  \  { t } ) )  <->  ( t  e.  ( 0 ... N
)  /\  ( z  e.  ( 0 ... N
)  /\  z  =/=  t ) ) )
256253, 255, 2313imtr4i 269 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( t  e.  ( 0 ... N )  /\  z  e.  ( (
0 ... N )  \  { t } ) )  ->  t  e.  ( ( 0 ... N )  \  {
z } ) )
257256adantll 718 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  t  e.  ( 0 ... N
) )  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  ->  t  e.  ( ( 0 ... N
)  \  { z } ) )
258257adantr 466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  t  e.  ( 0 ... N ) )  /\  z  e.  ( ( 0 ... N
)  \  { t } ) )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { z } ) i  =  [_ <. T ,  U >.  /  s ]_ C )  ->  t  e.  ( ( 0 ... N
)  \  { z } ) )
25935nfel1 2600 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ j
[_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) )
26043, 259nfim 1976 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ j ( ( ph  /\  t  e.  ( 0 ... N ) )  ->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) ) )
26137eleq1d 2491 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  t  ->  ( [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) )  <->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) ) ) )
26247, 261imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  t  ->  (
( ( ph  /\  j  e.  ( 0 ... N ) )  ->  [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) ) )  <->  ( ( ph  /\  t  e.  ( 0 ... N ) )  ->  [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  - 
1 ) ) ) ) )
26332necomd 2695 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  [_ <. T ,  U >.  /  s ]_ C  =/=  N
)
264263neneqd 2625 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  -.  [_
<. T ,  U >.  /  s ]_ C  =  N )
265 fzm1 11875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( N  e.  ( ZZ>= `  0
)  ->  ( [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
)  <->  ( [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) )  \/ 
[_ <. T ,  U >.  /  s ]_ C  =  N ) ) )
266160, 265syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ph  ->  ( [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N )  <->  ( [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) )  \/  [_ <. T ,  U >.  /  s ]_ C  =  N
) ) )
267266adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
)  <->  ( [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) )  \/ 
[_ <. T ,  U >.  /  s ]_ C  =  N ) ) )
268155, 267mpbid 213 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) )  \/  [_ <. T ,  U >.  /  s ]_ C  =  N
) )
269268ord 378 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( -.  [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) )  ->  [_ <. T ,  U >.  /  s ]_ C  =  N )
)
270264, 269mt3d 128 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) ) )
271260, 262, 270chvar 2067 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) ) )
272271ad2antrr 730 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  t  e.  ( 0 ... N ) )  /\  z  e.  ( ( 0 ... N
)  \  { t } ) )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { z } ) i  =  [_ <. T ,  U >.  /  s ]_ C )  ->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) ) )
273 eldifi 3587 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  ( ( 0 ... N )  \  { t } )  ->  z  e.  ( 0 ... N ) )
274 eleq1 2494 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( t  =  z  ->  (
t  e.  ( 0 ... N )  <->  z  e.  ( 0 ... N
) ) )
275274anbi2d 708 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  z  ->  (
( ph  /\  t  e.  ( 0 ... N
) )  <->  ( ph  /\  z  e.  ( 0 ... N ) ) ) )
276 sneq 4006 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( t  =  z  ->  { t }  =  { z } )
277276difeq2d 3583 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( t  =  z  ->  (
( 0 ... N
)  \  { t } )  =  ( ( 0 ... N
)  \  { z } ) )
278277breq2d 4432 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  z  ->  (
( 0 ... ( N  -  1 ) )  ~~  ( ( 0 ... N ) 
\  { t } )  <->  ( 0 ... ( N  -  1 ) )  ~~  (
( 0 ... N
)  \  { z } ) ) )
279275, 278imbi12d 321 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( t  =  z  ->  (
( ( ph  /\  t  e.  ( 0 ... N ) )  ->  ( 0 ... ( N  -  1 ) )  ~~  (
( 0 ... N
)  \  { t } ) )  <->  ( ( ph  /\  z  e.  ( 0 ... N ) )  ->  ( 0 ... ( N  - 
1 ) )  ~~  ( ( 0 ... N )  \  {
z } ) ) ) )
280279, 189chvarv 2068 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  z  e.  ( 0 ... N
) )  ->  (
0 ... ( N  - 
1 ) )  ~~  ( ( 0 ... N )  \  {
z } ) )
281273, 280sylan2 476 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  ->  ( 0 ... ( N  -  1 ) )  ~~  (
( 0 ... N
)  \  { z } ) )
282281adantlr 719 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  t  e.  ( 0 ... N
) )  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  ->  ( 0 ... ( N  -  1 ) )  ~~  (
( 0 ... N
)  \  { z } ) )
283 phpreu 31843 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( 0 ... ( N  -  1 ) )  e.  Fin  /\  ( 0 ... ( N  -  1 ) )  ~~  ( ( 0 ... N ) 
\  { z } ) )  ->  ( A. i  e.  (
0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { z } ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  A. i  e.  ( 0 ... ( N  -  1 ) ) E! j  e.  ( ( 0 ... N )  \  {
z } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
284168, 283mpan 674 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 0 ... ( N  -  1 ) ) 
~~  ( ( 0 ... N )  \  { z } )  ->  ( A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
z } ) i  =  [_ <. T ,  U >.  /  s ]_ C 
<-> 
A. i  e.  ( 0 ... ( N  -  1 ) ) E! j  e.  ( ( 0 ... N
)  \  { z } ) i  = 
[_ <. T ,  U >.  /  s ]_ C
) )
285284biimpa 486 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( 0 ... ( N  -  1 ) )  ~~  ( ( 0 ... N ) 
\  { z } )  /\  A. i  e.  ( 0 ... ( N  -  1 ) ) E. j  e.  ( ( 0 ... N )  \  {
z } ) i  =  [_ <. T ,  U >.  /  s ]_ C )  ->  A. i  e.  ( 0 ... ( N  -  1 ) ) E! j  e.  ( ( 0 ... N )  \  {
z } ) i  =  [_ <. T ,  U >.  /  s ]_ C )
286282, 285sylan 473 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  t  e.  ( 0 ... N ) )  /\  z  e.  ( ( 0 ... N
)  \  { t } ) )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { z } ) i  =  [_ <. T ,  U >.  /  s ]_ C )  ->  A. i  e.  ( 0 ... ( N  -  1 ) ) E! j  e.  ( ( 0 ... N
)  \  { z } ) i  = 
[_ <. T ,  U >.  /  s ]_ C
)
287 eqeq1 2426 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  =  [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  ->  ( i  = 
[_ <. T ,  U >.  /  s ]_ C  <->  [_ t  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  = 
[_ <. T ,  U >.  /  s ]_ C
) )
288287adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( i  =  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  /\  j  e.  ( ( 0 ... N )  \  {
z } ) )  ->  ( i  = 
[_ <. T ,  U >.  /  s ]_ C  <->  [_ t  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  = 
[_ <. T ,  U >.  /  s ]_ C
) )
289210, 288reubida 3011 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( i  =  [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  ->  ( E! j  e.  ( ( 0 ... N )  \  { z } ) i  =  [_ <. T ,  U >.  /  s ]_ C  <->  E! j  e.  ( ( 0 ... N
)  \  { z } ) [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ <. T ,  U >.  /  s ]_ C ) )
290289rspcv 3178 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) )  -> 
( A. i  e.  ( 0 ... ( N  -  1 ) ) E! j  e.  ( ( 0 ... N )  \  {
z } ) i  =  [_ <. T ,  U >.  /  s ]_ C  ->  E! j  e.  ( ( 0 ... N )  \  {
z } ) [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ <. T ,  U >.  /  s ]_ C ) )
291272, 286, 290sylc 62 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  t  e.  ( 0 ... N ) )  /\  z  e.  ( ( 0 ... N
)  \  { t } ) )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { z } ) i  =  [_ <. T ,  U >.  /  s ]_ C )  ->  E! j  e.  ( ( 0 ... N )  \  {
z } ) [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ <. T ,  U >.  /  s ]_ C )
292 reurmo 3046 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E! j  e.  ( ( 0 ... N ) 
\  { z } ) [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ <. T ,  U >.  /  s ]_ C  ->  E* j  e.  ( ( 0 ... N )  \  {
z } ) [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ <. T ,  U >.  /  s ]_ C )
293291, 292syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  t  e.  ( 0 ... N ) )  /\  z  e.  ( ( 0 ... N
)  \  { t } ) )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.  ( ( 0 ... N ) 
\  { z } ) i  =  [_ <. T ,  U >.  /  s ]_ C )  ->  E* j  e.  ( ( 0 ... N )  \  {
z } ) [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ <. T ,  U >.  /  s ]_ C )
294 nfv 1751 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ i
[_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ <. T ,  U >.  /  s ]_ C
295294rmo3 3390 . . . . . . . . . . . . . . . . . . . . 21  |-  ( E* j  e.  ( ( 0 ... N ) 
\  { z } ) [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ <. T ,  U >.  /  s ]_ C 
<-> 
A. j  e.  ( ( 0 ... N
)  \  { z } ) A. i  e.  ( ( 0 ... N )  \  {
z } ) ( ( [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ <. T ,  U >.  /  s ]_ C  /\  [ i  / 
j ] [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ <. T ,  U >.  /  s ]_ C )  ->  j  =  i ) )
296293, 295sylib 199 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  t  e.  ( 0 ... N ) )  /\  z  e.  ( ( 0 ... N
)  \  { t } ) )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E. j  e.