Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  subfacp1lem5 Unicode version

Theorem subfacp1lem5 23730
Description: Lemma for subfacp1 23732. In subfacp1lem6 23731 we cut up the set of all derangements on  1 ... ( N  +  1 ) first according to the value at  1, and then by whether or not  ( f `  ( f `  1
) )  =  1. In this lemma, we show that the subset of all  N  +  1 derangements with  ( f `  ( f `  1
) )  =/=  1 for fixed  M  =  ( f ` 
1 ) is in bijection with derangements of  2 ... ( N  + 
1 ), because pre-composing with the function  F swaps  1 and  M and turns the function into a bijection with  ( f `  1 )  =  1 and  ( f `  x )  =/=  x for all other  x, so dropping the point at  1 yields a derangement on the  N remaining points. (Contributed by Mario Carneiro, 23-Jan-2015.)
Hypotheses
Ref Expression
derang.d  |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y )  =/=  y
) } ) )
subfac.n  |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1 ... n ) ) )
subfacp1lem.a  |-  A  =  { f  |  ( f : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) )  /\  A. y  e.  ( 1 ... ( N  + 
1 ) ) ( f `  y )  =/=  y ) }
subfacp1lem1.n  |-  ( ph  ->  N  e.  NN )
subfacp1lem1.m  |-  ( ph  ->  M  e.  ( 2 ... ( N  + 
1 ) ) )
subfacp1lem1.x  |-  M  e. 
_V
subfacp1lem1.k  |-  K  =  ( ( 2 ... ( N  +  1 ) )  \  { M } )
subfacp1lem5.b  |-  B  =  { g  e.  A  |  ( ( g `
 1 )  =  M  /\  ( g `
 M )  =/=  1 ) }
subfacp1lem5.f  |-  F  =  ( (  _I  |`  K )  u.  { <. 1 ,  M >. ,  <. M , 
1 >. } )
subfacp1lem5.c  |-  C  =  { f  |  ( f : ( 2 ... ( N  + 
1 ) ) -1-1-onto-> ( 2 ... ( N  + 
1 ) )  /\  A. y  e.  ( 2 ... ( N  + 
1 ) ) ( f `  y )  =/=  y ) }
Assertion
Ref Expression
subfacp1lem5  |-  ( ph  ->  ( # `  B
)  =  ( S `
 N ) )
Distinct variable groups:    f, g, n, x, y, A    f, F, g, x, y    f, N, g, n, x, y    B, f, g, x, y   
x, C, y    ph, x, y    D, n    f, K, n, x, y    f, M, g, x, y    S, n, x, y
Allowed substitution hints:    ph( f, g, n)    B( n)    C( f,
g, n)    D( x, y, f, g)    S( f, g)    F( n)    K( g)    M( n)

Proof of Theorem subfacp1lem5
Dummy variables  b 
c are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 subfacp1lem.a . . . . . . . 8  |-  A  =  { f  |  ( f : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) )  /\  A. y  e.  ( 1 ... ( N  + 
1 ) ) ( f `  y )  =/=  y ) }
2 fzfi 11050 . . . . . . . . 9  |-  ( 1 ... ( N  + 
1 ) )  e. 
Fin
3 deranglem 23712 . . . . . . . . 9  |-  ( ( 1 ... ( N  +  1 ) )  e.  Fin  ->  { f  |  ( f : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  /\  A. y  e.  ( 1 ... ( N  +  1 ) ) ( f `  y )  =/=  y
) }  e.  Fin )
42, 3ax-mp 8 . . . . . . . 8  |-  { f  |  ( f : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  /\  A. y  e.  ( 1 ... ( N  +  1 ) ) ( f `  y )  =/=  y
) }  e.  Fin
51, 4eqeltri 2366 . . . . . . 7  |-  A  e. 
Fin
6 subfacp1lem5.b . . . . . . . 8  |-  B  =  { g  e.  A  |  ( ( g `
 1 )  =  M  /\  ( g `
 M )  =/=  1 ) }
7 ssrab2 3271 . . . . . . . 8  |-  { g  e.  A  |  ( ( g `  1
)  =  M  /\  ( g `  M
)  =/=  1 ) }  C_  A
86, 7eqsstri 3221 . . . . . . 7  |-  B  C_  A
9 ssfi 7099 . . . . . . 7  |-  ( ( A  e.  Fin  /\  B  C_  A )  ->  B  e.  Fin )
105, 8, 9mp2an 653 . . . . . 6  |-  B  e. 
Fin
1110elexi 2810 . . . . 5  |-  B  e. 
_V
1211a1i 10 . . . 4  |-  ( ph  ->  B  e.  _V )
13 subfacp1lem5.c . . . . . . 7  |-  C  =  { f  |  ( f : ( 2 ... ( N  + 
1 ) ) -1-1-onto-> ( 2 ... ( N  + 
1 ) )  /\  A. y  e.  ( 2 ... ( N  + 
1 ) ) ( f `  y )  =/=  y ) }
14 fzfi 11050 . . . . . . . 8  |-  ( 2 ... ( N  + 
1 ) )  e. 
Fin
15 deranglem 23712 . . . . . . . 8  |-  ( ( 2 ... ( N  +  1 ) )  e.  Fin  ->  { f  |  ( f : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  /\  A. y  e.  ( 2 ... ( N  +  1 ) ) ( f `  y )  =/=  y
) }  e.  Fin )
1614, 15ax-mp 8 . . . . . . 7  |-  { f  |  ( f : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  /\  A. y  e.  ( 2 ... ( N  +  1 ) ) ( f `  y )  =/=  y
) }  e.  Fin
1713, 16eqeltri 2366 . . . . . 6  |-  C  e. 
Fin
1817elexi 2810 . . . . 5  |-  C  e. 
_V
1918a1i 10 . . . 4  |-  ( ph  ->  C  e.  _V )
20 derang.d . . . . . . . . . . . . 13  |-  D  =  ( x  e.  Fin  |->  ( # `  { f  |  ( f : x -1-1-onto-> x  /\  A. y  e.  x  ( f `  y )  =/=  y
) } ) )
21 subfac.n . . . . . . . . . . . . 13  |-  S  =  ( n  e.  NN0  |->  ( D `  ( 1 ... n ) ) )
22 subfacp1lem1.n . . . . . . . . . . . . 13  |-  ( ph  ->  N  e.  NN )
23 subfacp1lem1.m . . . . . . . . . . . . 13  |-  ( ph  ->  M  e.  ( 2 ... ( N  + 
1 ) ) )
24 subfacp1lem1.x . . . . . . . . . . . . 13  |-  M  e. 
_V
25 subfacp1lem1.k . . . . . . . . . . . . 13  |-  K  =  ( ( 2 ... ( N  +  1 ) )  \  { M } )
26 subfacp1lem5.f . . . . . . . . . . . . 13  |-  F  =  ( (  _I  |`  K )  u.  { <. 1 ,  M >. ,  <. M , 
1 >. } )
27 f1oi 5527 . . . . . . . . . . . . . 14  |-  (  _I  |`  K ) : K -1-1-onto-> K
2827a1i 10 . . . . . . . . . . . . 13  |-  ( ph  ->  (  _I  |`  K ) : K -1-1-onto-> K )
2920, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2a 23726 . . . . . . . . . . . 12  |-  ( ph  ->  ( F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  /\  ( F ` 
1 )  =  M  /\  ( F `  M )  =  1 ) )
3029simp1d 967 . . . . . . . . . . 11  |-  ( ph  ->  F : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) ) )
3130adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  B )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
32 simpr 447 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  b  e.  B )  ->  b  e.  B )
33 fveq1 5540 . . . . . . . . . . . . . . . . 17  |-  ( g  =  b  ->  (
g `  1 )  =  ( b ` 
1 ) )
3433eqeq1d 2304 . . . . . . . . . . . . . . . 16  |-  ( g  =  b  ->  (
( g `  1
)  =  M  <->  ( b `  1 )  =  M ) )
35 fveq1 5540 . . . . . . . . . . . . . . . . 17  |-  ( g  =  b  ->  (
g `  M )  =  ( b `  M ) )
3635neeq1d 2472 . . . . . . . . . . . . . . . 16  |-  ( g  =  b  ->  (
( g `  M
)  =/=  1  <->  (
b `  M )  =/=  1 ) )
3734, 36anbi12d 691 . . . . . . . . . . . . . . 15  |-  ( g  =  b  ->  (
( ( g ` 
1 )  =  M  /\  ( g `  M )  =/=  1
)  <->  ( ( b `
 1 )  =  M  /\  ( b `
 M )  =/=  1 ) ) )
3837, 6elrab2 2938 . . . . . . . . . . . . . 14  |-  ( b  e.  B  <->  ( b  e.  A  /\  (
( b `  1
)  =  M  /\  ( b `  M
)  =/=  1 ) ) )
3932, 38sylib 188 . . . . . . . . . . . . 13  |-  ( (
ph  /\  b  e.  B )  ->  (
b  e.  A  /\  ( ( b ` 
1 )  =  M  /\  ( b `  M )  =/=  1
) ) )
4039simpld 445 . . . . . . . . . . . 12  |-  ( (
ph  /\  b  e.  B )  ->  b  e.  A )
41 vex 2804 . . . . . . . . . . . . 13  |-  b  e. 
_V
42 f1oeq1 5479 . . . . . . . . . . . . . 14  |-  ( f  =  b  ->  (
f : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) )  <->  b :
( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) ) )
43 fveq1 5540 . . . . . . . . . . . . . . . 16  |-  ( f  =  b  ->  (
f `  y )  =  ( b `  y ) )
4443neeq1d 2472 . . . . . . . . . . . . . . 15  |-  ( f  =  b  ->  (
( f `  y
)  =/=  y  <->  ( b `  y )  =/=  y
) )
4544ralbidv 2576 . . . . . . . . . . . . . 14  |-  ( f  =  b  ->  ( A. y  e.  (
1 ... ( N  + 
1 ) ) ( f `  y )  =/=  y  <->  A. y  e.  ( 1 ... ( N  +  1 ) ) ( b `  y )  =/=  y
) )
4642, 45anbi12d 691 . . . . . . . . . . . . 13  |-  ( f  =  b  ->  (
( f : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  /\  A. y  e.  ( 1 ... ( N  +  1 ) ) ( f `  y )  =/=  y
)  <->  ( b : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  /\  A. y  e.  ( 1 ... ( N  +  1 ) ) ( b `  y )  =/=  y
) ) )
4741, 46, 1elab2 2930 . . . . . . . . . . . 12  |-  ( b  e.  A  <->  ( b : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  /\  A. y  e.  ( 1 ... ( N  +  1 ) ) ( b `  y )  =/=  y
) )
4840, 47sylib 188 . . . . . . . . . . 11  |-  ( (
ph  /\  b  e.  B )  ->  (
b : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) )  /\  A. y  e.  ( 1 ... ( N  + 
1 ) ) ( b `  y )  =/=  y ) )
4948simpld 445 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  B )  ->  b : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
50 f1oco 5512 . . . . . . . . . 10  |-  ( ( F : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) )  /\  b : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )  ->  ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
5131, 49, 50syl2anc 642 . . . . . . . . 9  |-  ( (
ph  /\  b  e.  B )  ->  ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
52 f1of1 5487 . . . . . . . . 9  |-  ( ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  ( F  o.  b ) : ( 1 ... ( N  +  1 ) )
-1-1-> ( 1 ... ( N  +  1 ) ) )
53 df-f1 5276 . . . . . . . . . 10  |-  ( ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) -1-1-> ( 1 ... ( N  + 
1 ) )  <->  ( ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) )  /\  Fun  `' ( F  o.  b ) ) )
5453simprbi 450 . . . . . . . . 9  |-  ( ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) -1-1-> ( 1 ... ( N  + 
1 ) )  ->  Fun  `' ( F  o.  b ) )
5551, 52, 543syl 18 . . . . . . . 8  |-  ( (
ph  /\  b  e.  B )  ->  Fun  `' ( F  o.  b
) )
56 f1ofn 5489 . . . . . . . . . . . 12  |-  ( ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  ( F  o.  b )  Fn  (
1 ... ( N  + 
1 ) ) )
57 fnresdm 5369 . . . . . . . . . . . 12  |-  ( ( F  o.  b )  Fn  ( 1 ... ( N  +  1 ) )  ->  (
( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) )  =  ( F  o.  b
) )
5851, 56, 573syl 18 . . . . . . . . . . 11  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) )  =  ( F  o.  b
) )
59 f1oeq1 5479 . . . . . . . . . . 11  |-  ( ( ( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) )  =  ( F  o.  b
)  ->  ( (
( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  <->  ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) ) )
6058, 59syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  B )  ->  (
( ( F  o.  b )  |`  (
1 ... ( N  + 
1 ) ) ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  <->  ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) ) )
6151, 60mpbird 223 . . . . . . . . 9  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
62 f1ofo 5495 . . . . . . . . 9  |-  ( ( ( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  ( ( F  o.  b )  |`  ( 1 ... ( N  +  1 ) ) ) : ( 1 ... ( N  +  1 ) )
-onto-> ( 1 ... ( N  +  1 ) ) )
6361, 62syl 15 . . . . . . . 8  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) ) : ( 1 ... ( N  +  1 ) ) -onto-> ( 1 ... ( N  +  1 ) ) )
64 1ex 8849 . . . . . . . . . . 11  |-  1  e.  _V
6564, 64f1osn 5529 . . . . . . . . . 10  |-  { <. 1 ,  1 >. } : { 1 } -1-1-onto-> { 1 }
6651, 56syl 15 . . . . . . . . . . . . 13  |-  ( (
ph  /\  b  e.  B )  ->  ( F  o.  b )  Fn  ( 1 ... ( N  +  1 ) ) )
6722peano2nnd 9779 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  1 )  e.  NN )
68 nnuz 10279 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
6967, 68syl6eleq 2386 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
1 ) )
70 eluzfz1 10819 . . . . . . . . . . . . . . 15  |-  ( ( N  +  1 )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( N  +  1 ) ) )
7169, 70syl 15 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  e.  ( 1 ... ( N  + 
1 ) ) )
7271adantr 451 . . . . . . . . . . . . 13  |-  ( (
ph  /\  b  e.  B )  ->  1  e.  ( 1 ... ( N  +  1 ) ) )
73 fnressn 5721 . . . . . . . . . . . . 13  |-  ( ( ( F  o.  b
)  Fn  ( 1 ... ( N  + 
1 ) )  /\  1  e.  ( 1 ... ( N  + 
1 ) ) )  ->  ( ( F  o.  b )  |`  { 1 } )  =  { <. 1 ,  ( ( F  o.  b ) ` 
1 ) >. } )
7466, 72, 73syl2anc 642 . . . . . . . . . . . 12  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  { 1 } )  =  { <. 1 ,  ( ( F  o.  b ) `  1 ) >. } )
75 f1of 5488 . . . . . . . . . . . . . . . . 17  |-  ( b : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  b :
( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) ) )
7649, 75syl 15 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  b  e.  B )  ->  b : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
77 fvco3 5612 . . . . . . . . . . . . . . . 16  |-  ( ( b : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  1  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( ( F  o.  b ) `  1 )  =  ( F `  (
b `  1 )
) )
7876, 72, 77syl2anc 642 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
) `  1 )  =  ( F `  ( b `  1
) ) )
7939simprd 449 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  b  e.  B )  ->  (
( b `  1
)  =  M  /\  ( b `  M
)  =/=  1 ) )
8079simpld 445 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  b  e.  B )  ->  (
b `  1 )  =  M )
8180fveq2d 5545 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  B )  ->  ( F `  ( b `  1 ) )  =  ( F `  M ) )
8229simp3d 969 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F `  M
)  =  1 )
8382adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  B )  ->  ( F `  M )  =  1 )
8478, 81, 833eqtrd 2332 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
) `  1 )  =  1 )
8584opeq2d 3819 . . . . . . . . . . . . 13  |-  ( (
ph  /\  b  e.  B )  ->  <. 1 ,  ( ( F  o.  b ) ` 
1 ) >.  =  <. 1 ,  1 >. )
8685sneqd 3666 . . . . . . . . . . . 12  |-  ( (
ph  /\  b  e.  B )  ->  { <. 1 ,  ( ( F  o.  b ) `  1 ) >. }  =  { <. 1 ,  1 >. } )
8774, 86eqtrd 2328 . . . . . . . . . . 11  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  { 1 } )  =  { <. 1 ,  1 >. } )
88 f1oeq1 5479 . . . . . . . . . . 11  |-  ( ( ( F  o.  b
)  |`  { 1 } )  =  { <. 1 ,  1 >. }  ->  ( ( ( F  o.  b )  |`  { 1 } ) : { 1 } -1-1-onto-> { 1 }  <->  { <. 1 ,  1 >. } : { 1 } -1-1-onto-> { 1 } ) )
8987, 88syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  B )  ->  (
( ( F  o.  b )  |`  { 1 } ) : {
1 } -1-1-onto-> { 1 }  <->  { <. 1 ,  1 >. } : { 1 } -1-1-onto-> { 1 } ) )
9065, 89mpbiri 224 . . . . . . . . 9  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  { 1 } ) : { 1 } -1-1-onto-> { 1 } )
91 f1ofo 5495 . . . . . . . . 9  |-  ( ( ( F  o.  b
)  |`  { 1 } ) : { 1 } -1-1-onto-> { 1 }  ->  ( ( F  o.  b
)  |`  { 1 } ) : { 1 } -onto-> { 1 } )
9290, 91syl 15 . . . . . . . 8  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  { 1 } ) : { 1 } -onto-> { 1 } )
93 resdif 5510 . . . . . . . 8  |-  ( ( Fun  `' ( F  o.  b )  /\  ( ( F  o.  b )  |`  (
1 ... ( N  + 
1 ) ) ) : ( 1 ... ( N  +  1 ) ) -onto-> ( 1 ... ( N  + 
1 ) )  /\  ( ( F  o.  b )  |`  { 1 } ) : {
1 } -onto-> { 1 } )  ->  (
( F  o.  b
)  |`  ( ( 1 ... ( N  + 
1 ) )  \  { 1 } ) ) : ( ( 1 ... ( N  +  1 ) ) 
\  { 1 } ) -1-1-onto-> ( ( 1 ... ( N  +  1 ) )  \  {
1 } ) )
9455, 63, 92, 93syl3anc 1182 . . . . . . 7  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( ( 1 ... ( N  + 
1 ) )  \  { 1 } ) ) : ( ( 1 ... ( N  +  1 ) ) 
\  { 1 } ) -1-1-onto-> ( ( 1 ... ( N  +  1 ) )  \  {
1 } ) )
95 fzsplit 10832 . . . . . . . . . . . 12  |-  ( 1  e.  ( 1 ... ( N  +  1 ) )  ->  (
1 ... ( N  + 
1 ) )  =  ( ( 1 ... 1 )  u.  (
( 1  +  1 ) ... ( N  +  1 ) ) ) )
9671, 95syl 15 . . . . . . . . . . 11  |-  ( ph  ->  ( 1 ... ( N  +  1 ) )  =  ( ( 1 ... 1 )  u.  ( ( 1  +  1 ) ... ( N  +  1 ) ) ) )
97 1z 10069 . . . . . . . . . . . . 13  |-  1  e.  ZZ
98 fzsn 10849 . . . . . . . . . . . . 13  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
9997, 98ax-mp 8 . . . . . . . . . . . 12  |-  ( 1 ... 1 )  =  { 1 }
100 1p1e2 9856 . . . . . . . . . . . . 13  |-  ( 1  +  1 )  =  2
101100oveq1i 5884 . . . . . . . . . . . 12  |-  ( ( 1  +  1 ) ... ( N  + 
1 ) )  =  ( 2 ... ( N  +  1 ) )
10299, 101uneq12i 3340 . . . . . . . . . . 11  |-  ( ( 1 ... 1 )  u.  ( ( 1  +  1 ) ... ( N  +  1 ) ) )  =  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )
10396, 102syl6req 2345 . . . . . . . . . 10  |-  ( ph  ->  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  =  ( 1 ... ( N  +  1 ) ) )
10471snssd 3776 . . . . . . . . . . 11  |-  ( ph  ->  { 1 }  C_  ( 1 ... ( N  +  1 ) ) )
105 incom 3374 . . . . . . . . . . . 12  |-  ( { 1 }  i^i  (
2 ... ( N  + 
1 ) ) )  =  ( ( 2 ... ( N  + 
1 ) )  i^i 
{ 1 } )
106 1lt2 9902 . . . . . . . . . . . . . . 15  |-  1  <  2
107 1re 8853 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
108 2re 9831 . . . . . . . . . . . . . . . 16  |-  2  e.  RR
109107, 108ltnlei 8955 . . . . . . . . . . . . . . 15  |-  ( 1  <  2  <->  -.  2  <_  1 )
110106, 109mpbi 199 . . . . . . . . . . . . . 14  |-  -.  2  <_  1
111 elfzle1 10815 . . . . . . . . . . . . . 14  |-  ( 1  e.  ( 2 ... ( N  +  1 ) )  ->  2  <_  1 )
112110, 111mto 167 . . . . . . . . . . . . 13  |-  -.  1  e.  ( 2 ... ( N  +  1 ) )
113 disjsn 3706 . . . . . . . . . . . . 13  |-  ( ( ( 2 ... ( N  +  1 ) )  i^i  { 1 } )  =  (/)  <->  -.  1  e.  ( 2 ... ( N  + 
1 ) ) )
114112, 113mpbir 200 . . . . . . . . . . . 12  |-  ( ( 2 ... ( N  +  1 ) )  i^i  { 1 } )  =  (/)
115105, 114eqtri 2316 . . . . . . . . . . 11  |-  ( { 1 }  i^i  (
2 ... ( N  + 
1 ) ) )  =  (/)
116 uneqdifeq 3555 . . . . . . . . . . 11  |-  ( ( { 1 }  C_  ( 1 ... ( N  +  1 ) )  /\  ( { 1 }  i^i  (
2 ... ( N  + 
1 ) ) )  =  (/) )  ->  (
( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  =  ( 1 ... ( N  +  1 ) )  <->  ( ( 1 ... ( N  + 
1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) ) ) )
117104, 115, 116sylancl 643 . . . . . . . . . 10  |-  ( ph  ->  ( ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) )  =  ( 1 ... ( N  +  1 ) )  <->  ( (
1 ... ( N  + 
1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) ) ) )
118103, 117mpbid 201 . . . . . . . . 9  |-  ( ph  ->  ( ( 1 ... ( N  +  1 ) )  \  {
1 } )  =  ( 2 ... ( N  +  1 ) ) )
119118adantr 451 . . . . . . . 8  |-  ( (
ph  /\  b  e.  B )  ->  (
( 1 ... ( N  +  1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) ) )
120 reseq2 4966 . . . . . . . . . 10  |-  ( ( ( 1 ... ( N  +  1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) )  ->  ( ( F  o.  b )  |`  ( ( 1 ... ( N  +  1 ) )  \  {
1 } ) )  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) )
121 f1oeq1 5479 . . . . . . . . . 10  |-  ( ( ( F  o.  b
)  |`  ( ( 1 ... ( N  + 
1 ) )  \  { 1 } ) )  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  ->  (
( ( F  o.  b )  |`  (
( 1 ... ( N  +  1 ) )  \  { 1 } ) ) : ( ( 1 ... ( N  +  1 ) )  \  {
1 } ) -1-1-onto-> ( ( 1 ... ( N  +  1 ) ) 
\  { 1 } )  <->  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) : ( ( 1 ... ( N  +  1 ) )  \  { 1 } ) -1-1-onto-> ( ( 1 ... ( N  +  1 ) )  \  {
1 } ) ) )
122120, 121syl 15 . . . . . . . . 9  |-  ( ( ( 1 ... ( N  +  1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) )  ->  ( ( ( F  o.  b )  |`  ( ( 1 ... ( N  +  1 ) )  \  {
1 } ) ) : ( ( 1 ... ( N  + 
1 ) )  \  { 1 } ) -1-1-onto-> ( ( 1 ... ( N  +  1 ) )  \  { 1 } )  <->  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) : ( ( 1 ... ( N  +  1 ) )  \  { 1 } ) -1-1-onto-> ( ( 1 ... ( N  +  1 ) )  \  {
1 } ) ) )
123 f1oeq2 5480 . . . . . . . . 9  |-  ( ( ( 1 ... ( N  +  1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) )  ->  ( ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) : ( ( 1 ... ( N  +  1 ) )  \  { 1 } ) -1-1-onto-> ( ( 1 ... ( N  +  1 ) )  \  {
1 } )  <->  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( ( 1 ... ( N  +  1 ) )  \  { 1 } ) ) )
124 f1oeq3 5481 . . . . . . . . 9  |-  ( ( ( 1 ... ( N  +  1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) )  ->  ( ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( ( 1 ... ( N  +  1 ) )  \  { 1 } )  <->  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) ) )
125122, 123, 1243bitrd 270 . . . . . . . 8  |-  ( ( ( 1 ... ( N  +  1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) )  ->  ( ( ( F  o.  b )  |`  ( ( 1 ... ( N  +  1 ) )  \  {
1 } ) ) : ( ( 1 ... ( N  + 
1 ) )  \  { 1 } ) -1-1-onto-> ( ( 1 ... ( N  +  1 ) )  \  { 1 } )  <->  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) ) )
126119, 125syl 15 . . . . . . 7  |-  ( (
ph  /\  b  e.  B )  ->  (
( ( F  o.  b )  |`  (
( 1 ... ( N  +  1 ) )  \  { 1 } ) ) : ( ( 1 ... ( N  +  1 ) )  \  {
1 } ) -1-1-onto-> ( ( 1 ... ( N  +  1 ) ) 
\  { 1 } )  <->  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) ) )
12794, 126mpbid 201 . . . . . 6  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 2 ... ( N  +  1 ) ) ) : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) )
12876adantr 451 . . . . . . . . 9  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  b : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
129 fzp1ss 10853 . . . . . . . . . . . 12  |-  ( 1  e.  ZZ  ->  (
( 1  +  1 ) ... ( N  +  1 ) ) 
C_  ( 1 ... ( N  +  1 ) ) )
13097, 129ax-mp 8 . . . . . . . . . . 11  |-  ( ( 1  +  1 ) ... ( N  + 
1 ) )  C_  ( 1 ... ( N  +  1 ) )
131101, 130eqsstr3i 3222 . . . . . . . . . 10  |-  ( 2 ... ( N  + 
1 ) )  C_  ( 1 ... ( N  +  1 ) )
132 simpr 447 . . . . . . . . . 10  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  y  e.  ( 2 ... ( N  +  1 ) ) )
133131, 132sseldi 3191 . . . . . . . . 9  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  y  e.  ( 1 ... ( N  +  1 ) ) )
134 fvco3 5612 . . . . . . . . 9  |-  ( ( b : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( ( F  o.  b ) `  y )  =  ( F `  ( b `
 y ) ) )
135128, 133, 134syl2anc 642 . . . . . . . 8  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( F  o.  b
) `  y )  =  ( F `  ( b `  y
) ) )
13620, 21, 1, 22, 23, 24, 25, 6, 26subfacp1lem4 23729 . . . . . . . . . . . 12  |-  ( ph  ->  `' F  =  F
)
137136fveq1d 5543 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F `  y )  =  ( F `  y ) )
138137ad2antrr 706 . . . . . . . . . 10  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( `' F `  y )  =  ( F `  y ) )
13979simprd 449 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  B )  ->  (
b `  M )  =/=  1 )
140139, 83neeqtrrd 2483 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  b  e.  B )  ->  (
b `  M )  =/=  ( F `  M
) )
141140adantr 451 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
b `  M )  =/=  ( F `  M
) )
142 fveq2 5541 . . . . . . . . . . . . . 14  |-  ( y  =  M  ->  (
b `  y )  =  ( b `  M ) )
143 fveq2 5541 . . . . . . . . . . . . . 14  |-  ( y  =  M  ->  ( F `  y )  =  ( F `  M ) )
144142, 143neeq12d 2474 . . . . . . . . . . . . 13  |-  ( y  =  M  ->  (
( b `  y
)  =/=  ( F `
 y )  <->  ( b `  M )  =/=  ( F `  M )
) )
145141, 144syl5ibrcom 213 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
y  =  M  -> 
( b `  y
)  =/=  ( F `
 y ) ) )
146131sseli 3189 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 2 ... ( N  +  1 ) )  ->  y  e.  ( 1 ... ( N  +  1 ) ) )
14748simprd 449 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  b  e.  B )  ->  A. y  e.  ( 1 ... ( N  +  1 ) ) ( b `  y )  =/=  y
)
148147r19.21bi 2654 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
b `  y )  =/=  y )
149146, 148sylan2 460 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
b `  y )  =/=  y )
150149adantrr 697 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  b  e.  B )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( b `  y )  =/=  y
)
15125eleq2i 2360 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  K  <->  y  e.  ( ( 2 ... ( N  +  1 ) )  \  { M } ) )
152 eldifsn 3762 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( ( 2 ... ( N  + 
1 ) )  \  { M } )  <->  ( y  e.  ( 2 ... ( N  +  1 ) )  /\  y  =/= 
M ) )
153151, 152bitri 240 . . . . . . . . . . . . . . . 16  |-  ( y  e.  K  <->  ( y  e.  ( 2 ... ( N  +  1 ) )  /\  y  =/= 
M ) )
15420, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2b 23727 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  K )  ->  ( F `  y )  =  ( (  _I  |`  K ) `  y
) )
155 fvresi 5727 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  K  ->  (
(  _I  |`  K ) `
 y )  =  y )
156155adantl 452 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  K )  ->  (
(  _I  |`  K ) `
 y )  =  y )
157154, 156eqtrd 2328 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  K )  ->  ( F `  y )  =  y )
158153, 157sylan2br 462 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  ( 2 ... ( N  +  1 ) )  /\  y  =/= 
M ) )  -> 
( F `  y
)  =  y )
159158adantlr 695 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  b  e.  B )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( F `  y )  =  y )
160150, 159neeqtrrd 2483 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  b  e.  B )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( b `  y )  =/=  ( F `  y )
)
161160expr 598 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
y  =/=  M  -> 
( b `  y
)  =/=  ( F `
 y ) ) )
162145, 161pm2.61dne 2536 . . . . . . . . . . 11  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
b `  y )  =/=  ( F `  y
) )
163162necomd 2542 . . . . . . . . . 10  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( F `  y )  =/=  ( b `  y
) )
164138, 163eqnetrd 2477 . . . . . . . . 9  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( `' F `  y )  =/=  ( b `  y ) )
16531adantr 451 . . . . . . . . . . 11  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
166 ffvelrn 5679 . . . . . . . . . . . 12  |-  ( ( b : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( b `  y )  e.  ( 1 ... ( N  +  1 ) ) )
16776, 146, 166syl2an 463 . . . . . . . . . . 11  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
b `  y )  e.  ( 1 ... ( N  +  1 ) ) )
168 f1ocnvfv 5810 . . . . . . . . . . 11  |-  ( ( F : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) )  /\  ( b `  y
)  e.  ( 1 ... ( N  + 
1 ) ) )  ->  ( ( F `
 ( b `  y ) )  =  y  ->  ( `' F `  y )  =  ( b `  y ) ) )
169165, 167, 168syl2anc 642 . . . . . . . . . 10  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( F `  (
b `  y )
)  =  y  -> 
( `' F `  y )  =  ( b `  y ) ) )
170169necon3d 2497 . . . . . . . . 9  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( `' F `  y )  =/=  (
b `  y )  ->  ( F `  (
b `  y )
)  =/=  y ) )
171164, 170mpd 14 . . . . . . . 8  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( F `  ( b `  y ) )  =/=  y )
172135, 171eqnetrd 2477 . . . . . . 7  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( F  o.  b
) `  y )  =/=  y )
173172ralrimiva 2639 . . . . . 6  |-  ( (
ph  /\  b  e.  B )  ->  A. y  e.  ( 2 ... ( N  +  1 ) ) ( ( F  o.  b ) `  y )  =/=  y
)
174 f1of 5488 . . . . . . . . . . . . 13  |-  ( (  _I  |`  K ) : K -1-1-onto-> K  ->  (  _I  |`  K ) : K --> K )
17527, 174ax-mp 8 . . . . . . . . . . . 12  |-  (  _I  |`  K ) : K --> K
176 difexg 4178 . . . . . . . . . . . . . 14  |-  ( ( 2 ... ( N  +  1 ) )  e.  Fin  ->  (
( 2 ... ( N  +  1 ) )  \  { M } )  e.  _V )
17714, 176ax-mp 8 . . . . . . . . . . . . 13  |-  ( ( 2 ... ( N  +  1 ) ) 
\  { M }
)  e.  _V
17825, 177eqeltri 2366 . . . . . . . . . . . 12  |-  K  e. 
_V
179 fex 5765 . . . . . . . . . . . 12  |-  ( ( (  _I  |`  K ) : K --> K  /\  K  e.  _V )  ->  (  _I  |`  K )  e.  _V )
180175, 178, 179mp2an 653 . . . . . . . . . . 11  |-  (  _I  |`  K )  e.  _V
181 prex 4233 . . . . . . . . . . 11  |-  { <. 1 ,  M >. , 
<. M ,  1 >. }  e.  _V
182180, 181unex 4534 . . . . . . . . . 10  |-  ( (  _I  |`  K )  u.  { <. 1 ,  M >. ,  <. M ,  1
>. } )  e.  _V
18326, 182eqeltri 2366 . . . . . . . . 9  |-  F  e. 
_V
184183, 41coex 5232 . . . . . . . 8  |-  ( F  o.  b )  e. 
_V
185184resex 5011 . . . . . . 7  |-  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  e.  _V
186 f1oeq1 5479 . . . . . . . 8  |-  ( f  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  ->  (
f : ( 2 ... ( N  + 
1 ) ) -1-1-onto-> ( 2 ... ( N  + 
1 ) )  <->  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) ) )
187 fveq1 5540 . . . . . . . . . . 11  |-  ( f  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  ->  (
f `  y )  =  ( ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) `  y
) )
188 fvres 5558 . . . . . . . . . . 11  |-  ( y  e.  ( 2 ... ( N  +  1 ) )  ->  (
( ( F  o.  b )  |`  (
2 ... ( N  + 
1 ) ) ) `
 y )  =  ( ( F  o.  b ) `  y
) )
189187, 188sylan9eq 2348 . . . . . . . . . 10  |-  ( ( f  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
f `  y )  =  ( ( F  o.  b ) `  y ) )
190189neeq1d 2472 . . . . . . . . 9  |-  ( ( f  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( f `  y
)  =/=  y  <->  ( ( F  o.  b ) `  y )  =/=  y
) )
191190ralbidva 2572 . . . . . . . 8  |-  ( f  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  ->  ( A. y  e.  (
2 ... ( N  + 
1 ) ) ( f `  y )  =/=  y  <->  A. y  e.  ( 2 ... ( N  +  1 ) ) ( ( F  o.  b ) `  y )  =/=  y
) )
192186, 191anbi12d 691 . . . . . . 7  |-  ( f  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  ->  (
( f : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  /\  A. y  e.  ( 2 ... ( N  +  1 ) ) ( f `  y )  =/=  y
)  <->  ( ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  /\  A. y  e.  ( 2 ... ( N  +  1 ) ) ( ( F  o.  b ) `  y )  =/=  y
) ) )
193185, 192, 13elab2 2930 . . . . . 6  |-  ( ( ( F  o.  b
)  |`  ( 2 ... ( N  +  1 ) ) )  e.  C  <->  ( ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  /\  A. y  e.  ( 2 ... ( N  +  1 ) ) ( ( F  o.  b ) `  y )  =/=  y
) )
194127, 173, 193sylanbrc 645 . . . . 5  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 2 ... ( N  +  1 ) ) )  e.  C )
195194ex 423 . . . 4  |-  ( ph  ->  ( b  e.  B  ->  ( ( F  o.  b )  |`  (
2 ... ( N  + 
1 ) ) )  e.  C ) )
19630adantr 451 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
197 simpr 447 . . . . . . . . . . . 12  |-  ( (
ph  /\  c  e.  C )  ->  c  e.  C )
198 vex 2804 . . . . . . . . . . . . 13  |-  c  e. 
_V
199 f1oeq1 5479 . . . . . . . . . . . . . 14  |-  ( f  =  c  ->  (
f : ( 2 ... ( N  + 
1 ) ) -1-1-onto-> ( 2 ... ( N  + 
1 ) )  <->  c :
( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) ) )
200 fveq1 5540 . . . . . . . . . . . . . . . 16  |-  ( f  =  c  ->  (
f `  y )  =  ( c `  y ) )
201200neeq1d 2472 . . . . . . . . . . . . . . 15  |-  ( f  =  c  ->  (
( f `  y
)  =/=  y  <->  ( c `  y )  =/=  y
) )
202201ralbidv 2576 . . . . . . . . . . . . . 14  |-  ( f  =  c  ->  ( A. y  e.  (
2 ... ( N  + 
1 ) ) ( f `  y )  =/=  y  <->  A. y  e.  ( 2 ... ( N  +  1 ) ) ( c `  y )  =/=  y
) )
203199, 202anbi12d 691 . . . . . . . . . . . . 13  |-  ( f  =  c  ->  (
( f : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  /\  A. y  e.  ( 2 ... ( N  +  1 ) ) ( f `  y )  =/=  y
)  <->  ( c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  /\  A. y  e.  ( 2 ... ( N  +  1 ) ) ( c `  y )  =/=  y
) ) )
204198, 203, 13elab2 2930 . . . . . . . . . . . 12  |-  ( c  e.  C  <->  ( c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  /\  A. y  e.  ( 2 ... ( N  +  1 ) ) ( c `  y )  =/=  y
) )
205197, 204sylib 188 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  (
c : ( 2 ... ( N  + 
1 ) ) -1-1-onto-> ( 2 ... ( N  + 
1 ) )  /\  A. y  e.  ( 2 ... ( N  + 
1 ) ) ( c `  y )  =/=  y ) )
206205simpld 445 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) )
207 f1oun 5508 . . . . . . . . . . 11  |-  ( ( ( { <. 1 ,  1 >. } : { 1 } -1-1-onto-> { 1 }  /\  c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) )  /\  (
( { 1 }  i^i  ( 2 ... ( N  +  1 ) ) )  =  (/)  /\  ( { 1 }  i^i  ( 2 ... ( N  + 
1 ) ) )  =  (/) ) )  -> 
( { <. 1 ,  1 >. }  u.  c ) : ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) -1-1-onto-> ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) )
208115, 115, 207mpanr12 666 . . . . . . . . . 10  |-  ( ( { <. 1 ,  1
>. } : { 1 } -1-1-onto-> { 1 }  /\  c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) )  ->  ( { <. 1 ,  1
>. }  u.  c ) : ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) ) -1-1-onto-> ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) )
20965, 206, 208sylancr 644 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  ( { <. 1 ,  1
>. }  u.  c ) : ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) ) -1-1-onto-> ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) )
210 f1oeq2 5480 . . . . . . . . . . . 12  |-  ( ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  =  ( 1 ... ( N  +  1 ) )  ->  ( ( {
<. 1 ,  1
>. }  u.  c ) : ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) ) -1-1-onto-> ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  <->  ( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) ) )
211 f1oeq3 5481 . . . . . . . . . . . 12  |-  ( ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  =  ( 1 ... ( N  +  1 ) )  ->  ( ( {
<. 1 ,  1
>. }  u.  c ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  <->  ( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) ) )
212210, 211bitrd 244 . . . . . . . . . . 11  |-  ( ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  =  ( 1 ... ( N  +  1 ) )  ->  ( ( {
<. 1 ,  1
>. }  u.  c ) : ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) ) -1-1-onto-> ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  <->  ( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) ) )
213103, 212syl 15 . . . . . . . . . 10  |-  ( ph  ->  ( ( { <. 1 ,  1 >. }  u.  c ) : ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) -1-1-onto-> ( { 1 }  u.  (
2 ... ( N  + 
1 ) ) )  <-> 
( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) ) )
214213biimpa 470 . . . . . . . . 9  |-  ( (
ph  /\  ( { <. 1 ,  1 >. }  u.  c ) : ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) ) -1-1-onto-> ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) )  -> 
( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
215209, 214syldan 456 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  ( { <. 1 ,  1
>. }  u.  c ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
216 f1oco 5512 . . . . . . . 8  |-  ( ( F : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) )  /\  ( { <. 1 ,  1
>. }  u.  c ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )  ->  ( F  o.  ( { <. 1 ,  1 >. }  u.  c )
) : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) ) )
217196, 215, 216syl2anc 642 . . . . . . 7  |-  ( (
ph  /\  c  e.  C )  ->  ( F  o.  ( { <. 1 ,  1 >. }  u.  c )
) : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) ) )
218 f1of 5488 . . . . . . . . . . 11  |-  ( ( { <. 1 ,  1
>. }  u.  c ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  ( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
219215, 218syl 15 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  ( { <. 1 ,  1
>. }  u.  c ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
220 fvco3 5612 . . . . . . . . . 10  |-  ( ( ( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  y )  =  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) ) )
221219, 220sylan 457 . . . . . . . . 9  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  y )  =  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) ) )
222137ad2antrr 706 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( `' F `  y )  =  ( F `  y ) )
223 simpr 447 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  y  e.  ( 1 ... ( N  +  1 ) ) )
224103ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  =  ( 1 ... ( N  +  1 ) ) )
225223, 224eleqtrrd 2373 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  y  e.  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) )
226 elun 3329 . . . . . . . . . . . . 13  |-  ( y  e.  ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) )  <-> 
( y  e.  {
1 }  \/  y  e.  ( 2 ... ( N  +  1 ) ) ) )
227225, 226sylib 188 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
y  e.  { 1 }  \/  y  e.  ( 2 ... ( N  +  1 ) ) ) )
228 nelne2 2549 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  e.  ( 2 ... ( N  + 
1 ) )  /\  -.  1  e.  (
2 ... ( N  + 
1 ) ) )  ->  M  =/=  1
)
22923, 112, 228sylancl 643 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  =/=  1 )
230229adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  C )  ->  M  =/=  1 )
23129simp2d 968 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( F `  1
)  =  M )
232231adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  1 )  =  M )
233 f1ofun 5490 . . . . . . . . . . . . . . . . . . 19  |-  ( ( { <. 1 ,  1
>. }  u.  c ) : ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) ) -1-1-onto-> ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  ->  Fun  ( { <. 1 ,  1
>. }  u.  c ) )
234209, 233syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  c  e.  C )  ->  Fun  ( { <. 1 ,  1
>. }  u.  c ) )
235 ssun1 3351 . . . . . . . . . . . . . . . . . . 19  |-  { <. 1 ,  1 >. } 
C_  ( { <. 1 ,  1 >. }  u.  c )
23664snid 3680 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  { 1 }
23764dmsnop 5163 . . . . . . . . . . . . . . . . . . . 20  |-  dom  { <. 1 ,  1 >. }  =  { 1 }
238236, 237eleqtrri 2369 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  dom  { <. 1 ,  1 >. }
239 funssfv 5559 . . . . . . . . . . . . . . . . . . 19  |-  ( ( Fun  ( { <. 1 ,  1 >. }  u.  c )  /\  {
<. 1 ,  1
>. }  C_  ( { <. 1 ,  1 >. }  u.  c )  /\  1  e.  dom  {
<. 1 ,  1
>. } )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  1
)  =  ( {
<. 1 ,  1
>. } `  1 ) )
240235, 238, 239mp3an23 1269 . . . . . . . . . . . . . . . . . 18  |-  ( Fun  ( { <. 1 ,  1 >. }  u.  c )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  1
)  =  ( {
<. 1 ,  1
>. } `  1 ) )
241234, 240syl 15 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  c  e.  C )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  1
)  =  ( {
<. 1 ,  1
>. } `  1 ) )
24264, 64fvsn 5729 . . . . . . . . . . . . . . . . 17  |-  ( {
<. 1 ,  1
>. } `  1 )  =  1
243241, 242syl6eq 2344 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  C )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  1
)  =  1 )
244230, 232, 2433netr4d 2486 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  1 )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) )
245 elsni 3677 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  { 1 }  ->  y  =  1 )
246245fveq2d 5545 . . . . . . . . . . . . . . . 16  |-  ( y  e.  { 1 }  ->  ( F `  y )  =  ( F `  1 ) )
247245fveq2d 5545 . . . . . . . . . . . . . . . 16  |-  ( y  e.  { 1 }  ->  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) )
248246, 247neeq12d 2474 . . . . . . . . . . . . . . 15  |-  ( y  e.  { 1 }  ->  ( ( F `
 y )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) `  y )  <->  ( F `  1 )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) ) )
249244, 248syl5ibrcom 213 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  C )  ->  (
y  e.  { 1 }  ->  ( F `  y )  =/=  (
( { <. 1 ,  1 >. }  u.  c ) `  y
) ) )
250249imp 418 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  { 1 } )  ->  ( F `  y )  =/=  (
( { <. 1 ,  1 >. }  u.  c ) `  y
) )
251234adantr 451 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  Fun  ( { <. 1 ,  1
>. }  u.  c ) )
252 ssun2 3352 . . . . . . . . . . . . . . . . 17  |-  c  C_  ( { <. 1 ,  1
>. }  u.  c )
253252a1i 10 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  c  C_  ( { <. 1 ,  1 >. }  u.  c ) )
254 f1odm 5492 . . . . . . . . . . . . . . . . . . 19  |-  ( c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  ->  dom  c  =  ( 2 ... ( N  +  1 ) ) )
255206, 254syl 15 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  c  e.  C )  ->  dom  c  =  ( 2 ... ( N  + 
1 ) ) )
256255eleq2d 2363 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  c  e.  C )  ->  (
y  e.  dom  c  <->  y  e.  ( 2 ... ( N  +  1 ) ) ) )
257256biimpar 471 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  y  e.  dom  c )
258 funssfv 5559 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  ( { <. 1 ,  1 >. }  u.  c )  /\  c  C_  ( { <. 1 ,  1 >. }  u.  c )  /\  y  e.  dom  c )  ->  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 y )  =  ( c `  y
) )
259251, 253, 257, 258syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  =  ( c `
 y ) )
260 f1of 5488 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  ->  c :
( 2 ... ( N  +  1 ) ) --> ( 2 ... ( N  +  1 ) ) )
261206, 260syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  c  e.  C )  ->  c : ( 2 ... ( N  +  1 ) ) --> ( 2 ... ( N  + 
1 ) ) )
26223adantr 451 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  c  e.  C )  ->  M  e.  ( 2 ... ( N  +  1 ) ) )
263 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( c : ( 2 ... ( N  + 
1 ) ) --> ( 2 ... ( N  +  1 ) )  /\  M  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( c `  M )  e.  ( 2 ... ( N  +  1 ) ) )
264261, 262, 263syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  c  e.  C )  ->  (
c `  M )  e.  ( 2 ... ( N  +  1 ) ) )
265 nelne2 2549 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( c `  M
)  e.  ( 2 ... ( N  + 
1 ) )  /\  -.  1  e.  (
2 ... ( N  + 
1 ) ) )  ->  ( c `  M )  =/=  1
)
266264, 112, 265sylancl 643 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  c  e.  C )  ->  (
c `  M )  =/=  1 )
267266adantr 451 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
c `  M )  =/=  1 )
26882ad2antrr 706 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( F `  M )  =  1 )
269267, 268neeqtrrd 2483 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
c `  M )  =/=  ( F `  M
) )
270 fveq2 5541 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  M  ->  (
c `  y )  =  ( c `  M ) )
271270, 143neeq12d 2474 . . . . . . . . . . . . . . . . 17  |-  ( y  =  M  ->  (
( c `  y
)  =/=  ( F `
 y )  <->  ( c `  M )  =/=  ( F `  M )
) )
272269, 271syl5ibrcom 213 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
y  =  M  -> 
( c `  y
)  =/=  ( F `
 y ) ) )
273205simprd 449 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  c  e.  C )  ->  A. y  e.  ( 2 ... ( N  +  1 ) ) ( c `  y )  =/=  y
)
274273r19.21bi 2654 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
c `  y )  =/=  y )
275274adantrr 697 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  C )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( c `  y )  =/=  y
)
276158adantlr 695 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  C )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( F `  y )  =  y )
277275, 276neeqtrrd 2483 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  c  e.  C )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( c `  y )  =/=  ( F `  y )
)
278277expr 598 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
y  =/=  M  -> 
( c `  y
)  =/=  ( F `
 y ) ) )
279272, 278pm2.61dne 2536 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
c `  y )  =/=  ( F `  y
) )
280259, 279eqnetrd 2477 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  =/=  ( F `
 y ) )
281280necomd 2542 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( F `  y )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) )
282250, 281jaodan 760 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  C )  /\  (
y  e.  { 1 }  \/  y  e.  ( 2 ... ( N  +  1 ) ) ) )  -> 
( F `  y
)  =/=  ( ( { <. 1 ,  1
>. }  u.  c ) `
 y ) )
283227, 282syldan 456 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( F `  y )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) )
284222, 283eqnetrd 2477 . . . . . . . . . 10  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( `' F `  y )  =/=  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 y ) )
285196adantr 451 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
286 ffvelrn 5679 . . . . . . . . . . . . 13  |-  ( ( ( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  e.  ( 1 ... ( N  + 
1 ) ) )
287219, 286sylan 457 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  e.  ( 1 ... ( N  + 
1 ) ) )
288 f1ocnvfv 5810 . . . . . . . . . . . 12  |-  ( ( F : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) )  /\  ( ( { <. 1 ,  1 >. }  u.  c ) `  y )  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( ( F `  ( ( { <. 1 ,  1
>. }  u.  c ) `
 y ) )  =  y  ->  ( `' F `  y )  =  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 y ) ) )
289285, 287, 288syl2anc 642 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( F `  (
( { <. 1 ,  1 >. }  u.  c ) `  y
) )  =  y  ->  ( `' F `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
) ) )
290289necon3d 2497 . . . . . . . . . 10  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( `' F `  y )  =/=  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  ->  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) )  =/=  y ) )
291284, 290mpd 14 . . . . . . . . 9  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( F `  ( ( { <. 1 ,  1
>. }  u.  c ) `
 y ) )  =/=  y )
292221, 291eqnetrd 2477 . . . . . . . 8  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  y )  =/=  y )
293292ralrimiva 2639 . . . . . . 7  |-  ( (
ph  /\  c  e.  C )  ->  A. y  e.  ( 1 ... ( N  +  1 ) ) ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 y )  =/=  y )
294 snex 4232 . . . . . . . . . 10  |-  { <. 1 ,  1 >. }  e.  _V
295294, 198unex 4534 . . . . . . . . 9  |-  ( {
<. 1 ,  1
>. }  u.  c )  e.  _V
296183, 295coex 5232 . . . . . . . 8  |-  ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) )  e.  _V
297 f1oeq1 5479 . . . . . . . . 9  |-  ( f  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( f : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  <->  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) ) ) )
298 fveq1 5540 . . . . . . . . . . 11  |-  ( f  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( f `  y )  =  ( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  y ) )
299298neeq1d 2472 . . . . . . . . . 10  |-  ( f  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( (
f `  y )  =/=  y  <->  ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 y )  =/=  y ) )
300299ralbidv 2576 . . . . . . . . 9  |-  ( f  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( A. y  e.  ( 1 ... ( N  + 
1 ) ) ( f `  y )  =/=  y  <->  A. y  e.  ( 1 ... ( N  +  1 ) ) ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 y )  =/=  y ) )
301297, 300anbi12d 691 . . . . . . . 8  |-  ( f  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( (
f : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) )  /\  A. y  e.  ( 1 ... ( N  + 
1 ) ) ( f `  y )  =/=  y )  <->  ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c )
) : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) )  /\  A. y  e.  ( 1 ... ( N  + 
1 ) ) ( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  y )  =/=  y ) ) )
302296, 301, 1elab2 2930 . . . . . . 7  |-  ( ( F  o.  ( {
<. 1 ,  1
>. }  u.  c ) )  e.  A  <->  ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c )
) : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) )  /\  A. y  e.  ( 1 ... ( N  + 
1 ) ) ( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  y )  =/=  y ) )
303217, 293, 302sylanbrc 645 . . . . . 6  |-  ( (
ph  /\  c  e.  C )  ->  ( F  o.  ( { <. 1 ,  1 >. }  u.  c )
)  e.  A )
30471adantr 451 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  1  e.  ( 1 ... ( N  +  1 ) ) )
305 fvco3 5612 . . . . . . . . 9  |-  ( ( ( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  1  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  1 )  =  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) ) )
306219, 304, 305syl2anc 642 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  1 )  =  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) ) )
307243fveq2d 5545 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  ( ( { <. 1 ,  1
>. }  u.  c ) `
 1 ) )  =  ( F ` 
1 ) )
308306, 307, 2323eqtrd 2332 . . . . . . 7  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  1 )  =  M )
309131, 23sseldi 3191 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ( 1 ... ( N  + 
1 ) ) )
310309adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  M  e.  ( 1 ... ( N  +  1 ) ) )
311 fvco3 5612 . . . . . . . . . 10  |-  ( ( ( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  M  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M )  =  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) `  M ) ) )
312219, 310, 311syl2anc 642 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M )  =  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) `  M ) ) )
313252a1i 10 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  c  C_  ( { <. 1 ,  1 >. }  u.  c ) )
314262, 255eleqtrrd 2373 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  M  e.  dom  c )
315 funssfv 5559 . . . . . . . . . . 11  |-  ( ( Fun  ( { <. 1 ,  1 >. }  u.  c )  /\  c  C_  ( { <. 1 ,  1 >. }  u.  c )  /\  M  e.  dom  c )  ->  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 M )  =  ( c `  M
) )
316234, 313, 314, 315syl3anc 1182 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  M
)  =  ( c `
 M ) )
317316fveq2d 5545 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  ( ( { <. 1 ,  1
>. }  u.  c ) `
 M ) )  =  ( F `  ( c `  M
) ) )
318312, 317eqtrd 2328 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M )  =  ( F `  ( c `  M
) ) )
319136fveq1d 5543 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F ` 
1 )  =  ( F `  1 ) )
320319, 231eqtrd 2328 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F ` 
1 )  =  M )
321320adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  ( `' F `  1 )  =  M )
322 id 19 . . . . . . . . . . . . . 14  |-  ( y  =  M  ->  y  =  M )
323270, 322neeq12d 2474 . . . . . . . . . . . . 13  |-  ( y  =  M  ->  (
( c `  y
)  =/=  y  <->  ( c `  M )  =/=  M
) )
324323rspcv 2893 . . . . . . . . . . . 12  |-  ( M  e.  ( 2 ... ( N  +  1 ) )  ->  ( A. y  e.  (
2 ... ( N  + 
1 ) ) ( c `  y )  =/=  y  ->  (
c `  M )  =/=  M ) )
325262, 273, 324sylc 56 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  (
c `  M )  =/=  M )
326325necomd 2542 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  M  =/=  ( c `  M
) )
327321, 326eqnetrd 2477 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  ( `' F `  1 )  =/=  ( c `  M ) )
328131, 264sseldi 3191 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  (
c `  M )  e.  ( 1 ... ( N  +  1 ) ) )
329 f1ocnvfv 5810 . . . . . . . . . . 11  |-  ( ( F : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) )  /\  ( c `  M
)  e.  ( 1 ... ( N  + 
1 ) ) )  ->  ( ( F `
 ( c `  M ) )  =  1  ->  ( `' F `  1 )  =  ( c `  M ) ) )
330196, 328, 329syl2anc 642 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  (
( F `  (
c `  M )
)  =  1  -> 
( `' F ` 
1 )  =  ( c `  M ) ) )
331330necon3d 2497 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  (
( `' F ` 
1 )  =/=  (
c `  M )  ->  ( F `  (
c `  M )
)  =/=  1 ) )
332327, 331mpd 14 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  ( c `  M ) )  =/=  1 )
333318, 332eqnetrd 2477 . . . . . . 7  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M )  =/=  1 )
334308, 333jca 518 . . . . . 6  |-  ( (
ph  /\  c  e.  C )  ->  (
( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  1 )  =  M  /\  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M )  =/=  1 ) )
335 fveq1 5540 . . . . . . . . 9  |-  ( g  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( g `  1 )  =  ( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  1 ) )
336335eqeq1d 2304 . . . . . . . 8  |-  ( g  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( (
g `  1 )  =  M  <->  ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 1 )  =  M ) )
337 fveq1 5540 . . . . . . . . 9  |-  ( g  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( g `  M )  =  ( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M ) )
338337neeq1d 2472 . . . . . . . 8  |-  ( g  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( (
g `  M )  =/=  1  <->  ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 M )  =/=  1 ) )
339336, 338anbi12d 691 . . . . . . 7  |-  ( g  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( (
( g `  1
)  =  M  /\  ( g `  M
)  =/=  1 )  <-> 
( ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 1 )  =  M  /\  ( ( F  o.  ( {
<. 1 ,  1
>. }  u.  c ) ) `  M )  =/=  1 ) ) )
340339, 6elrab2 2938 . . . . . 6  |-  ( ( F  o.  ( {
<. 1 ,  1
>. }  u.  c ) )  e.  B  <->  ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c )
)  e.  A  /\  ( ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 1 )  =  M  /\  ( ( F  o.  ( {
<. 1 ,  1
>. }  u.  c ) ) `  M )  =/=  1 ) ) )
341303, 334, 340sylanbrc 645 . . . . 5  |-  ( (
ph  /\  c  e.  C )  ->  ( F  o.  ( { <. 1 ,  1 >. }  u.  c )
)  e.  B )
342341ex 423 . . . 4  |-  ( ph  ->  ( c  e.  C  ->  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  e.  B ) )
34330adantr 451 . . . . . . . 8  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
344 f1of1 5487 . . . . . . . 8  |-  ( F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  F :
( 1 ... ( N  +  1 ) ) -1-1-> ( 1 ... ( N  +  1 ) ) )
345343, 344syl 15 . . . . . . 7  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-> ( 1 ... ( N  + 
1 ) ) )
346 f1of 5488 . . . . . . . . 9  |-  ( F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  F :
( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) ) )
347343, 346syl 15 . . . . . . . 8  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  ->  F : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
34876adantrr 697 . . . . . . . 8  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
b : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) ) )
349 fco 5414 . . . . . . . 8  |-  ( ( F : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  b : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) ) )  ->  ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
350347, 348, 349syl2anc 642 . . . . . . 7  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( F  o.  b
) : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) ) )
351219adantrl 696 . . . . . . 7  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) ) )
352 cocan1 5817 . . . . . . 7  |-  ( ( F : ( 1 ... ( N  + 
1 ) ) -1-1-> ( 1 ... ( N  +  1 ) )  /\  ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  ( {
<. 1 ,  1
>. }  u.  c ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )  ->  ( ( F  o.  ( F  o.  b ) )  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  <->  ( F  o.  b )  =  ( { <. 1 ,  1
>. }  u.  c ) ) )
353345, 350, 351, 352syl3anc 1182 . . . . . 6  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  ( F  o.  b
) )  =  ( F  o.  ( {
<. 1 ,  1
>. }  u.  c ) )  <->  ( F  o.  b )  =  ( { <. 1 ,  1
>. }  u.  c ) ) )
354 coass 5207 . . . . . . . 8  |-  ( ( F  o.  F )  o.  b )  =  ( F  o.  ( F  o.  b )
)
355136coeq1d 4861 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F  o.  F )  =  ( F  o.  F ) )
356 f1ococnv1 5518 . . . . . . . . . . . . 13  |-  ( F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  ( `' F  o.  F )  =  (  _I  |`  (
1 ... ( N  + 
1 ) ) ) )
35730, 356syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F  o.  F )  =  (  _I  |`  ( 1 ... ( N  + 
1 ) ) ) )
358355, 357eqtr3d 2330 . . . . . . . . . . 11  |-  ( ph  ->  ( F  o.  F
)  =  (  _I  |`  ( 1 ... ( N  +  1 ) ) ) )
359358adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( F  o.  F
)  =  (  _I  |`  ( 1 ... ( N  +  1 ) ) ) )
360359coeq1d 4861 . . . . . . . . 9  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  F )  o.  b
)  =  ( (  _I  |`  ( 1 ... ( N  + 
1 ) ) )  o.  b ) )
361 fcoi2 5432 . . . . . . . . . 10  |-  ( b : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) )  -> 
( (  _I  |`  (
1 ... ( N  + 
1 ) ) )  o.  b )  =  b )
362348, 361syl 15 . . . . . . . . 9  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( (  _I  |`  (
1 ... ( N  + 
1 ) ) )  o.  b )  =  b )
363360, 362eqtrd 2328 . . . . . . . 8  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  F )  o.  b
)  =  b )
364354, 363syl5eqr 2342 . . . . . . 7  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( F  o.  ( F  o.  b )
)  =  b )
365364eqeq1d 2304 . . . . . 6  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  ( F  o.  b
) )  =  ( F  o.  ( {
<. 1 ,  1
>. }  u.  c ) )  <->  b  =  ( F  o.  ( {
<. 1 ,  1
>. }  u.  c ) ) ) )
36684adantrr 697 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  b ) `  1
)  =  1 )
367243adantrl 696 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 )  =  1 )
368366, 367eqtr4d 2331 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  b ) `  1
)  =  ( ( { <. 1 ,  1
>. }  u.  c ) `
 1 ) )
369 fveq2 5541 . . . . . . . . . . . . . 14  |-  ( y  =  1  ->  (
( F  o.  b
) `  y )  =  ( ( F  o.  b ) ` 
1 ) )
370 fveq2 5541 . . . . . . . . . . . . . 14  |-  ( y  =  1  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  =  ( ( { <. 1 ,  1
>. }  u.  c ) `
 1 ) )
371369, 370eqeq12d 2310 . . . . . . . . . . . . 13  |-  ( y  =  1  ->  (
( ( F  o.  b ) `  y
)  =  ( ( { <. 1 ,  1
>. }  u.  c ) `
 y )  <->  ( ( F  o.  b ) `  1 )  =  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) ) )
37264, 371ralsn 3687 . . . . . . . . . . . 12  |-  ( A. y  e.  { 1 }  ( ( F  o.  b ) `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
)  <->  ( ( F  o.  b ) ` 
1 )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  1
) )
373368, 372sylibr 203 . . . . . . . . . . 11  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  ->  A. y  e.  { 1 }  ( ( F  o.  b ) `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
) )
374373biantrurd 494 . . . . . . . . . 10  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( A. y  e.  ( 2 ... ( N  +  1 ) ) ( ( F  o.  b ) `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
)  <->  ( A. y  e.  { 1 }  (
( F  o.  b
) `  y )  =  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 y )  /\  A. y  e.  ( 2 ... ( N  + 
1 ) ) ( ( F  o.  b
) `  y )  =  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 y ) ) ) )
375 ralunb 3369 . . . . . . . . . 10  |-  ( A. y  e.  ( {
1 }  u.  (
2 ... ( N  + 
1 ) ) ) ( ( F  o.  b ) `  y
)  =  ( ( { <. 1 ,  1
>. }  u.  c ) `
 y )  <->  ( A. y  e.  { 1 }  ( ( F  o.  b ) `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
)  /\  A. y  e.  ( 2 ... ( N  +  1 ) ) ( ( F  o.  b ) `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
) ) )
376374, 375syl6bbr 254 . . . . . . . . 9  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( A. y  e.  ( 2 ... ( N  +  1 ) ) ( ( F  o.  b ) `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
)  <->  A. y  e.  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) ( ( F  o.  b ) `
 y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) ) )
377188adantl 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
b  e.  B  /\  c  e.  C )
)  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( ( F  o.  b )  |`  (
2 ... ( N  + 
1 ) ) ) `
 y )  =  ( ( F  o.  b ) `  y
) )
378377eqcomd 2301 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
b  e.  B  /\  c  e.  C )
)  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( F  o.  b
) `  y )  =  ( ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) `  y
) )
379259adantlrl 700 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
b  e.  B  /\  c  e.  C )
)  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  =  ( c `
 y ) )
380378, 379eqeq12d 2310 . . . . . . . . . 10  |-  ( ( ( ph  /\  (
b  e.  B  /\  c  e.  C )
)  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( ( F  o.  b ) `  y
)  =  ( ( { <. 1 ,  1
>. }  u.  c ) `
 y )  <->  ( (
( F  o.  b
)  |`  ( 2 ... ( N  +  1 ) ) ) `  y )  =  ( c `  y ) ) )
381380ralbidva 2572 . . . . . . . . 9  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( A. y  e.  ( 2 ... ( N  +  1 ) ) ( ( F  o.  b ) `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
)  <->  A. y  e.  ( 2 ... ( N  +  1 ) ) ( ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) `  y
)  =  ( c `
 y ) ) )
382103adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  =  ( 1 ... ( N  +  1 ) ) )
383382raleqdv 2755 . . . . . . . . 9  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( A. y  e.  ( { 1 }  u.  ( 2 ... (