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

Theorem poimirlem28 31888
Description: Lemma for poimir 31893, a variant of Sperner's lemma. (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 ) )
poimirlem28.3  |-  ( (
ph  /\  ( n  e.  ( 1 ... N
)  /\  p :
( 1 ... N
) --> ( 0 ... K )  /\  (
p `  n )  =  0 ) )  ->  B  <  n
)
poimirlem28.4  |-  ( (
ph  /\  ( n  e.  ( 1 ... N
)  /\  p :
( 1 ... N
) --> ( 0 ... K )  /\  (
p `  n )  =  K ) )  ->  B  =/=  ( n  - 
1 ) )
poimirlem28.5  |-  ( ph  ->  K  e.  NN )
Assertion
Ref Expression
poimirlem28  |-  ( ph  ->  E. s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } ) A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  C )
Distinct variable groups:    f, i,
j, n, p, s    ph, j, n    j, N, n    ph, i, p, s    B, f, i, j, n, s    f, K, i, j, n, p, s   
f, N, i, p, s    C, i, n, p
Allowed substitution hints:    ph( f)    B( p)    C( f, j, s)

Proof of Theorem poimirlem28
Dummy variables  k  m  q  t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poimir.0 . . . . . 6  |-  ( ph  ->  N  e.  NN )
21nnnn0d 10927 . . . . 5  |-  ( ph  ->  N  e.  NN0 )
31nnred 10626 . . . . . 6  |-  ( ph  ->  N  e.  RR )
43leidd 10182 . . . . 5  |-  ( ph  ->  N  <_  N )
52, 2, 43jca 1186 . . . 4  |-  ( ph  ->  ( N  e.  NN0  /\  N  e.  NN0  /\  N  <_  N ) )
6 oveq2 6311 . . . . . . . . . . . . . . . 16  |-  ( k  =  0  ->  (
1 ... k )  =  ( 1 ... 0
) )
7 fz10 11822 . . . . . . . . . . . . . . . 16  |-  ( 1 ... 0 )  =  (/)
86, 7syl6eq 2480 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  (
1 ... k )  =  (/) )
98oveq2d 6319 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  (
( 0..^ K )  ^m  ( 1 ... k ) )  =  ( ( 0..^ K )  ^m  (/) ) )
10 fzofi 12188 . . . . . . . . . . . . . . . 16  |-  ( 0..^ K )  e.  Fin
11 map0e 7515 . . . . . . . . . . . . . . . 16  |-  ( ( 0..^ K )  e. 
Fin  ->  ( ( 0..^ K )  ^m  (/) )  =  1o )
1210, 11ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( ( 0..^ K )  ^m  (/) )  =  1o
13 df1o2 7200 . . . . . . . . . . . . . . 15  |-  1o  =  { (/) }
1412, 13eqtri 2452 . . . . . . . . . . . . . 14  |-  ( ( 0..^ K )  ^m  (/) )  =  { (/) }
159, 14syl6eq 2480 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  (
( 0..^ K )  ^m  ( 1 ... k ) )  =  { (/) } )
16 eqidd 2424 . . . . . . . . . . . . . . . . 17  |-  ( k  =  0  ->  f  =  f )
1716, 8, 8f1oeq123d 5826 . . . . . . . . . . . . . . . 16  |-  ( k  =  0  ->  (
f : ( 1 ... k ) -1-1-onto-> ( 1 ... k )  <->  f : (/) -1-1-onto-> (/) ) )
18 eqid 2423 . . . . . . . . . . . . . . . . 17  |-  (/)  =  (/)
19 f1o00 5861 . . . . . . . . . . . . . . . . 17  |-  ( f : (/)
-1-1-onto-> (/)  <->  ( f  =  (/)  /\  (/)  =  (/) ) )
2018, 19mpbiran2 928 . . . . . . . . . . . . . . . 16  |-  ( f : (/)
-1-1-onto-> (/)  <->  f  =  (/) )
2117, 20syl6bb 265 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  (
f : ( 1 ... k ) -1-1-onto-> ( 1 ... k )  <->  f  =  (/) ) )
2221abbidv 2559 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) }  =  { f  |  f  =  (/) } )
23 df-sn 3998 . . . . . . . . . . . . . 14  |-  { (/) }  =  { f  |  f  =  (/) }
2422, 23syl6eqr 2482 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) }  =  { (/) } )
2515, 24xpeq12d 4876 . . . . . . . . . . . 12  |-  ( k  =  0  ->  (
( ( 0..^ K )  ^m  ( 1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } )  =  ( {
(/) }  X.  { (/) } ) )
26 0ex 4554 . . . . . . . . . . . . 13  |-  (/)  e.  _V
2726, 26xpsn 6079 . . . . . . . . . . . 12  |-  ( {
(/) }  X.  { (/) } )  =  { <. (/)
,  (/) >. }
2825, 27syl6req 2481 . . . . . . . . . . 11  |-  ( k  =  0  ->  { <. (/)
,  (/) >. }  =  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } ) )
29 elsni 4022 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  { <. (/) ,  (/) >. }  ->  s  =  <. (/)
,  (/) >. )
3026, 26op1std 6815 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  <. (/) ,  (/) >.  ->  ( 1st `  s )  =  (/) )
3129, 30syl 17 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  { <. (/) ,  (/) >. }  ->  ( 1st `  s
)  =  (/) )
3231oveq1d 6318 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  { <. (/) ,  (/) >. }  ->  ( ( 1st `  s )  oF  +  (/) )  =  (
(/)  oF  +  (/) ) )
33 f0 5779 . . . . . . . . . . . . . . . . . . . 20  |-  (/) : (/) --> (/)
34 ffn 5744 . . . . . . . . . . . . . . . . . . . 20  |-  ( (/) :
(/) --> (/)  ->  (/)  Fn  (/) )
3533, 34mp1i 13 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  { <. (/) ,  (/) >. }  ->  (/)  Fn  (/) )
3626a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( s  e.  { <. (/) ,  (/) >. }  ->  (/)  e.  _V )
37 inidm 3672 . . . . . . . . . . . . . . . . . . 19  |-  ( (/)  i^i  (/) )  =  (/)
38 0fv 5912 . . . . . . . . . . . . . . . . . . . 20  |-  ( (/) `  n )  =  (/)
3938a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( s  e.  { <. (/)
,  (/) >. }  /\  n  e.  (/) )  ->  ( (/) `  n )  =  (/) )
4035, 35, 36, 36, 37, 39, 39offval 6550 . . . . . . . . . . . . . . . . . 18  |-  ( s  e.  { <. (/) ,  (/) >. }  ->  ( (/)  oF  +  (/) )  =  ( n  e.  (/)  |->  ( (/)  +  (/) ) ) )
41 mpt0 5721 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  (/)  |->  ( (/)  +  (/) ) )  =  (/)
4240, 41syl6eq 2480 . . . . . . . . . . . . . . . . 17  |-  ( s  e.  { <. (/) ,  (/) >. }  ->  ( (/)  oF  +  (/) )  =  (/) )
4332, 42eqtrd 2464 . . . . . . . . . . . . . . . 16  |-  ( s  e.  { <. (/) ,  (/) >. }  ->  ( ( 1st `  s )  oF  +  (/) )  =  (/) )
4443uneq1d 3620 . . . . . . . . . . . . . . 15  |-  ( s  e.  { <. (/) ,  (/) >. }  ->  ( ( ( 1st `  s )  oF  +  (/) )  u.  ( (
1 ... N )  X. 
{ 0 } ) )  =  ( (/)  u.  ( ( 1 ... N )  X.  {
0 } ) ) )
45 uncom 3611 . . . . . . . . . . . . . . . 16  |-  ( (/)  u.  ( ( 1 ... N )  X.  {
0 } ) )  =  ( ( ( 1 ... N )  X.  { 0 } )  u.  (/) )
46 un0 3788 . . . . . . . . . . . . . . . 16  |-  ( ( ( 1 ... N
)  X.  { 0 } )  u.  (/) )  =  ( ( 1 ... N )  X.  {
0 } )
4745, 46eqtri 2452 . . . . . . . . . . . . . . 15  |-  ( (/)  u.  ( ( 1 ... N )  X.  {
0 } ) )  =  ( ( 1 ... N )  X. 
{ 0 } )
4844, 47syl6req 2481 . . . . . . . . . . . . . 14  |-  ( s  e.  { <. (/) ,  (/) >. }  ->  ( ( 1 ... N )  X. 
{ 0 } )  =  ( ( ( 1st `  s )  oF  +  (/) )  u.  ( (
1 ... N )  X. 
{ 0 } ) ) )
4948csbeq1d 3403 . . . . . . . . . . . . 13  |-  ( s  e.  { <. (/) ,  (/) >. }  ->  [_ ( ( 1 ... N )  X. 
{ 0 } )  /  p ]_ B  =  [_ ( ( ( 1st `  s )  oF  +  (/) )  u.  ( (
1 ... N )  X. 
{ 0 } ) )  /  p ]_ B )
5049eqeq2d 2437 . . . . . . . . . . . 12  |-  ( s  e.  { <. (/) ,  (/) >. }  ->  ( 0  = 
[_ ( ( 1 ... N )  X. 
{ 0 } )  /  p ]_ B  <->  0  =  [_ ( ( ( 1st `  s
)  oF  +  (/) )  u.  ( ( 1 ... N )  X.  { 0 } ) )  /  p ]_ B ) )
51 oveq2 6311 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  (
0 ... k )  =  ( 0 ... 0
) )
52 0z 10950 . . . . . . . . . . . . . . . 16  |-  0  e.  ZZ
53 fzsn 11842 . . . . . . . . . . . . . . . 16  |-  ( 0  e.  ZZ  ->  (
0 ... 0 )  =  { 0 } )
5452, 53ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( 0 ... 0 )  =  { 0 }
5551, 54syl6eq 2480 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  (
0 ... k )  =  { 0 } )
56 oveq2 6311 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( k  =  0  ->  (
( j  +  1 ) ... k )  =  ( ( j  +  1 ) ... 0 ) )
5756imaeq2d 5185 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  0  ->  (
( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  =  ( ( 2nd `  s ) " (
( j  +  1 ) ... 0 ) ) )
5857xpeq1d 4874 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  0  ->  (
( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } )  =  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... 0 ) )  X.  { 0 } ) )
5958uneq2d 3621 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  0  ->  (
( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) )  =  ( ( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... 0 ) )  X.  { 0 } ) ) )
6059oveq2d 6319 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  0  ->  (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... 0 ) )  X. 
{ 0 } ) ) ) )
61 oveq1 6310 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( k  =  0  ->  (
k  +  1 )  =  ( 0  +  1 ) )
62 0p1e1 10723 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 0  +  1 )  =  1
6361, 62syl6eq 2480 . . . . . . . . . . . . . . . . . . . . 21  |-  ( k  =  0  ->  (
k  +  1 )  =  1 )
6463oveq1d 6318 . . . . . . . . . . . . . . . . . . . 20  |-  ( k  =  0  ->  (
( k  +  1 ) ... N )  =  ( 1 ... N ) )
6564xpeq1d 4874 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  0  ->  (
( ( k  +  1 ) ... N
)  X.  { 0 } )  =  ( ( 1 ... N
)  X.  { 0 } ) )
6660, 65uneq12d 3622 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  0  ->  (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  =  ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... 0 ) )  X.  { 0 } ) ) )  u.  ( ( 1 ... N )  X.  {
0 } ) ) )
6766csbeq1d 3403 . . . . . . . . . . . . . . . . 17  |-  ( k  =  0  ->  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... 0 ) )  X.  { 0 } ) ) )  u.  ( ( 1 ... N )  X.  {
0 } ) )  /  p ]_ B
)
6867eqeq2d 2437 . . . . . . . . . . . . . . . 16  |-  ( k  =  0  ->  (
i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... 0 ) )  X.  { 0 } ) ) )  u.  ( ( 1 ... N )  X.  {
0 } ) )  /  p ]_ B
) )
6955, 68rexeqbidv 3041 . . . . . . . . . . . . . . 15  |-  ( k  =  0  ->  ( E. j  e.  (
0 ... k ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  E. j  e.  { 0 } i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... 0 ) )  X. 
{ 0 } ) ) )  u.  (
( 1 ... N
)  X.  { 0 } ) )  /  p ]_ B ) )
70 c0ex 9639 . . . . . . . . . . . . . . . 16  |-  0  e.  _V
71 oveq2 6311 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  0  ->  (
1 ... j )  =  ( 1 ... 0
) )
7271, 7syl6eq 2480 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  0  ->  (
1 ... j )  =  (/) )
7372imaeq2d 5185 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  0  ->  (
( 2nd `  s
) " ( 1 ... j ) )  =  ( ( 2nd `  s ) " (/) ) )
74 ima0 5200 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 2nd `  s )
" (/) )  =  (/)
7573, 74syl6eq 2480 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  0  ->  (
( 2nd `  s
) " ( 1 ... j ) )  =  (/) )
7675xpeq1d 4874 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  0  ->  (
( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  =  ( (/)  X. 
{ 1 } ) )
77 0xp 4932 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (/)  X. 
{ 1 } )  =  (/)
7876, 77syl6eq 2480 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  0  ->  (
( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  =  (/) )
79 oveq1 6310 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( j  =  0  ->  (
j  +  1 )  =  ( 0  +  1 ) )
8079, 62syl6eq 2480 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( j  =  0  ->  (
j  +  1 )  =  1 )
8180oveq1d 6318 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( j  =  0  ->  (
( j  +  1 ) ... 0 )  =  ( 1 ... 0 ) )
8281, 7syl6eq 2480 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( j  =  0  ->  (
( j  +  1 ) ... 0 )  =  (/) )
8382imaeq2d 5185 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( j  =  0  ->  (
( 2nd `  s
) " ( ( j  +  1 ) ... 0 ) )  =  ( ( 2nd `  s ) " (/) ) )
8483, 74syl6eq 2480 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( j  =  0  ->  (
( 2nd `  s
) " ( ( j  +  1 ) ... 0 ) )  =  (/) )
8584xpeq1d 4874 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( j  =  0  ->  (
( ( 2nd `  s
) " ( ( j  +  1 ) ... 0 ) )  X.  { 0 } )  =  ( (/)  X. 
{ 0 } ) )
86 0xp 4932 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (/)  X. 
{ 0 } )  =  (/)
8785, 86syl6eq 2480 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( j  =  0  ->  (
( ( 2nd `  s
) " ( ( j  +  1 ) ... 0 ) )  X.  { 0 } )  =  (/) )
8878, 87uneq12d 3622 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  0  ->  (
( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... 0 ) )  X.  { 0 } ) )  =  (
(/)  u.  (/) ) )
89 un0 3788 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (/)  u.  (/) )  =  (/)
9088, 89syl6eq 2480 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  0  ->  (
( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... 0 ) )  X.  { 0 } ) )  =  (/) )
9190oveq2d 6319 . . . . . . . . . . . . . . . . . . 19  |-  ( j  =  0  ->  (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... 0 ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  s
)  oF  +  (/) ) )
9291uneq1d 3620 . . . . . . . . . . . . . . . . . 18  |-  ( j  =  0  ->  (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... 0 ) )  X. 
{ 0 } ) ) )  u.  (
( 1 ... N
)  X.  { 0 } ) )  =  ( ( ( 1st `  s )  oF  +  (/) )  u.  (
( 1 ... N
)  X.  { 0 } ) ) )
9392csbeq1d 3403 . . . . . . . . . . . . . . . . 17  |-  ( j  =  0  ->  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... 0 ) )  X. 
{ 0 } ) ) )  u.  (
( 1 ... N
)  X.  { 0 } ) )  /  p ]_ B  =  [_ ( ( ( 1st `  s )  oF  +  (/) )  u.  (
( 1 ... N
)  X.  { 0 } ) )  /  p ]_ B )
9493eqeq2d 2437 . . . . . . . . . . . . . . . 16  |-  ( j  =  0  ->  (
i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... 0 ) )  X. 
{ 0 } ) ) )  u.  (
( 1 ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  i  =  [_ ( ( ( 1st `  s )  oF  +  (/) )  u.  (
( 1 ... N
)  X.  { 0 } ) )  /  p ]_ B ) )
9570, 94rexsn 4037 . . . . . . . . . . . . . . 15  |-  ( E. j  e.  { 0 } i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... 0 ) )  X.  { 0 } ) ) )  u.  ( ( 1 ... N )  X.  {
0 } ) )  /  p ]_ B  <->  i  =  [_ ( ( ( 1st `  s
)  oF  +  (/) )  u.  ( ( 1 ... N )  X.  { 0 } ) )  /  p ]_ B )
9669, 95syl6bb 265 . . . . . . . . . . . . . 14  |-  ( k  =  0  ->  ( E. j  e.  (
0 ... k ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  i  =  [_ ( ( ( 1st `  s )  oF  +  (/) )  u.  (
( 1 ... N
)  X.  { 0 } ) )  /  p ]_ B ) )
9755, 96raleqbidv 3040 . . . . . . . . . . . . 13  |-  ( k  =  0  ->  ( A. i  e.  (
0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  A. i  e.  { 0 } i  =  [_ ( ( ( 1st `  s
)  oF  +  (/) )  u.  ( ( 1 ... N )  X.  { 0 } ) )  /  p ]_ B ) )
98 eqeq1 2427 . . . . . . . . . . . . . 14  |-  ( i  =  0  ->  (
i  =  [_ (
( ( 1st `  s
)  oF  +  (/) )  u.  ( ( 1 ... N )  X.  { 0 } ) )  /  p ]_ B  <->  0  =  [_ ( ( ( 1st `  s )  oF  +  (/) )  u.  (
( 1 ... N
)  X.  { 0 } ) )  /  p ]_ B ) )
9970, 98ralsn 4036 . . . . . . . . . . . . 13  |-  ( A. i  e.  { 0 } i  =  [_ ( ( ( 1st `  s )  oF  +  (/) )  u.  (
( 1 ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  0  =  [_ ( ( ( 1st `  s )  oF  +  (/) )  u.  (
( 1 ... N
)  X.  { 0 } ) )  /  p ]_ B )
10097, 99syl6rbb 266 . . . . . . . . . . . 12  |-  ( k  =  0  ->  (
0  =  [_ (
( ( 1st `  s
)  oF  +  (/) )  u.  ( ( 1 ... N )  X.  { 0 } ) )  /  p ]_ B  <->  A. i  e.  ( 0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B ) )
10150, 100sylan9bbr 706 . . . . . . . . . . 11  |-  ( ( k  =  0  /\  s  e.  { <. (/)
,  (/) >. } )  -> 
( 0  =  [_ ( ( 1 ... N )  X.  {
0 } )  /  p ]_ B  <->  A. i  e.  ( 0 ... k
) E. j  e.  ( 0 ... k
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) ) )  u.  ( ( ( k  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
) )
10228, 101rabeqbidva 3078 . . . . . . . . . 10  |-  ( k  =  0  ->  { s  e.  { <. (/) ,  (/) >. }  |  0  =  [_ ( ( 1 ... N )  X.  {
0 } )  /  p ]_ B }  =  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } )  |  A. i  e.  ( 0 ... k
) E. j  e.  ( 0 ... k
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) ) )  u.  ( ( ( k  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } )
103102eqcomd 2431 . . . . . . . . 9  |-  ( k  =  0  ->  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k
) )  X.  {
f  |  f : ( 1 ... k
)
-1-1-onto-> ( 1 ... k
) } )  | 
A. i  e.  ( 0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B }  =  { s  e.  { <.
(/) ,  (/) >. }  | 
0  =  [_ (
( 1 ... N
)  X.  { 0 } )  /  p ]_ B } )
104103fveq2d 5883 . . . . . . . 8  |-  ( k  =  0  ->  ( # `
 { s  e.  ( ( ( 0..^ K )  ^m  (
1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } )  |  A. i  e.  ( 0 ... k
) E. j  e.  ( 0 ... k
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) ) )  u.  ( ( ( k  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } )  =  (
# `  { s  e.  { <. (/) ,  (/) >. }  | 
0  =  [_ (
( 1 ... N
)  X.  { 0 } )  /  p ]_ B } ) )
105104breq2d 4433 . . . . . . 7  |-  ( k  =  0  ->  (
2  ||  ( # `  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X. 
{ f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k
) } )  | 
A. i  e.  ( 0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B } )  <->  2  ||  ( # `  { s  e.  { <.
(/) ,  (/) >. }  | 
0  =  [_ (
( 1 ... N
)  X.  { 0 } )  /  p ]_ B } ) ) )
106105notbid 296 . . . . . 6  |-  ( k  =  0  ->  ( -.  2  ||  ( # `  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } )  |  A. i  e.  ( 0 ... k
) E. j  e.  ( 0 ... k
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) ) )  u.  ( ( ( k  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } )  <->  -.  2  ||  ( # `  {
s  e.  { <. (/)
,  (/) >. }  |  0  =  [_ ( ( 1 ... N )  X.  { 0 } )  /  p ]_ B } ) ) )
107106imbi2d 318 . . . . 5  |-  ( k  =  0  ->  (
( ph  ->  -.  2  ||  ( # `  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X. 
{ f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k
) } )  | 
A. i  e.  ( 0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B } ) )  <->  ( ph  ->  -.  2  ||  ( # `  { s  e.  { <.
(/) ,  (/) >. }  | 
0  =  [_ (
( 1 ... N
)  X.  { 0 } )  /  p ]_ B } ) ) ) )
108 oveq2 6311 . . . . . . . . . . . 12  |-  ( k  =  m  ->  (
1 ... k )  =  ( 1 ... m
) )
109108oveq2d 6319 . . . . . . . . . . 11  |-  ( k  =  m  ->  (
( 0..^ K )  ^m  ( 1 ... k ) )  =  ( ( 0..^ K )  ^m  ( 1 ... m ) ) )
110 eqidd 2424 . . . . . . . . . . . . 13  |-  ( k  =  m  ->  f  =  f )
111110, 108, 108f1oeq123d 5826 . . . . . . . . . . . 12  |-  ( k  =  m  ->  (
f : ( 1 ... k ) -1-1-onto-> ( 1 ... k )  <->  f :
( 1 ... m
)
-1-1-onto-> ( 1 ... m
) ) )
112111abbidv 2559 . . . . . . . . . . 11  |-  ( k  =  m  ->  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) }  =  { f  |  f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } )
113109, 112xpeq12d 4876 . . . . . . . . . 10  |-  ( k  =  m  ->  (
( ( 0..^ K )  ^m  ( 1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } )  =  ( ( ( 0..^ K )  ^m  ( 1 ... m ) )  X. 
{ f  |  f : ( 1 ... m ) -1-1-onto-> ( 1 ... m
) } ) )
114 oveq2 6311 . . . . . . . . . . 11  |-  ( k  =  m  ->  (
0 ... k )  =  ( 0 ... m
) )
115 oveq2 6311 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  m  ->  (
( j  +  1 ) ... k )  =  ( ( j  +  1 ) ... m ) )
116115imaeq2d 5185 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  m  ->  (
( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  =  ( ( 2nd `  s ) " (
( j  +  1 ) ... m ) ) )
117116xpeq1d 4874 . . . . . . . . . . . . . . . . 17  |-  ( k  =  m  ->  (
( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } )  =  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... m ) )  X.  { 0 } ) )
118117uneq2d 3621 . . . . . . . . . . . . . . . 16  |-  ( k  =  m  ->  (
( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) )  =  ( ( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... m ) )  X.  { 0 } ) ) )
119118oveq2d 6319 . . . . . . . . . . . . . . 15  |-  ( k  =  m  ->  (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... m ) )  X. 
{ 0 } ) ) ) )
120 oveq1 6310 . . . . . . . . . . . . . . . . 17  |-  ( k  =  m  ->  (
k  +  1 )  =  ( m  + 
1 ) )
121120oveq1d 6318 . . . . . . . . . . . . . . . 16  |-  ( k  =  m  ->  (
( k  +  1 ) ... N )  =  ( ( m  +  1 ) ... N ) )
122121xpeq1d 4874 . . . . . . . . . . . . . . 15  |-  ( k  =  m  ->  (
( ( k  +  1 ) ... N
)  X.  { 0 } )  =  ( ( ( m  + 
1 ) ... N
)  X.  { 0 } ) )
123119, 122uneq12d 3622 . . . . . . . . . . . . . 14  |-  ( k  =  m  ->  (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  =  ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... m ) )  X.  { 0 } ) ) )  u.  ( ( ( m  +  1 ) ... N )  X.  {
0 } ) ) )
124123csbeq1d 3403 . . . . . . . . . . . . 13  |-  ( k  =  m  ->  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... m ) )  X.  { 0 } ) ) )  u.  ( ( ( m  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
)
125124eqeq2d 2437 . . . . . . . . . . . 12  |-  ( k  =  m  ->  (
i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... m ) )  X.  { 0 } ) ) )  u.  ( ( ( m  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
) )
126114, 125rexeqbidv 3041 . . . . . . . . . . 11  |-  ( k  =  m  ->  ( E. j  e.  (
0 ... k ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  E. j  e.  ( 0 ... m
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... m ) )  X.  { 0 } ) ) )  u.  ( ( ( m  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
) )
127114, 126raleqbidv 3040 . . . . . . . . . 10  |-  ( k  =  m  ->  ( A. i  e.  (
0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  A. i  e.  ( 0 ... m
) E. j  e.  ( 0 ... m
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... m ) )  X.  { 0 } ) ) )  u.  ( ( ( m  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
) )
128113, 127rabeqbidv 3077 . . . . . . . . 9  |-  ( k  =  m  ->  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k
) )  X.  {
f  |  f : ( 1 ... k
)
-1-1-onto-> ( 1 ... k
) } )  | 
A. i  e.  ( 0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B }  =  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... m ) )  X.  { f  |  f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } )  |  A. i  e.  ( 0 ... m
) E. j  e.  ( 0 ... m
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... m ) )  X.  { 0 } ) ) )  u.  ( ( ( m  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } )
129128fveq2d 5883 . . . . . . . 8  |-  ( k  =  m  ->  ( # `
 { s  e.  ( ( ( 0..^ K )  ^m  (
1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } )  |  A. i  e.  ( 0 ... k
) E. j  e.  ( 0 ... k
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) ) )  u.  ( ( ( k  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } )  =  (
# `  { s  e.  ( ( ( 0..^ K )  ^m  (
1 ... m ) )  X.  { f  |  f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } )  |  A. i  e.  ( 0 ... m
) E. j  e.  ( 0 ... m
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... m ) )  X.  { 0 } ) ) )  u.  ( ( ( m  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } ) )
130129breq2d 4433 . . . . . . 7  |-  ( k  =  m  ->  (
2  ||  ( # `  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X. 
{ f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k
) } )  | 
A. i  e.  ( 0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B } )  <->  2  ||  ( # `  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... m ) )  X.  { f  |  f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } )  |  A. i  e.  ( 0 ... m
) E. j  e.  ( 0 ... m
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... m ) )  X.  { 0 } ) ) )  u.  ( ( ( m  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } ) ) )
131130notbid 296 . . . . . 6  |-  ( k  =  m  ->  ( -.  2  ||  ( # `  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } )  |  A. i  e.  ( 0 ... k
) E. j  e.  ( 0 ... k
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) ) )  u.  ( ( ( k  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } )  <->  -.  2  ||  ( # `  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... m ) )  X. 
{ f  |  f : ( 1 ... m ) -1-1-onto-> ( 1 ... m
) } )  | 
A. i  e.  ( 0 ... m ) E. j  e.  ( 0 ... m ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... m ) )  X. 
{ 0 } ) ) )  u.  (
( ( m  + 
1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B } ) ) )
132131imbi2d 318 . . . . 5  |-  ( k  =  m  ->  (
( ph  ->  -.  2  ||  ( # `  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X. 
{ f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k
) } )  | 
A. i  e.  ( 0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B } ) )  <->  ( ph  ->  -.  2  ||  ( # `  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... m ) )  X.  { f  |  f : ( 1 ... m ) -1-1-onto-> ( 1 ... m ) } )  |  A. i  e.  ( 0 ... m
) E. j  e.  ( 0 ... m
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... m ) )  X.  { 0 } ) ) )  u.  ( ( ( m  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } ) ) ) )
133 oveq2 6311 . . . . . . . . . . . 12  |-  ( k  =  ( m  + 
1 )  ->  (
1 ... k )  =  ( 1 ... (
m  +  1 ) ) )
134133oveq2d 6319 . . . . . . . . . . 11  |-  ( k  =  ( m  + 
1 )  ->  (
( 0..^ K )  ^m  ( 1 ... k ) )  =  ( ( 0..^ K )  ^m  ( 1 ... ( m  + 
1 ) ) ) )
135 eqidd 2424 . . . . . . . . . . . . 13  |-  ( k  =  ( m  + 
1 )  ->  f  =  f )
136135, 133, 133f1oeq123d 5826 . . . . . . . . . . . 12  |-  ( k  =  ( m  + 
1 )  ->  (
f : ( 1 ... k ) -1-1-onto-> ( 1 ... k )  <->  f :
( 1 ... (
m  +  1 ) ) -1-1-onto-> ( 1 ... (
m  +  1 ) ) ) )
137136abbidv 2559 . . . . . . . . . . 11  |-  ( k  =  ( m  + 
1 )  ->  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) }  =  { f  |  f : ( 1 ... ( m  +  1 ) ) -1-1-onto-> ( 1 ... ( m  +  1 ) ) } )
138134, 137xpeq12d 4876 . . . . . . . . . 10  |-  ( k  =  ( m  + 
1 )  ->  (
( ( 0..^ K )  ^m  ( 1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } )  =  ( ( ( 0..^ K )  ^m  ( 1 ... ( m  +  1 ) ) )  X. 
{ f  |  f : ( 1 ... ( m  +  1 ) ) -1-1-onto-> ( 1 ... (
m  +  1 ) ) } ) )
139 oveq2 6311 . . . . . . . . . . 11  |-  ( k  =  ( m  + 
1 )  ->  (
0 ... k )  =  ( 0 ... (
m  +  1 ) ) )
140 oveq2 6311 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  ( m  + 
1 )  ->  (
( j  +  1 ) ... k )  =  ( ( j  +  1 ) ... ( m  +  1 ) ) )
141140imaeq2d 5185 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  ( m  + 
1 )  ->  (
( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  =  ( ( 2nd `  s ) " (
( j  +  1 ) ... ( m  +  1 ) ) ) )
142141xpeq1d 4874 . . . . . . . . . . . . . . . . 17  |-  ( k  =  ( m  + 
1 )  ->  (
( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } )  =  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( m  + 
1 ) ) )  X.  { 0 } ) )
143142uneq2d 3621 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( m  + 
1 )  ->  (
( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) )  =  ( ( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( m  + 
1 ) ) )  X.  { 0 } ) ) )
144143oveq2d 6319 . . . . . . . . . . . . . . 15  |-  ( k  =  ( m  + 
1 )  ->  (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... ( m  +  1 ) ) )  X. 
{ 0 } ) ) ) )
145 oveq1 6310 . . . . . . . . . . . . . . . . 17  |-  ( k  =  ( m  + 
1 )  ->  (
k  +  1 )  =  ( ( m  +  1 )  +  1 ) )
146145oveq1d 6318 . . . . . . . . . . . . . . . 16  |-  ( k  =  ( m  + 
1 )  ->  (
( k  +  1 ) ... N )  =  ( ( ( m  +  1 )  +  1 ) ... N ) )
147146xpeq1d 4874 . . . . . . . . . . . . . . 15  |-  ( k  =  ( m  + 
1 )  ->  (
( ( k  +  1 ) ... N
)  X.  { 0 } )  =  ( ( ( ( m  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )
148144, 147uneq12d 3622 . . . . . . . . . . . . . 14  |-  ( k  =  ( m  + 
1 )  ->  (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  =  ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( m  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( m  +  1 )  +  1 ) ... N )  X.  {
0 } ) ) )
149148csbeq1d 3403 . . . . . . . . . . . . 13  |-  ( k  =  ( m  + 
1 )  ->  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( m  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( m  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
)
150149eqeq2d 2437 . . . . . . . . . . . 12  |-  ( k  =  ( m  + 
1 )  ->  (
i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( m  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( m  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
) )
151139, 150rexeqbidv 3041 . . . . . . . . . . 11  |-  ( k  =  ( m  + 
1 )  ->  ( E. j  e.  (
0 ... k ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  E. j  e.  ( 0 ... (
m  +  1 ) ) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( m  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( m  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
) )
152139, 151raleqbidv 3040 . . . . . . . . . 10  |-  ( k  =  ( m  + 
1 )  ->  ( A. i  e.  (
0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  A. i  e.  ( 0 ... (
m  +  1 ) ) E. j  e.  ( 0 ... (
m  +  1 ) ) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( m  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( m  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
) )
153138, 152rabeqbidv 3077 . . . . . . . . 9  |-  ( k  =  ( m  + 
1 )  ->  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k
) )  X.  {
f  |  f : ( 1 ... k
)
-1-1-onto-> ( 1 ... k
) } )  | 
A. i  e.  ( 0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B }  =  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( m  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( m  + 
1 ) ) -1-1-onto-> ( 1 ... ( m  + 
1 ) ) } )  |  A. i  e.  ( 0 ... (
m  +  1 ) ) E. j  e.  ( 0 ... (
m  +  1 ) ) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( m  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( m  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } )
154153fveq2d 5883 . . . . . . . 8  |-  ( k  =  ( m  + 
1 )  ->  ( # `
 { s  e.  ( ( ( 0..^ K )  ^m  (
1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } )  |  A. i  e.  ( 0 ... k
) E. j  e.  ( 0 ... k
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) ) )  u.  ( ( ( k  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } )  =  (
# `  { s  e.  ( ( ( 0..^ K )  ^m  (
1 ... ( m  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( m  + 
1 ) ) -1-1-onto-> ( 1 ... ( m  + 
1 ) ) } )  |  A. i  e.  ( 0 ... (
m  +  1 ) ) E. j  e.  ( 0 ... (
m  +  1 ) ) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( m  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( m  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } ) )
155154breq2d 4433 . . . . . . 7  |-  ( k  =  ( m  + 
1 )  ->  (
2  ||  ( # `  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X. 
{ f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k
) } )  | 
A. i  e.  ( 0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B } )  <->  2  ||  ( # `  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( m  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( m  + 
1 ) ) -1-1-onto-> ( 1 ... ( m  + 
1 ) ) } )  |  A. i  e.  ( 0 ... (
m  +  1 ) ) E. j  e.  ( 0 ... (
m  +  1 ) ) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( m  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( m  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } ) ) )
156155notbid 296 . . . . . 6  |-  ( k  =  ( m  + 
1 )  ->  ( -.  2  ||  ( # `  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } )  |  A. i  e.  ( 0 ... k
) E. j  e.  ( 0 ... k
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) ) )  u.  ( ( ( k  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } )  <->  -.  2  ||  ( # `  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( m  +  1 ) ) )  X. 
{ f  |  f : ( 1 ... ( m  +  1 ) ) -1-1-onto-> ( 1 ... (
m  +  1 ) ) } )  | 
A. i  e.  ( 0 ... ( m  +  1 ) ) E. j  e.  ( 0 ... ( m  +  1 ) ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... ( m  +  1 ) ) )  X. 
{ 0 } ) ) )  u.  (
( ( ( m  +  1 )  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B } ) ) )
157156imbi2d 318 . . . . 5  |-  ( k  =  ( m  + 
1 )  ->  (
( ph  ->  -.  2  ||  ( # `  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X. 
{ f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k
) } )  | 
A. i  e.  ( 0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B } ) )  <->  ( ph  ->  -.  2  ||  ( # `  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... ( m  + 
1 ) ) )  X.  { f  |  f : ( 1 ... ( m  + 
1 ) ) -1-1-onto-> ( 1 ... ( m  + 
1 ) ) } )  |  A. i  e.  ( 0 ... (
m  +  1 ) ) E. j  e.  ( 0 ... (
m  +  1 ) ) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... ( m  + 
1 ) ) )  X.  { 0 } ) ) )  u.  ( ( ( ( m  +  1 )  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } ) ) ) )
158 oveq2 6311 . . . . . . . . . . . 12  |-  ( k  =  N  ->  (
1 ... k )  =  ( 1 ... N
) )
159158oveq2d 6319 . . . . . . . . . . 11  |-  ( k  =  N  ->  (
( 0..^ K )  ^m  ( 1 ... k ) )  =  ( ( 0..^ K )  ^m  ( 1 ... N ) ) )
160 eqidd 2424 . . . . . . . . . . . . 13  |-  ( k  =  N  ->  f  =  f )
161160, 158, 158f1oeq123d 5826 . . . . . . . . . . . 12  |-  ( k  =  N  ->  (
f : ( 1 ... k ) -1-1-onto-> ( 1 ... k )  <->  f :
( 1 ... N
)
-1-1-onto-> ( 1 ... N
) ) )
162161abbidv 2559 . . . . . . . . . . 11  |-  ( k  =  N  ->  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) }  =  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )
163159, 162xpeq12d 4876 . . . . . . . . . 10  |-  ( k  =  N  ->  (
( ( 0..^ K )  ^m  ( 1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } )  =  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } ) )
164 oveq2 6311 . . . . . . . . . . 11  |-  ( k  =  N  ->  (
0 ... k )  =  ( 0 ... N
) )
165 oveq2 6311 . . . . . . . . . . . . . . . . . . 19  |-  ( k  =  N  ->  (
( j  +  1 ) ... k )  =  ( ( j  +  1 ) ... N ) )
166165imaeq2d 5185 . . . . . . . . . . . . . . . . . 18  |-  ( k  =  N  ->  (
( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  =  ( ( 2nd `  s ) " (
( j  +  1 ) ... N ) ) )
167166xpeq1d 4874 . . . . . . . . . . . . . . . . 17  |-  ( k  =  N  ->  (
( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } )  =  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) )
168167uneq2d 3621 . . . . . . . . . . . . . . . 16  |-  ( k  =  N  ->  (
( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) )  =  ( ( ( ( 2nd `  s ) " (
1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )
169168oveq2d 6319 . . . . . . . . . . . . . . 15  |-  ( k  =  N  ->  (
( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  =  ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) ) )
170 oveq1 6310 . . . . . . . . . . . . . . . . 17  |-  ( k  =  N  ->  (
k  +  1 )  =  ( N  + 
1 ) )
171170oveq1d 6318 . . . . . . . . . . . . . . . 16  |-  ( k  =  N  ->  (
( k  +  1 ) ... N )  =  ( ( N  +  1 ) ... N ) )
172171xpeq1d 4874 . . . . . . . . . . . . . . 15  |-  ( k  =  N  ->  (
( ( k  +  1 ) ... N
)  X.  { 0 } )  =  ( ( ( N  + 
1 ) ... N
)  X.  { 0 } ) )
173169, 172uneq12d 3622 . . . . . . . . . . . . . 14  |-  ( k  =  N  ->  (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  =  ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  u.  ( ( ( N  +  1 ) ... N )  X.  {
0 } ) ) )
174173csbeq1d 3403 . . . . . . . . . . . . 13  |-  ( k  =  N  ->  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  u.  ( ( ( N  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
)
175174eqeq2d 2437 . . . . . . . . . . . 12  |-  ( k  =  N  ->  (
i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  u.  ( ( ( N  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
) )
176164, 175rexeqbidv 3041 . . . . . . . . . . 11  |-  ( k  =  N  ->  ( E. j  e.  (
0 ... k ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  E. j  e.  ( 0 ... N
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  u.  ( ( ( N  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
) )
177164, 176raleqbidv 3040 . . . . . . . . . 10  |-  ( k  =  N  ->  ( A. i  e.  (
0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ ( ( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B  <->  A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  u.  ( ( ( N  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B
) )
178163, 177rabeqbidv 3077 . . . . . . . . 9  |-  ( k  =  N  ->  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k
) )  X.  {
f  |  f : ( 1 ... k
)
-1-1-onto-> ( 1 ... k
) } )  | 
A. i  e.  ( 0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B }  =  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  |  A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  u.  ( ( ( N  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } )
179178fveq2d 5883 . . . . . . . 8  |-  ( k  =  N  ->  ( # `
 { s  e.  ( ( ( 0..^ K )  ^m  (
1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } )  |  A. i  e.  ( 0 ... k
) E. j  e.  ( 0 ... k
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) ) )  u.  ( ( ( k  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } )  =  (
# `  { s  e.  ( ( ( 0..^ K )  ^m  (
1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  |  A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  u.  ( ( ( N  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } ) )
180179breq2d 4433 . . . . . . 7  |-  ( k  =  N  ->  (
2  ||  ( # `  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X. 
{ f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k
) } )  | 
A. i  e.  ( 0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B } )  <->  2  ||  ( # `  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  |  A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  u.  ( ( ( N  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } ) ) )
181180notbid 296 . . . . . 6  |-  ( k  =  N  ->  ( -.  2  ||  ( # `  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X.  { f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k ) } )  |  A. i  e.  ( 0 ... k
) E. j  e.  ( 0 ... k
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... k ) )  X.  { 0 } ) ) )  u.  ( ( ( k  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } )  <->  -.  2  ||  ( # `  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X. 
{ f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N
) } )  | 
A. i  e.  ( 0 ... N ) E. j  e.  ( 0 ... N ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... N ) )  X. 
{ 0 } ) ) )  u.  (
( ( N  + 
1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B } ) ) )
182181imbi2d 318 . . . . 5  |-  ( k  =  N  ->  (
( ph  ->  -.  2  ||  ( # `  {
s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... k ) )  X. 
{ f  |  f : ( 1 ... k ) -1-1-onto-> ( 1 ... k
) } )  | 
A. i  e.  ( 0 ... k ) E. j  e.  ( 0 ... k ) i  =  [_ (
( ( 1st `  s
)  oF  +  ( ( ( ( 2nd `  s )
" ( 1 ... j ) )  X. 
{ 1 } )  u.  ( ( ( 2nd `  s )
" ( ( j  +  1 ) ... k ) )  X. 
{ 0 } ) ) )  u.  (
( ( k  +  1 ) ... N
)  X.  { 0 } ) )  /  p ]_ B } ) )  <->  ( ph  ->  -.  2  ||  ( # `  { s  e.  ( ( ( 0..^ K )  ^m  ( 1 ... N ) )  X.  { f  |  f : ( 1 ... N ) -1-1-onto-> ( 1 ... N ) } )  |  A. i  e.  ( 0 ... N
) E. j  e.  ( 0 ... N
) i  =  [_ ( ( ( 1st `  s )  oF  +  ( ( ( ( 2nd `  s
) " ( 1 ... j ) )  X.  { 1 } )  u.  ( ( ( 2nd `  s
) " ( ( j  +  1 ) ... N ) )  X.  { 0 } ) ) )  u.  ( ( ( N  +  1 ) ... N )  X.  {
0 } ) )  /  p ]_ B } ) ) ) )
183 n2dvds1 14347 . . . . . . 7  |-  -.  2  ||  1
184 opex 4683 . . . . . . . . . 10  |-  <. (/) ,  (/) >.  e.  _V
185 hashsng 12550 . . . . . . . . . 10  |-  ( <. (/)
,  (/) >.  e.  _V  ->  ( # `  { <.
(/) ,  (/) >. } )  =  1 )
186184, 185ax-mp 5 . . . . . . . . 9  |-  ( # `  { <. (/) ,  (/) >. } )  =  1
187 nnuz 11196 . . . . . . . . . . . . . . . . 17  |-  NN  =  ( ZZ>= `  1 )
1881, 187syl6eleq 2521 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  N  e.  ( ZZ>= ` 
1 ) )
189 eluzfz1 11808 . . . . . . . . . . . . . . . 16  |-  ( N  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... N
) )
190188, 189syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  1  e.  ( 1 ... N ) )
191 poimirlem28.5 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  K  e.  NN )
192191nnnn0d 10927 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  K  e.  NN0 )
193 0elfz 11891 . . . . . . . . . . . . . . . 16  |-  ( K  e.  NN0  ->  0  e.  ( 0 ... K
) )
194 fconst6g 5787 . . . . . . . . . . . . . . . 16  |-  ( 0  e.  ( 0 ... K )  ->  (
( 1 ... N
)  X.  { 0 } ) : ( 1 ... N ) --> ( 0 ... K
) )
195192, 193, 1943syl 18 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( 1 ... N )  X.  {
0 } ) : ( 1 ... N
) --> ( 0 ... K ) )
19670fvconst2 6133 . . . . . . . . . . . . . . . 16  |-  ( 1  e.  ( 1 ... N )  ->  (
( ( 1 ... N )  X.  {
0 } ) ` 
1 )  =  0 )
197190, 196syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( ( ( 1 ... N )  X. 
{ 0 } ) `
 1 )  =  0 )
198190, 195, 1973jca 1186 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( 1  e.  ( 1 ... N )  /\  ( ( 1 ... N )  X. 
{ 0 } ) : ( 1 ... N ) --> ( 0 ... K )  /\  ( ( ( 1 ... N )  X. 
{ 0 } ) `
 1 )  =  0 ) )
199 nfv 1752 . . . . . . . . . . . . . . . 16  |-  F/ p
( ph  /\  (
1  e.  ( 1 ... N )  /\  ( ( 1 ... N )  X.  {
0 } ) : ( 1 ... N
) --> ( 0 ... K )  /\  (
( ( 1 ... N )  X.  {
0 } ) ` 
1 )  =  0 ) )
200 nfcsb1v 3412 . . . . . . . . . . . . . . . . 17  |-  F/_ p [_ ( ( 1 ... N )  X.  {
0 } )  /  p ]_ B
201200nfeq1 2600 . . . . . . . . . . . . . . . 16  |-  F/ p [_ ( ( 1 ... N )  X.  {
0 } )  /  p ]_ B  =  0
202199, 201nfim 1977 . . . . . . . . . . . . . . 15  |-  F/ p
( ( ph  /\  ( 1  e.  ( 1 ... N )  /\  ( ( 1 ... N )  X. 
{ 0 } ) : ( 1 ... N ) --> ( 0 ... K )  /\  ( ( ( 1 ... N )  X. 
{ 0 } ) `
 1 )  =  0 ) )  ->  [_ ( ( 1 ... N )  X.  {
0 } )  /  p ]_ B  =  0 )
203 ovex 6331 . . . . . . . . . . . . . . . 16  |-  ( 1 ... N )  e. 
_V
204 snex 4660 . . . . . . . . . . . . . . . 16  |-  { 0 }  e.  _V
205203, 204xpex 6607 . . . . . . . . . . . . . . 15  |-  ( ( 1 ... N )  X.  { 0 } )  e.  _V
206 feq1 5726 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( ( 1 ... N )  X. 
{ 0 } )  ->  ( p : ( 1 ... N
) --> ( 0 ... K )  <->  ( (
1 ... N )  X. 
{ 0 } ) : ( 1 ... N ) --> ( 0 ... K ) ) )
207 fveq1 5878 . . . . . . . . . . . . . . . . . . 19  |-  ( p  =  ( ( 1 ... N )  X. 
{ 0 } )  ->  ( p ` 
1 )  =  ( ( ( 1 ... N )  X.  {
0 } ) ` 
1 ) )
208207eqeq1d 2425 . . . . . . . . . . . . . . . . . 18  |-  ( p  =  ( ( 1 ... N )  X. 
{ 0 } )  ->  ( ( p `
 1 )  =  0  <->  ( ( ( 1 ... N )  X.  { 0 } ) `  1 )  =  0 ) )
209206, 2083anbi23d 1339 . . . . . . . . . . . . . . . . 17  |-  ( p  =  ( ( 1 ... N )  X. 
{ 0 } )  ->  ( ( 1  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... K )  /\  ( p `  1
)  =  0 )  <-> 
( 1  e.  ( 1 ... N )  /\  ( ( 1 ... N )  X. 
{ 0 } ) : ( 1 ... N ) --> ( 0 ... K )  /\  ( ( ( 1 ... N )  X. 
{ 0 } ) `
 1 )  =  0 ) ) )
210209anbi2d 709 . . . . . . . . . . . . . . . 16  |-  ( p  =  ( ( 1 ... N )  X. 
{ 0 } )  ->  ( ( ph  /\  ( 1  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... K
)  /\  ( p `  1 )  =  0 ) )  <->  ( ph  /\  ( 1  e.  ( 1 ... N )  /\  ( ( 1 ... N )  X. 
{ 0 } ) : ( 1 ... N ) --> ( 0 ... K )  /\  ( ( ( 1 ... N )  X. 
{ 0 } ) `
 1 )  =  0 ) ) ) )
211 csbeq1a 3405 . . . . . . . . . . . . . . . . 17  |-  ( p  =  ( ( 1 ... N )  X. 
{ 0 } )  ->  B  =  [_ ( ( 1 ... N )  X.  {
0 } )  /  p ]_ B )
212211eqeq1d 2425 . . . . . . . . . . . . . . . 16  |-  ( p  =  ( ( 1 ... N )  X. 
{ 0 } )  ->  ( B  =  0  <->  [_ ( ( 1 ... N )  X. 
{ 0 } )  /  p ]_ B  =  0 ) )
213210, 212imbi12d 322 . . . . . . . . . . . . . . 15  |-  ( p  =  ( ( 1 ... N )  X. 
{ 0 } )  ->  ( ( (
ph  /\  ( 1  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... K )  /\  ( p `  1
)  =  0 ) )  ->  B  = 
0 )  <->  ( ( ph  /\  ( 1  e.  ( 1 ... N
)  /\  ( (
1 ... N )  X. 
{ 0 } ) : ( 1 ... N ) --> ( 0 ... K )  /\  ( ( ( 1 ... N )  X. 
{ 0 } ) `
 1 )  =  0 ) )  ->  [_ ( ( 1 ... N )  X.  {
0 } )  /  p ]_ B  =  0 ) ) )
214 1ex 9640 . . . . . . . . . . . . . . . . 17  |-  1  e.  _V
215 eleq1 2495 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  (
n  e.  ( 1 ... N )  <->  1  e.  ( 1 ... N
) ) )
216 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( n  =  1  ->  (
p `  n )  =  ( p ` 
1 ) )
217216eqeq1d 2425 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  (
( p `  n
)  =  0  <->  (
p `  1 )  =  0 ) )
218215, 2173anbi13d 1338 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
( n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... K
)  /\  ( p `  n )  =  0 )  <->  ( 1  e.  ( 1 ... N
)  /\  p :
( 1 ... N
) --> ( 0 ... K )  /\  (
p `  1 )  =  0 ) ) )
219218anbi2d 709 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
( ph  /\  (
n  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... K )  /\  ( p `  n
)  =  0 ) )  <->  ( ph  /\  ( 1  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... K
)  /\  ( p `  1 )  =  0 ) ) ) )
220 breq2 4425 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  ( B  <  n  <->  B  <  1 ) )
221219, 220imbi12d 322 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  (
( ( ph  /\  ( n  e.  (
1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... K )  /\  ( p `  n
)  =  0 ) )  ->  B  <  n )  <->  ( ( ph  /\  ( 1  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... K
)  /\  ( p `  1 )  =  0 ) )  ->  B  <  1 ) ) )
222 poimirlem28.3 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( n  e.  ( 1 ... N
)  /\  p :
( 1 ... N
) --> ( 0 ... K )  /\  (
p `  n )  =  0 ) )  ->  B  <  n
)
223214, 221, 222vtocl 3134 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( 1  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... K )  /\  ( p `  1
)  =  0 ) )  ->  B  <  1 )
224 poimirlem28.2 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  p :
( 1 ... N
) --> ( 0 ... K ) )  ->  B  e.  ( 0 ... N ) )
225 elfznn0 11889 . . . . . . . . . . . . . . . . . 18  |-  ( B  e.  ( 0 ... N )  ->  B  e.  NN0 )
226 nn0lt10b 11000 . . . . . . . . . . . . . . . . . 18  |-  ( B  e.  NN0  ->  ( B  <  1  <->  B  = 
0 ) )
227224, 225, 2263syl 18 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  p :
( 1 ... N
) --> ( 0 ... K ) )  -> 
( B  <  1  <->  B  =  0 ) )
2282273ad2antr2 1172 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( 1  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... K )  /\  ( p `  1
)  =  0 ) )  ->  ( B  <  1  <->  B  =  0
) )
229223, 228mpbid 214 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( 1  e.  ( 1 ... N )  /\  p : ( 1 ... N ) --> ( 0 ... K )  /\  ( p `  1
)  =  0 ) )  ->  B  = 
0 )
230202, 205, 213, 229vtoclf 3133 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( 1  e.  ( 1 ... N )  /\  (
( 1 ... N
)  X.  { 0 } ) : ( 1 ... N ) --> ( 0 ... K
)  /\  ( (
( 1 ... N
)  X.  { 0 } ) `  1
)  =  0 ) )  ->  [_ ( ( 1 ... N )  X.  { 0 } )  /  p ]_ B  =  0 )
231198, 230mpdan 673 . . . . . . . . . . . . 13  |-  ( ph  ->  [_ ( ( 1 ... N )  X. 
{ 0 } )  /  p ]_ B  =  0 )
232231eqcomd 2431 . . . . . . . . . . . 12  |-  ( ph  ->  0  =  [_ (
( 1 ... N
)  X.  { 0 } )  /  p ]_ B )
233232ralrimivw 2841 . . . . . . . . . . 11  |-  ( ph  ->  A. s  e.  { <.
(/) ,  (/) >. } 0  =  [_ ( ( 1 ... N )  X.  { 0 } )  /  p ]_ B )
234 rabid2 3007 . . . . . . . . . . 11  |-  ( {
<. (/) ,  (/) >. }  =  { s  e.  { <.
(/) ,  (/) >. }  | 
0  =  [_ (
( 1 ... N
)  X.  { 0 } )  /  p ]_ B }  <->  A. s  e.  { <. (/) ,  (/) >. } 0  =  [_ ( ( 1 ... N )  X.  { 0 } )  /  p ]_ B )
235233, 234sylibr 216 . . . . . . . . . 10  |-  ( ph  ->  { <. (/) ,  (/) >. }  =  { s  e.  { <.
(/) ,  (/) >. }  | 
0  =  [_ (
( 1 ... N
)  X.  { 0 } )  /  p ]_ B } )
236235fveq2d 5883 . . . . . . . . 9  |-  ( ph  ->  ( # `  { <.
(/) ,  (/) >. } )  =  ( # `  {
s  e.  { <. (/)
,  (/) >. }  |  0  =  [_ ( ( 1 ... N )  X.  { 0 } )  /  p ]_ B } ) )
237186, 236syl5eqr 2478 . . . . . . . 8  |-  ( ph  ->  1  =  ( # `  { s  e.  { <.
(/) ,  (/) >. }  | 
0  =  [_ (
( 1 ... N
)  X.  { 0 } )  /  p ]_ B } ) )
238237breq2d 4433 . . . . . . 7  |-  ( ph  ->  ( 2  ||  1  <->  2 
||  ( # `  {
s  e.  { <. (/)
,  (/) >. }  |  0  =  [_ ( ( 1 ... N )  X.  { 0 } )  /  p ]_ B } ) ) )
239183, 238mtbii 304 . . . . . 6  |-  ( ph  ->  -.  2  ||  ( # `
 { s  e. 
{ <. (/) ,  (/) >. }  | 
0  =  [_ (
( 1 ... N
)  X.  { 0 } )  /  p ]_ B } ) )
240239a1i 11 . . . . 5  |-  ( N  e.  NN0  ->  ( ph  ->  -.  2  ||  ( # `
 { s  e. 
{ <. (/) ,  (/) >. }