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

Theorem poimirlem25 31977
Description: Lemma for poimir 31985 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 3744 . . 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 10976 . . . . . . . 8  |-  2  e.  ZZ
3 iddvds 14328 . . . . . . . 8  |-  ( 2  e.  ZZ  ->  2  ||  2 )
42, 3ax-mp 5 . . . . . . 7  |-  2  ||  2
5 df-2 10675 . . . . . . . 8  |-  2  =  ( 1  +  1 )
6 vex 3050 . . . . . . . . . 10  |-  t  e. 
_V
7 hashsng 12556 . . . . . . . . . 10  |-  ( t  e.  _V  ->  ( # `
 { t } )  =  1 )
86, 7ax-mp 5 . . . . . . . . 9  |-  ( # `  { t } )  =  1
98oveq2i 6306 . . . . . . . 8  |-  ( 1  +  ( # `  {
t } ) )  =  ( 1  +  1 )
105, 9eqtr4i 2478 . . . . . . 7  |-  2  =  ( 1  +  ( # `  {
t } ) )
114, 10breqtri 4429 . . . . . 6  |-  2  ||  ( 1  +  (
# `  { t } ) )
12 fzfi 12192 . . . . . . . . . . . 12  |-  ( 0 ... N )  e. 
Fin
13 rabfi 7801 . . . . . . . . . . . 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 7808 . . . . . . . . . . 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 7655 . . . . . . . . . 10  |-  { t }  e.  Fin
18 incom 3627 . . . . . . . . . . 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 3841 . . . . . . . . . . 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 2475 . . . . . . . . . 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 12568 . . . . . . . . . 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 1366 . . . . . . . . 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 4121 . . . . . . . . . 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 5874 . . . . . . . . 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 2501 . . . . . . . 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 468 . . . . . . 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 3980 . . . . . . . . . . . . 13  |-  ( y  =  t  ->  { y }  =  { t } )
2827difeq2d 3553 . . . . . . . . . . . 12  |-  ( y  =  t  ->  (
( 0 ... N
)  \  { y } )  =  ( ( 0 ... N
)  \  { t } ) )
2928rexeqdv 2996 . . . . . . . . . . 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 2829 . . . . . . . . . 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 3198 . . . . . . . . 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 2804 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  A. j  e.  ( 0 ... N ) N  =/=  [_ <. T ,  U >.  /  s ]_ C )
34 nfcv 2594 . . . . . . . . . . . . . . . . . 18  |-  F/_ j N
35 nfcsb1v 3381 . . . . . . . . . . . . . . . . . 18  |-  F/_ j [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
3634, 35nfne 2725 . . . . . . . . . . . . . . . . 17  |-  F/ j  N  =/=  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
37 csbeq1a 3374 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  t  ->  [_ <. T ,  U >.  /  s ]_ C  =  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C )
3837neeq2d 2686 . . . . . . . . . . . . . . . . 17  |-  ( j  =  t  ->  ( N  =/=  [_ <. T ,  U >.  /  s ]_ C  <->  N  =/=  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
) )
3936, 38rspc 3146 . . . . . . . . . . . . . . . 16  |-  ( t  e.  ( 0 ... N )  ->  ( A. j  e.  (
0 ... N ) N  =/=  [_ <. T ,  U >.  /  s ]_ C  ->  N  =/=  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C ) )
4033, 39mpan9 472 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  N  =/=  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
)
41 nesym 2682 . . . . . . . . . . . . . . 15  |-  ( N  =/=  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  <->  -. 
[_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  N )
4240, 41sylib 200 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  -.  [_ t  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  =  N )
43 nfv 1763 . . . . . . . . . . . . . . . . . 18  |-  F/ j ( ph  /\  t  e.  ( 0 ... N
) )
4435nfel1 2608 . . . . . . . . . . . . . . . . . 18  |-  F/ j
[_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
)
4543, 44nfim 2005 . . . . . . . . . . . . . . . . 17  |-  F/ j ( ( ph  /\  t  e.  ( 0 ... N ) )  ->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
) )
46 eleq1 2519 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  t  ->  (
j  e.  ( 0 ... N )  <->  t  e.  ( 0 ... N
) ) )
4746anbi2d 711 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  t  ->  (
( ph  /\  j  e.  ( 0 ... N
) )  <->  ( ph  /\  t  e.  ( 0 ... N ) ) ) )
4837eleq1d 2515 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  t  ->  ( [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
)  <->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
) ) )
4947, 48imbi12d 322 . . . . . . . . . . . . . . . . 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 6323 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0..^ K )  e.  _V
52 ovex 6323 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 1 ... N )  e. 
_V
5351, 52elmap 7505 . . . . . . . . . . . . . . . . . . . . 21  |-  ( T  e.  ( ( 0..^ K )  ^m  (
1 ... N ) )  <-> 
T : ( 1 ... N ) --> ( 0..^ K ) )
5450, 53sylibr 216 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  T  e.  ( ( 0..^ K )  ^m  ( 1 ... N
) ) )
55 poimirlem25.4 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ph  ->  U : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
56 fzfi 12192 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 1 ... N )  e. 
Fin
57 f1oexrnex 6747 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N )  /\  ( 1 ... N
)  e.  Fin )  ->  U  e.  _V )
5856, 57mpan2 678 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( U : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  U  e.  _V )
59 f1oeq1 5810 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( f  =  U  ->  (
f : ( 1 ... N ) -1-1-onto-> ( 1 ... N )  <->  U :
( 1 ... N
)
-1-1-onto-> ( 1 ... N
) ) )
6059elabg 3188 . . . . . . . . . . . . . . . . . . . . . . 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 246 . . . . . . . . . . . . . . . . . . . . 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 4869 . . . . . . . . . . . . . . . . . . . 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 667 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  -> 
<. T ,  U >.  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) )
6665adantr 467 . . . . . . . . . . . . . . . . . 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 2594 . . . . . . . . . . . . . . . . . . 19  |-  F/_ s <. T ,  U >.
68 nfv 1763 . . . . . . . . . . . . . . . . . . . 20  |-  F/ s ( ph  /\  j  e.  ( 0 ... N
) )
69 nfcsb1v 3381 . . . . . . . . . . . . . . . . . . . . 21  |-  F/_ s [_ <. T ,  U >.  /  s ]_ C
7069nfel1 2608 . . . . . . . . . . . . . . . . . . . 20  |-  F/ s
[_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
)
7168, 70nfim 2005 . . . . . . . . . . . . . . . . . . 19  |-  F/ s ( ( ph  /\  j  e.  ( 0 ... N ) )  ->  [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
) )
72 csbeq1a 3374 . . . . . . . . . . . . . . . . . . . . 21  |-  ( s  =  <. T ,  U >.  ->  C  =  [_ <. T ,  U >.  /  s ]_ C )
7372eleq1d 2515 . . . . . . . . . . . . . . . . . . . 20  |-  ( s  =  <. T ,  U >.  ->  ( C  e.  ( 0 ... N
)  <->  [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... N
) ) )
7473imbi2d 318 . . . . . . . . . . . . . . . . . . 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 3576 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( p  e.  ( { 1 }  u.  { 0 } )  <->  ( p  e.  { 1 }  \/  p  e.  { 0 } ) )
76 fzofzp1 12015 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  e.  ( 0..^ K )  ->  ( i  +  1 )  e.  ( 0 ... K
) )
77 elsni 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( p  e.  { 1 }  ->  p  =  1 )
7877oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( p  e.  { 1 }  ->  ( i  +  p )  =  ( i  +  1 ) )
7978eleq1d 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( p  e.  { 1 }  ->  ( ( i  +  p )  e.  ( 0 ... K
)  <->  ( i  +  1 )  e.  ( 0 ... K ) ) )
8076, 79syl5ibrcom 226 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( 0..^ K )  ->  ( p  e.  { 1 }  ->  ( i  +  p )  e.  ( 0 ... K ) ) )
81 elfzonn0 11967 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( i  e.  ( 0..^ K )  ->  i  e.  NN0 )
8281nn0cnd 10934 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( i  e.  ( 0..^ K )  ->  i  e.  CC )
8382addid1d 9838 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  e.  ( 0..^ K )  ->  ( i  +  0 )  =  i )
84 elfzofz 11942 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( i  e.  ( 0..^ K )  ->  i  e.  ( 0 ... K
) )
8583, 84eqeltrd 2531 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( i  e.  ( 0..^ K )  ->  ( i  +  0 )  e.  ( 0 ... K
) )
86 elsni 3995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( p  e.  { 0 }  ->  p  =  0 )
8786oveq2d 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( p  e.  { 0 }  ->  ( i  +  p )  =  ( i  +  0 ) )
8887eleq1d 2515 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( p  e.  { 0 }  ->  ( ( i  +  p )  e.  ( 0 ... K
)  <->  ( i  +  0 )  e.  ( 0 ... K ) ) )
8985, 88syl5ibrcom 226 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( i  e.  ( 0..^ K )  ->  ( p  e.  { 0 }  ->  ( i  +  p )  e.  ( 0 ... K ) ) )
9080, 89jaod 382 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  e.  ( 0..^ K )  ->  ( (
p  e.  { 1 }  \/  p  e. 
{ 0 } )  ->  ( i  +  p )  e.  ( 0 ... K ) ) )
9175, 90syl5bi 221 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( i  e.  ( 0..^ K )  ->  ( p  e.  ( { 1 }  u.  { 0 } )  ->  ( i  +  p )  e.  ( 0 ... K ) ) )
9291imp 431 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( i  e.  ( 0..^ K )  /\  p  e.  ( { 1 }  u.  { 0 } ) )  ->  (
i  +  p )  e.  ( 0 ... K ) )
9392adantl 468 . . . . . . . . . . . . . . . . . . . . . . 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 6828 . . . . . . . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . . . . . 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 6829 . . . . . . . . . . . . . . . . . . . . . . . . 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 5880 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 2nd `  s )  e.  _V
100 f1oeq1 5810 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( f  =  ( 2nd `  s
)  ->  ( f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( 2nd `  s
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) ) )
10199, 100elab 3187 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 2nd `  s )  e.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) }  <-> 
( 2nd `  s
) : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) )
10298, 101sylib 200 . . . . . . . . . . . . . . . . . . . . . . . 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 9643 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  1  e.  _V
104103fconst 5774 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } ) : ( ( 2nd `  s )
" ( 1 ... j ) ) --> { 1 }
105 c0ex 9642 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  0  e.  _V
106105fconst 5774 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) : ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) ) --> { 0 }
107104, 106pm3.2i 457 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5825 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( 2nd `  s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  <->  ( ( 2nd `  s ) : ( 1 ... N )
-onto-> ( 1 ... N
)  /\  Fun  `' ( 2nd `  s ) ) )
109108simprbi 466 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 2nd `  s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  Fun  `' ( 2nd `  s ) )
110 imain 5664 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11894 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  e.  ( 0 ... N )  ->  j  e.  NN0 )
113112nn0red 10933 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  e.  ( 0 ... N )  ->  j  e.  RR )
114113ltp1d 10544 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  e.  ( 0 ... N )  ->  j  <  ( j  +  1 ) )
115 fzdisj 11833 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 5171 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  e.  ( 0 ... N )  ->  (
( 2nd `  s
) " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N ) ) )  =  ( ( 2nd `  s ) " (/) ) )
118 ima0 5186 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 2nd `  s )
" (/) )  =  (/)
119117, 118syl6eq 2503 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  e.  ( 0 ... N )  ->  (
( 2nd `  s
) " ( ( 1 ... j )  i^i  ( ( j  +  1 ) ... N ) ) )  =  (/) )
120111, 119sylan9req 2508 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5751 . . . . . . . . . . . . . . . . . . . . . . . . . 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 670 . . . . . . . . . . . . . . . . . . . . . . . . 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 10916 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( j  e.  NN0  ->  ( j  +  1 )  e.  NN )
124112, 123syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  NN )
125 nnuz 11201 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  NN  =  ( ZZ>= `  1 )
126124, 125syl6eleq 2541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  e.  ( 0 ... N )  ->  (
j  +  1 )  e.  ( ZZ>= `  1
) )
127 elfzuz3 11804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( j  e.  ( 0 ... N )  ->  N  e.  ( ZZ>= `  j )
)
128 fzsplit2 11831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( j  +  1 )  e.  ( ZZ>= ` 
1 )  /\  N  e.  ( ZZ>= `  j )
)  ->  ( 1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
129126, 127, 128syl2anc 667 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  e.  ( 0 ... N )  ->  (
1 ... N )  =  ( ( 1 ... j )  u.  (
( j  +  1 ) ... N ) ) )
130129imaeq2d 5171 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  e.  ( 0 ... N )  ->  (
( 2nd `  s
) " ( 1 ... N ) )  =  ( ( 2nd `  s ) " (
( 1 ... j
)  u.  ( ( j  +  1 ) ... N ) ) ) )
131 imaundi 5251 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 2nd `  s )
" ( ( 1 ... j )  u.  ( ( j  +  1 ) ... N
) ) )  =  ( ( ( 2nd `  s ) " (
1 ... j ) )  u.  ( ( 2nd `  s ) " (
( j  +  1 ) ... N ) ) )
132130, 131syl6req 2504 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  e.  ( 0 ... N )  ->  (
( ( 2nd `  s
) " ( 1 ... j ) )  u.  ( ( 2nd `  s ) " (
( j  +  1 ) ... N ) ) )  =  ( ( 2nd `  s
) " ( 1 ... N ) ) )
133 f1ofo 5826 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( 2nd `  s ) : ( 1 ... N ) -1-1-onto-> ( 1 ... N
)  ->  ( 2nd `  s ) : ( 1 ... N )
-onto-> ( 1 ... N
) )
134 foima 5803 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2509 . . . . . . . . . . . . . . . . . . . . . . . . . 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 5720 . . . . . . . . . . . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . . . . . . . . . . . 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 12193 . . . . . . . . . . . . . . . . . . . . . . 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 3643 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1 ... N )  i^i  ( 1 ... N ) )  =  ( 1 ... N
)
14293, 97, 139, 140, 140, 141off 6551 . . . . . . . . . . . . . . . . . . . . . 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 6323 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  e. 
_V
144 feq1 5715 . . . . . . . . . . . . . . . . . . . . . . . . 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 711 . . . . . . . . . . . . . . . . . . . . . . . 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 2515 . . . . . . . . . . . . . . . . . . . . . . . 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 322 . . . . . . . . . . . . . . . . . . . . . . 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 3102 . . . . . . . . . . . . . . . . . . . . . 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 477 . . . . . . . . . . . . . . . . . . . . 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 811 . . . . . . . . . . . . . . . . . . . 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 436 . . . . . . . . . . . . . . . . . . 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 3114 . . . . . . . . . . . . . . . . . 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 2108 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... N ) )
157 poimir.0 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  N  e.  NN )
158157nnnn0d 10932 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  NN0 )
159 nn0uz 11200 . . . . . . . . . . . . . . . . . . 19  |-  NN0  =  ( ZZ>= `  0 )
160158, 159syl6eleq 2541 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  N  e.  ( ZZ>= ` 
0 ) )
161 fzm1 11881 . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  ( [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) )  \/  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  N
) )
165164ord 379 . . . . . . . . . . . . . 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 129 . . . . . . . . . . . . 13  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) ) )
167166adantrr 724 . . . . . . . . . . . 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 12192 . . . . . . . . . . . . . . 15  |-  ( 0 ... ( N  - 
1 ) )  e. 
Fin
169157nncnd 10632 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  N  e.  CC )
170 1cnd 9664 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  1  e.  CC )
171169, 170, 170addsubd 10012 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( N  + 
1 )  -  1 )  =  ( ( N  -  1 )  +  1 ) )
172 hashfz0 12611 . . . . . . . . . . . . . . . . . . . 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 6313 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( ( # `  (
0 ... N ) )  -  ( # `  {
t } ) )  =  ( ( N  +  1 )  - 
1 ) )
176 nnm1nn0 10918 . . . . . . . . . . . . . . . . . . 19  |-  ( N  e.  NN  ->  ( N  -  1 )  e.  NN0 )
177 hashfz0 12611 . . . . . . . . . . . . . . . . . . 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 2498 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( # `  (
0 ... ( N  - 
1 ) ) )  =  ( ( # `  ( 0 ... N
) )  -  ( # `
 { t } ) ) )
180 snssi 4119 . . . . . . . . . . . . . . . . . . 19  |-  ( t  e.  ( 0 ... N )  ->  { t }  C_  ( 0 ... N ) )
181 hashssdif 12595 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( 0 ... N
)  e.  Fin  /\  { t }  C_  (
0 ... N ) )  ->  ( # `  (
( 0 ... N
)  \  { t } ) )  =  ( ( # `  (
0 ... N ) )  -  ( # `  {
t } ) ) )
18212, 180, 181sylancr 670 . . . . . . . . . . . . . . . . . 18  |-  ( t  e.  ( 0 ... N )  ->  ( # `
 ( ( 0 ... N )  \  { t } ) )  =  ( (
# `  ( 0 ... N ) )  -  ( # `  { t } ) ) )
183182eqcomd 2459 . . . . . . . . . . . . . . . . 17  |-  ( t  e.  ( 0 ... N )  ->  (
( # `  ( 0 ... N ) )  -  ( # `  {
t } ) )  =  ( # `  (
( 0 ... N
)  \  { t } ) ) )
184179, 183sylan9eq 2507 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  ( # `
 ( 0 ... ( N  -  1 ) ) )  =  ( # `  (
( 0 ... N
)  \  { t } ) ) )
185 diffi 7808 . . . . . . . . . . . . . . . . . 18  |-  ( ( 0 ... N )  e.  Fin  ->  (
( 0 ... N
)  \  { t } )  e.  Fin )
18612, 185ax-mp 5 . . . . . . . . . . . . . . . . 17  |-  ( ( 0 ... N ) 
\  { t } )  e.  Fin
187 hashen 12537 . . . . . . . . . . . . . . . . 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 679 . . . . . . . . . . . . . . . 16  |-  ( (
# `  ( 0 ... ( N  -  1 ) ) )  =  ( # `  (
( 0 ... N
)  \  { t } ) )  <->  ( 0 ... ( N  - 
1 ) )  ~~  ( ( 0 ... N )  \  {
t } ) )
189184, 188sylib 200 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  (
0 ... ( N  - 
1 ) )  ~~  ( ( 0 ... N )  \  {
t } ) )
190 phpreu 31941 . . . . . . . . . . . . . . 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 670 . . . . . . . . . . . . . 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 211 . . . . . . . . . . . . 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 625 . . . . . . . . . . . 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 1763 . . . . . . . . . . . . . . 15  |-  F/ z  i  =  [_ <. T ,  U >.  /  s ]_ C
195 nfcsb1v 3381 . . . . . . . . . . . . . . . 16  |-  F/_ j [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
196195nfeq2 2609 . . . . . . . . . . . . . . 15  |-  F/ j  i  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
197 csbeq1a 3374 . . . . . . . . . . . . . . . 16  |-  ( j  =  z  ->  [_ <. T ,  U >.  /  s ]_ C  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C )
198197eqeq2d 2463 . . . . . . . . . . . . . . 15  |-  ( j  =  z  ->  (
i  =  [_ <. T ,  U >.  /  s ]_ C  <->  i  =  [_ z  /  j ]_ [_ <. T ,  U >.  /  s ]_ C ) )
199194, 196, 198cbvreu 3019 . . . . . . . . . . . . . 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 2457 . . . . . . . . . . . . . . 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 2977 . . . . . . . . . . . . . 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 261 . . . . . . . . . . . . 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 3148 . . . . . . . . . . . 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 808 . . . . . . . . . . . . . . . 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 198 . . . . . . . . . . . . . . 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 721 . . . . . . . . . . . . . 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 2464 . . . . . . . . . . . . . . . . . . . . . 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 4006 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. j  e.  { t } i  =  [_ <. T ,  U >.  /  s ]_ C  <->  [. t  / 
j ]. i  =  [_ <. T ,  U >.  /  s ]_ C )
21035nfeq2 2609 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ j  i  =  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C
21137eqeq2d 2463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  t  ->  (
i  =  [_ <. T ,  U >.  /  s ]_ C  <->  i  =  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C ) )
212210, 211sbciegf 3301 . . . . . . . . . . . . . . . . . . . . . . . 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 253 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E. j  e.  { t } i  =  [_ <. T ,  U >.  /  s ]_ C  <->  i  =  [_ t  /  j ]_ [_
<. T ,  U >.  /  s ]_ C )
215 rexsns 4006 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( E. j  e.  { z } i  =  [_ <. T ,  U >.  /  s ]_ C  <->  [. z  / 
j ]. i  =  [_ <. T ,  U >.  /  s ]_ C )
216 vex 3050 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  z  e. 
_V
217196, 198sbciegf 3301 . . . . . . . . . . . . . . . . . . . . . . . 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 253 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( E. j  e.  { z } i  =  [_ <. T ,  U >.  /  s ]_ C  <->  i  =  [_ z  /  j ]_ [_
<. T ,  U >.  /  s ]_ C )
220208, 214, 2193bitr4g 292 . . . . . . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . . . . . 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 3616 . . . . . . . . . . . . . . . . . . . 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 3616 . . . . . . . . . . . . . . . . . . . 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 292 . . . . . . . . . . . . . . . . . . 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 468 . . . . . . . . . . . . . . . . . 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 4101 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  ( ( 0 ... N )  \  { t } )  ->  z  =/=  t
)
227226necomd 2681 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  ( ( 0 ... N )  \  { t } )  ->  t  =/=  z
)
228 dif32 3708 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( 0 ... N
)  \  { t } )  \  {
z } )  =  ( ( ( 0 ... N )  \  { z } ) 
\  { t } )
229228uneq2i 3587 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( { t }  u.  (
( ( 0 ... N )  \  {
t } )  \  { z } ) )  =  ( { t }  u.  (
( ( 0 ... N )  \  {
z } )  \  { t } ) )
230 snssi 4119 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  e.  ( ( 0 ... N )  \  { z } )  ->  { t } 
C_  ( ( 0 ... N )  \  { z } ) )
231 eldifsn 4100 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( t  e.  ( ( 0 ... N )  \  { z } )  <-> 
( t  e.  ( 0 ... N )  /\  t  =/=  z
) )
232 undif 3850 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( { t }  C_  (
( 0 ... N
)  \  { z } )  <->  ( {
t }  u.  (
( ( 0 ... N )  \  {
z } )  \  { t } ) )  =  ( ( 0 ... N ) 
\  { z } ) )
233230, 231, 2323imtr3i 269 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( t  e.  ( 0 ... N )  /\  t  =/=  z )  -> 
( { t }  u.  ( ( ( 0 ... N ) 
\  { z } )  \  { t } ) )  =  ( ( 0 ... N )  \  {
z } ) )
234229, 233syl5eq 2499 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( t  e.  ( 0 ... N )  /\  t  =/=  z )  -> 
( { t }  u.  ( ( ( 0 ... N ) 
\  { t } )  \  { z } ) )  =  ( ( 0 ... N )  \  {
z } ) )
235227, 234sylan2 477 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( t  e.  ( 0 ... N )  /\  z  e.  ( (
0 ... N )  \  { t } ) )  ->  ( {
t }  u.  (
( ( 0 ... N )  \  {
t } )  \  { z } ) )  =  ( ( 0 ... N ) 
\  { z } ) )
236235rexeqdv 2996 . . . . . . . . . . . . . . . . . . 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 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.  ( ( 0 ... N )  \  {
z } ) i  =  [_ <. T ,  U >.  /  s ]_ C ) )
238 snssi 4119 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  ( ( 0 ... N )  \  { t } )  ->  { z } 
C_  ( ( 0 ... N )  \  { t } ) )
239 undif 3850 . . . . . . . . . . . . . . . . . . . . 21  |-  ( { z }  C_  (
( 0 ... N
)  \  { t } )  <->  ( {
z }  u.  (
( ( 0 ... N )  \  {
t } )  \  { z } ) )  =  ( ( 0 ... N ) 
\  { t } ) )
240238, 239sylib 200 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  e.  ( ( 0 ... N )  \  { t } )  ->  ( { z }  u.  ( ( ( 0 ... N
)  \  { t } )  \  {
z } ) )  =  ( ( 0 ... N )  \  { t } ) )
241240rexeqdv 2996 . . . . . . . . . . . . . . . . . . 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 734 . . . . . . . . . . . . . . . . . 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 287 . . . . . . . . . . . . . . . . 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 2829 . . . . . . . . . . . . . . . 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 488 . . . . . . . . . . . . . . 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 814 . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . 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 459 . . . . . . . . . . . . . . . . . 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 573 . . . . . . . . . . . . . . . . 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 2679 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =/=  t  <->  t  =/=  z )
251250biimpi 198 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  =/=  t  ->  t  =/=  z )
252251adantl 468 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( z  e.  ( 0 ... N )  /\  z  =/=  t )  -> 
t  =/=  z )
253252anim2i 573 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( t  e.  ( 0 ... N )  /\  ( z  e.  ( 0 ... N )  /\  z  =/=  t
) )  ->  (
t  e.  ( 0 ... N )  /\  t  =/=  z ) )
254 eldifsn 4100 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z  e.  ( ( 0 ... N )  \  { t } )  <-> 
( z  e.  ( 0 ... N )  /\  z  =/=  t
) )
255254anbi2i 701 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( t  e.  ( 0 ... N )  /\  z  e.  ( (
0 ... N )  \  { t } ) )  <->  ( t  e.  ( 0 ... N
)  /\  ( z  e.  ( 0 ... N
)  /\  z  =/=  t ) ) )
256253, 255, 2313imtr4i 270 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( t  e.  ( 0 ... N )  /\  z  e.  ( (
0 ... N )  \  { t } ) )  ->  t  e.  ( ( 0 ... N )  \  {
z } ) )
257256adantll 721 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  t  e.  ( 0 ... N
) )  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  ->  t  e.  ( ( 0 ... N
)  \  { z } ) )
258257adantr 467 . . . . . . . . . . . . . . . . . . . 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 2608 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  F/ j
[_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) )
26043, 259nfim 2005 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  F/ j ( ( ph  /\  t  e.  ( 0 ... N ) )  ->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) ) )
26137eleq1d 2515 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  t  ->  ( [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) )  <->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) ) ) )
26247, 261imbi12d 322 . . . . . . . . . . . . . . . . . . . . . . . . 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 2681 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  [_ <. T ,  U >.  /  s ]_ C  =/=  N
)
264263neneqd 2631 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  -.  [_
<. T ,  U >.  /  s ]_ C  =  N )
265 fzm1 11881 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 467 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 214 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) )  \/  [_ <. T ,  U >.  /  s ]_ C  =  N
) )
269268ord 379 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  ( -.  [_ <. T ,  U >.  /  s ]_ C  e.  ( 0 ... ( N  -  1 ) )  ->  [_ <. T ,  U >.  /  s ]_ C  =  N )
)
270264, 269mt3d 129 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  j  e.  ( 0 ... N
) )  ->  [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) ) )
271260, 262, 270chvar 2108 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( (
ph  /\  t  e.  ( 0 ... N
) )  ->  [_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  e.  (
0 ... ( N  - 
1 ) ) )
272271ad2antrr 733 . . . . . . . . . . . . . . . . . . . . . . 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 3557 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  e.  ( ( 0 ... N )  \  { t } )  ->  z  e.  ( 0 ... N ) )
274 eleq1 2519 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( t  =  z  ->  (
t  e.  ( 0 ... N )  <->  z  e.  ( 0 ... N
) ) )
275274anbi2d 711 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  z  ->  (
( ph  /\  t  e.  ( 0 ... N
) )  <->  ( ph  /\  z  e.  ( 0 ... N ) ) ) )
276 sneq 3980 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( t  =  z  ->  { t }  =  { z } )
277276difeq2d 3553 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( t  =  z  ->  (
( 0 ... N
)  \  { t } )  =  ( ( 0 ... N
)  \  { z } ) )
278277breq2d 4417 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( t  =  z  ->  (
( 0 ... ( N  -  1 ) )  ~~  ( ( 0 ... N ) 
\  { t } )  <->  ( 0 ... ( N  -  1 ) )  ~~  (
( 0 ... N
)  \  { z } ) ) )
279275, 278imbi12d 322 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2109 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  z  e.  ( 0 ... N
) )  ->  (
0 ... ( N  - 
1 ) )  ~~  ( ( 0 ... N )  \  {
z } ) )
281273, 280sylan2 477 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  ->  ( 0 ... ( N  -  1 ) )  ~~  (
( 0 ... N
)  \  { z } ) )
282281adantlr 722 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  t  e.  ( 0 ... N
) )  /\  z  e.  ( ( 0 ... N )  \  {
t } ) )  ->  ( 0 ... ( N  -  1 ) )  ~~  (
( 0 ... N
)  \  { z } ) )
283 phpreu 31941 . . . . . . . . . . . . . . . . . . . . . . . . . 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 677 . . . . . . . . . . . . . . . . . . . . . . . . 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 487 . . . . . . . . . . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . . . . . . . . . . . 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 2457 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( i  =  [_ t  / 
j ]_ [_ <. T ,  U >.  /  s ]_ C  ->  ( i  = 
[_ <. T ,  U >.  /  s ]_ C  <->  [_ t  /  j ]_ [_
<. T ,  U >.  /  s ]_ C  = 
[_ <. T ,  U >.  /  s ]_ C
) )
288287adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . 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 2975 . . . . . . . . . . . . . . . . . . . . . . . 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 3148 . . . . . . . . . . . . . . . . . . . . . . 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 3012 . . . . . . . . . . . . . . . . . . . . . 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 1763 . . . . . . . . . . . . . . . . . . . . . 22  |-  F/ i
[_ t  /  j ]_ [_ <. T ,  U >.  /  s ]_ C  =  [_ <. T ,  U >.  /  s ]_ C
295294rmo3 3360 . . . . . . . . . . . . . . . . . . . . 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 200 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  t  e.  ( 0 ... N ) )  /\  z  e.  ( ( 0 ... N
)  \  { t } ) )  /\  A. i  e.  ( 0 ... ( N  - 
1 ) ) E.