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

Theorem subfacp1lem5 24872
Description: Lemma for subfacp1 24874. In subfacp1lem6 24873 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 11313 . . . . . . . . 9  |-  ( 1 ... ( N  + 
1 ) )  e. 
Fin
3 deranglem 24854 . . . . . . . . 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 2508 . . . . . . 7  |-  A  e. 
Fin
6 subfacp1lem5.b . . . . . . . 8  |-  B  =  { g  e.  A  |  ( ( g `
 1 )  =  M  /\  ( g `
 M )  =/=  1 ) }
7 ssrab2 3430 . . . . . . . 8  |-  { g  e.  A  |  ( ( g `  1
)  =  M  /\  ( g `  M
)  =/=  1 ) }  C_  A
86, 7eqsstri 3380 . . . . . . 7  |-  B  C_  A
9 ssfi 7331 . . . . . . 7  |-  ( ( A  e.  Fin  /\  B  C_  A )  ->  B  e.  Fin )
105, 8, 9mp2an 655 . . . . . 6  |-  B  e. 
Fin
1110elexi 2967 . . . . 5  |-  B  e. 
_V
1211a1i 11 . . . 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 11313 . . . . . . . 8  |-  ( 2 ... ( N  + 
1 ) )  e. 
Fin
15 deranglem 24854 . . . . . . . 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 2508 . . . . . 6  |-  C  e. 
Fin
1817elexi 2967 . . . . 5  |-  C  e. 
_V
1918a1i 11 . . . 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 5715 . . . . . . . . . . . . . 14  |-  (  _I  |`  K ) : K -1-1-onto-> K
2827a1i 11 . . . . . . . . . . . . 13  |-  ( ph  ->  (  _I  |`  K ) : K -1-1-onto-> K )
2920, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2a 24868 . . . . . . . . . . . 12  |-  ( ph  ->  ( F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  /\  ( F ` 
1 )  =  M  /\  ( F `  M )  =  1 ) )
3029simp1d 970 . . . . . . . . . . 11  |-  ( ph  ->  F : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) ) )
3130adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  B )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
32 simpr 449 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  b  e.  B )  ->  b  e.  B )
33 fveq1 5729 . . . . . . . . . . . . . . . . 17  |-  ( g  =  b  ->  (
g `  1 )  =  ( b ` 
1 ) )
3433eqeq1d 2446 . . . . . . . . . . . . . . . 16  |-  ( g  =  b  ->  (
( g `  1
)  =  M  <->  ( b `  1 )  =  M ) )
35 fveq1 5729 . . . . . . . . . . . . . . . . 17  |-  ( g  =  b  ->  (
g `  M )  =  ( b `  M ) )
3635neeq1d 2616 . . . . . . . . . . . . . . . 16  |-  ( g  =  b  ->  (
( g `  M
)  =/=  1  <->  (
b `  M )  =/=  1 ) )
3734, 36anbi12d 693 . . . . . . . . . . . . . . 15  |-  ( g  =  b  ->  (
( ( g ` 
1 )  =  M  /\  ( g `  M )  =/=  1
)  <->  ( ( b `
 1 )  =  M  /\  ( b `
 M )  =/=  1 ) ) )
3837, 6elrab2 3096 . . . . . . . . . . . . . 14  |-  ( b  e.  B  <->  ( b  e.  A  /\  (
( b `  1
)  =  M  /\  ( b `  M
)  =/=  1 ) ) )
3932, 38sylib 190 . . . . . . . . . . . . 13  |-  ( (
ph  /\  b  e.  B )  ->  (
b  e.  A  /\  ( ( b ` 
1 )  =  M  /\  ( b `  M )  =/=  1
) ) )
4039simpld 447 . . . . . . . . . . . 12  |-  ( (
ph  /\  b  e.  B )  ->  b  e.  A )
41 vex 2961 . . . . . . . . . . . . 13  |-  b  e. 
_V
42 f1oeq1 5667 . . . . . . . . . . . . . 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 5729 . . . . . . . . . . . . . . . 16  |-  ( f  =  b  ->  (
f `  y )  =  ( b `  y ) )
4443neeq1d 2616 . . . . . . . . . . . . . . 15  |-  ( f  =  b  ->  (
( f `  y
)  =/=  y  <->  ( b `  y )  =/=  y
) )
4544ralbidv 2727 . . . . . . . . . . . . . 14  |-  ( f  =  b  ->  ( A. y  e.  (
1 ... ( N  + 
1 ) ) ( f `  y )  =/=  y  <->  A. y  e.  ( 1 ... ( N  +  1 ) ) ( b `  y )  =/=  y
) )
4642, 45anbi12d 693 . . . . . . . . . . . . 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 3087 . . . . . . . . . . . 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 190 . . . . . . . . . . 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 447 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  B )  ->  b : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
50 f1oco 5700 . . . . . . . . . 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 644 . . . . . . . . 9  |-  ( (
ph  /\  b  e.  B )  ->  ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
52 f1of1 5675 . . . . . . . . 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 5461 . . . . . . . . . 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 452 . . . . . . . . 9  |-  ( ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) -1-1-> ( 1 ... ( N  + 
1 ) )  ->  Fun  `' ( F  o.  b ) )
5551, 52, 543syl 19 . . . . . . . 8  |-  ( (
ph  /\  b  e.  B )  ->  Fun  `' ( F  o.  b
) )
56 f1ofn 5677 . . . . . . . . . . 11  |-  ( ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  ( F  o.  b )  Fn  (
1 ... ( N  + 
1 ) ) )
57 fnresdm 5556 . . . . . . . . . . 11  |-  ( ( F  o.  b )  Fn  ( 1 ... ( N  +  1 ) )  ->  (
( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) )  =  ( F  o.  b
) )
58 f1oeq1 5667 . . . . . . . . . . 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 ) ) ) )
5951, 56, 57, 584syl 20 . . . . . . . . . 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 ) ) ) )
6051, 59mpbird 225 . . . . . . . . 9  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
61 f1ofo 5683 . . . . . . . . 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 ) ) )
6260, 61syl 16 . . . . . . . 8  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) ) : ( 1 ... ( N  +  1 ) ) -onto-> ( 1 ... ( N  +  1 ) ) )
63 1ex 9088 . . . . . . . . . . 11  |-  1  e.  _V
6463, 63f1osn 5717 . . . . . . . . . 10  |-  { <. 1 ,  1 >. } : { 1 } -1-1-onto-> { 1 }
6551, 56syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  b  e.  B )  ->  ( F  o.  b )  Fn  ( 1 ... ( N  +  1 ) ) )
6622peano2nnd 10019 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  1 )  e.  NN )
67 nnuz 10523 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
6866, 67syl6eleq 2528 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
1 ) )
69 eluzfz1 11066 . . . . . . . . . . . . . . 15  |-  ( ( N  +  1 )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( N  +  1 ) ) )
7068, 69syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  e.  ( 1 ... ( N  + 
1 ) ) )
7170adantr 453 . . . . . . . . . . . . 13  |-  ( (
ph  /\  b  e.  B )  ->  1  e.  ( 1 ... ( N  +  1 ) ) )
72 fnressn 5920 . . . . . . . . . . . . 13  |-  ( ( ( F  o.  b
)  Fn  ( 1 ... ( N  + 
1 ) )  /\  1  e.  ( 1 ... ( N  + 
1 ) ) )  ->  ( ( F  o.  b )  |`  { 1 } )  =  { <. 1 ,  ( ( F  o.  b ) ` 
1 ) >. } )
7365, 71, 72syl2anc 644 . . . . . . . . . . . 12  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  { 1 } )  =  { <. 1 ,  ( ( F  o.  b ) `  1 ) >. } )
74 f1of 5676 . . . . . . . . . . . . . . . . 17  |-  ( b : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  b :
( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) ) )
7549, 74syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  b  e.  B )  ->  b : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
76 fvco3 5802 . . . . . . . . . . . . . . . 16  |-  ( ( b : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  1  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( ( F  o.  b ) `  1 )  =  ( F `  (
b `  1 )
) )
7775, 71, 76syl2anc 644 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
) `  1 )  =  ( F `  ( b `  1
) ) )
7839simprd 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  b  e.  B )  ->  (
( b `  1
)  =  M  /\  ( b `  M
)  =/=  1 ) )
7978simpld 447 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  b  e.  B )  ->  (
b `  1 )  =  M )
8079fveq2d 5734 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  B )  ->  ( F `  ( b `  1 ) )  =  ( F `  M ) )
8129simp3d 972 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F `  M
)  =  1 )
8281adantr 453 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  B )  ->  ( F `  M )  =  1 )
8377, 80, 823eqtrd 2474 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
) `  1 )  =  1 )
8483opeq2d 3993 . . . . . . . . . . . . 13  |-  ( (
ph  /\  b  e.  B )  ->  <. 1 ,  ( ( F  o.  b ) ` 
1 ) >.  =  <. 1 ,  1 >. )
8584sneqd 3829 . . . . . . . . . . . 12  |-  ( (
ph  /\  b  e.  B )  ->  { <. 1 ,  ( ( F  o.  b ) `  1 ) >. }  =  { <. 1 ,  1 >. } )
8673, 85eqtrd 2470 . . . . . . . . . . 11  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  { 1 } )  =  { <. 1 ,  1 >. } )
87 f1oeq1 5667 . . . . . . . . . . 11  |-  ( ( ( F  o.  b
)  |`  { 1 } )  =  { <. 1 ,  1 >. }  ->  ( ( ( F  o.  b )  |`  { 1 } ) : { 1 } -1-1-onto-> { 1 }  <->  { <. 1 ,  1 >. } : { 1 } -1-1-onto-> { 1 } ) )
8886, 87syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  B )  ->  (
( ( F  o.  b )  |`  { 1 } ) : {
1 } -1-1-onto-> { 1 }  <->  { <. 1 ,  1 >. } : { 1 } -1-1-onto-> { 1 } ) )
8964, 88mpbiri 226 . . . . . . . . 9  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  { 1 } ) : { 1 } -1-1-onto-> { 1 } )
90 f1ofo 5683 . . . . . . . . 9  |-  ( ( ( F  o.  b
)  |`  { 1 } ) : { 1 } -1-1-onto-> { 1 }  ->  ( ( F  o.  b
)  |`  { 1 } ) : { 1 } -onto-> { 1 } )
9189, 90syl 16 . . . . . . . 8  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  { 1 } ) : { 1 } -onto-> { 1 } )
92 resdif 5698 . . . . . . . 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 } ) )
9355, 62, 91, 92syl3anc 1185 . . . . . . 7  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( ( 1 ... ( N  + 
1 ) )  \  { 1 } ) ) : ( ( 1 ... ( N  +  1 ) ) 
\  { 1 } ) -1-1-onto-> ( ( 1 ... ( N  +  1 ) )  \  {
1 } ) )
94 fzsplit 11079 . . . . . . . . . . . 12  |-  ( 1  e.  ( 1 ... ( N  +  1 ) )  ->  (
1 ... ( N  + 
1 ) )  =  ( ( 1 ... 1 )  u.  (
( 1  +  1 ) ... ( N  +  1 ) ) ) )
9570, 94syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( 1 ... ( N  +  1 ) )  =  ( ( 1 ... 1 )  u.  ( ( 1  +  1 ) ... ( N  +  1 ) ) ) )
96 1z 10313 . . . . . . . . . . . . 13  |-  1  e.  ZZ
97 fzsn 11096 . . . . . . . . . . . . 13  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
9896, 97ax-mp 8 . . . . . . . . . . . 12  |-  ( 1 ... 1 )  =  { 1 }
99 1p1e2 10096 . . . . . . . . . . . . 13  |-  ( 1  +  1 )  =  2
10099oveq1i 6093 . . . . . . . . . . . 12  |-  ( ( 1  +  1 ) ... ( N  + 
1 ) )  =  ( 2 ... ( N  +  1 ) )
10198, 100uneq12i 3501 . . . . . . . . . . 11  |-  ( ( 1 ... 1 )  u.  ( ( 1  +  1 ) ... ( N  +  1 ) ) )  =  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )
10295, 101syl6req 2487 . . . . . . . . . 10  |-  ( ph  ->  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  =  ( 1 ... ( N  +  1 ) ) )
10370snssd 3945 . . . . . . . . . . 11  |-  ( ph  ->  { 1 }  C_  ( 1 ... ( N  +  1 ) ) )
104 incom 3535 . . . . . . . . . . . 12  |-  ( { 1 }  i^i  (
2 ... ( N  + 
1 ) ) )  =  ( ( 2 ... ( N  + 
1 ) )  i^i 
{ 1 } )
105 1lt2 10144 . . . . . . . . . . . . . . 15  |-  1  <  2
106 1re 9092 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
107 2re 10071 . . . . . . . . . . . . . . . 16  |-  2  e.  RR
108106, 107ltnlei 9196 . . . . . . . . . . . . . . 15  |-  ( 1  <  2  <->  -.  2  <_  1 )
109105, 108mpbi 201 . . . . . . . . . . . . . 14  |-  -.  2  <_  1
110 elfzle1 11062 . . . . . . . . . . . . . 14  |-  ( 1  e.  ( 2 ... ( N  +  1 ) )  ->  2  <_  1 )
111109, 110mto 170 . . . . . . . . . . . . 13  |-  -.  1  e.  ( 2 ... ( N  +  1 ) )
112 disjsn 3870 . . . . . . . . . . . . 13  |-  ( ( ( 2 ... ( N  +  1 ) )  i^i  { 1 } )  =  (/)  <->  -.  1  e.  ( 2 ... ( N  + 
1 ) ) )
113111, 112mpbir 202 . . . . . . . . . . . 12  |-  ( ( 2 ... ( N  +  1 ) )  i^i  { 1 } )  =  (/)
114104, 113eqtri 2458 . . . . . . . . . . 11  |-  ( { 1 }  i^i  (
2 ... ( N  + 
1 ) ) )  =  (/)
115 uneqdifeq 3718 . . . . . . . . . . 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 ) ) ) )
116103, 114, 115sylancl 645 . . . . . . . . . 10  |-  ( ph  ->  ( ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) )  =  ( 1 ... ( N  +  1 ) )  <->  ( (
1 ... ( N  + 
1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) ) ) )
117102, 116mpbid 203 . . . . . . . . 9  |-  ( ph  ->  ( ( 1 ... ( N  +  1 ) )  \  {
1 } )  =  ( 2 ... ( N  +  1 ) ) )
118117adantr 453 . . . . . . . 8  |-  ( (
ph  /\  b  e.  B )  ->  (
( 1 ... ( N  +  1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) ) )
119 reseq2 5143 . . . . . . . . . 10  |-  ( ( ( 1 ... ( N  +  1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) )  ->  ( ( F  o.  b )  |`  ( ( 1 ... ( N  +  1 ) )  \  {
1 } ) )  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) )
120 f1oeq1 5667 . . . . . . . . . 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 } ) ) )
121119, 120syl 16 . . . . . . . . 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 } ) ) )
122 f1oeq2 5668 . . . . . . . . 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 } ) ) )
123 f1oeq3 5669 . . . . . . . . 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 ) ) ) )
124121, 122, 1233bitrd 272 . . . . . . . 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 ) ) ) )
125118, 124syl 16 . . . . . . 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 ) ) ) )
12693, 125mpbid 203 . . . . . 6  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 2 ... ( N  +  1 ) ) ) : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) )
12775adantr 453 . . . . . . . . 9  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  b : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
128 fzp1ss 11100 . . . . . . . . . . . 12  |-  ( 1  e.  ZZ  ->  (
( 1  +  1 ) ... ( N  +  1 ) ) 
C_  ( 1 ... ( N  +  1 ) ) )
12996, 128ax-mp 8 . . . . . . . . . . 11  |-  ( ( 1  +  1 ) ... ( N  + 
1 ) )  C_  ( 1 ... ( N  +  1 ) )
130100, 129eqsstr3i 3381 . . . . . . . . . 10  |-  ( 2 ... ( N  + 
1 ) )  C_  ( 1 ... ( N  +  1 ) )
131 simpr 449 . . . . . . . . . 10  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  y  e.  ( 2 ... ( N  +  1 ) ) )
132130, 131sseldi 3348 . . . . . . . . 9  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  y  e.  ( 1 ... ( N  +  1 ) ) )
133 fvco3 5802 . . . . . . . . 9  |-  ( ( b : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( ( F  o.  b ) `  y )  =  ( F `  ( b `
 y ) ) )
134127, 132, 133syl2anc 644 . . . . . . . 8  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( F  o.  b
) `  y )  =  ( F `  ( b `  y
) ) )
13520, 21, 1, 22, 23, 24, 25, 6, 26subfacp1lem4 24871 . . . . . . . . . . . 12  |-  ( ph  ->  `' F  =  F
)
136135fveq1d 5732 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F `  y )  =  ( F `  y ) )
137136ad2antrr 708 . . . . . . . . . 10  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( `' F `  y )  =  ( F `  y ) )
13878simprd 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  B )  ->  (
b `  M )  =/=  1 )
139138, 82neeqtrrd 2627 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  b  e.  B )  ->  (
b `  M )  =/=  ( F `  M
) )
140139adantr 453 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
b `  M )  =/=  ( F `  M
) )
141 fveq2 5730 . . . . . . . . . . . . . 14  |-  ( y  =  M  ->  (
b `  y )  =  ( b `  M ) )
142 fveq2 5730 . . . . . . . . . . . . . 14  |-  ( y  =  M  ->  ( F `  y )  =  ( F `  M ) )
143141, 142neeq12d 2618 . . . . . . . . . . . . 13  |-  ( y  =  M  ->  (
( b `  y
)  =/=  ( F `
 y )  <->  ( b `  M )  =/=  ( F `  M )
) )
144140, 143syl5ibrcom 215 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
y  =  M  -> 
( b `  y
)  =/=  ( F `
 y ) ) )
145130sseli 3346 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 2 ... ( N  +  1 ) )  ->  y  e.  ( 1 ... ( N  +  1 ) ) )
14648simprd 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  b  e.  B )  ->  A. y  e.  ( 1 ... ( N  +  1 ) ) ( b `  y )  =/=  y
)
147146r19.21bi 2806 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
b `  y )  =/=  y )
148145, 147sylan2 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
b `  y )  =/=  y )
149148adantrr 699 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  b  e.  B )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( b `  y )  =/=  y
)
15025eleq2i 2502 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  K  <->  y  e.  ( ( 2 ... ( N  +  1 ) )  \  { M } ) )
151 eldifsn 3929 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( ( 2 ... ( N  + 
1 ) )  \  { M } )  <->  ( y  e.  ( 2 ... ( N  +  1 ) )  /\  y  =/= 
M ) )
152150, 151bitri 242 . . . . . . . . . . . . . . . 16  |-  ( y  e.  K  <->  ( y  e.  ( 2 ... ( N  +  1 ) )  /\  y  =/= 
M ) )
15320, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2b 24869 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  K )  ->  ( F `  y )  =  ( (  _I  |`  K ) `  y
) )
154 fvresi 5926 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  K  ->  (
(  _I  |`  K ) `
 y )  =  y )
155154adantl 454 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  K )  ->  (
(  _I  |`  K ) `
 y )  =  y )
156153, 155eqtrd 2470 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  K )  ->  ( F `  y )  =  y )
157152, 156sylan2br 464 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  ( 2 ... ( N  +  1 ) )  /\  y  =/= 
M ) )  -> 
( F `  y
)  =  y )
158157adantlr 697 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  b  e.  B )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( F `  y )  =  y )
159149, 158neeqtrrd 2627 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  b  e.  B )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( b `  y )  =/=  ( F `  y )
)
160159expr 600 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
y  =/=  M  -> 
( b `  y
)  =/=  ( F `
 y ) ) )
161144, 160pm2.61dne 2683 . . . . . . . . . . 11  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
b `  y )  =/=  ( F `  y
) )
162161necomd 2689 . . . . . . . . . 10  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( F `  y )  =/=  ( b `  y
) )
163137, 162eqnetrd 2621 . . . . . . . . 9  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( `' F `  y )  =/=  ( b `  y ) )
16431adantr 453 . . . . . . . . . . 11  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
165 ffvelrn 5870 . . . . . . . . . . . 12  |-  ( ( b : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( b `  y )  e.  ( 1 ... ( N  +  1 ) ) )
16675, 145, 165syl2an 465 . . . . . . . . . . 11  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
b `  y )  e.  ( 1 ... ( N  +  1 ) ) )
167 f1ocnvfv 6018 . . . . . . . . . . 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 ) ) )
168164, 166, 167syl2anc 644 . . . . . . . . . 10  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( F `  (
b `  y )
)  =  y  -> 
( `' F `  y )  =  ( b `  y ) ) )
169168necon3d 2641 . . . . . . . . 9  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( `' F `  y )  =/=  (
b `  y )  ->  ( F `  (
b `  y )
)  =/=  y ) )
170163, 169mpd 15 . . . . . . . 8  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( F `  ( b `  y ) )  =/=  y )
171134, 170eqnetrd 2621 . . . . . . 7  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( F  o.  b
) `  y )  =/=  y )
172171ralrimiva 2791 . . . . . 6  |-  ( (
ph  /\  b  e.  B )  ->  A. y  e.  ( 2 ... ( N  +  1 ) ) ( ( F  o.  b ) `  y )  =/=  y
)
173 f1of 5676 . . . . . . . . . . . . 13  |-  ( (  _I  |`  K ) : K -1-1-onto-> K  ->  (  _I  |`  K ) : K --> K )
17427, 173ax-mp 8 . . . . . . . . . . . 12  |-  (  _I  |`  K ) : K --> K
175 difexg 4353 . . . . . . . . . . . . . 14  |-  ( ( 2 ... ( N  +  1 ) )  e.  Fin  ->  (
( 2 ... ( N  +  1 ) )  \  { M } )  e.  _V )
17614, 175ax-mp 8 . . . . . . . . . . . . 13  |-  ( ( 2 ... ( N  +  1 ) ) 
\  { M }
)  e.  _V
17725, 176eqeltri 2508 . . . . . . . . . . . 12  |-  K  e. 
_V
178 fex 5971 . . . . . . . . . . . 12  |-  ( ( (  _I  |`  K ) : K --> K  /\  K  e.  _V )  ->  (  _I  |`  K )  e.  _V )
179174, 177, 178mp2an 655 . . . . . . . . . . 11  |-  (  _I  |`  K )  e.  _V
180 prex 4408 . . . . . . . . . . 11  |-  { <. 1 ,  M >. , 
<. M ,  1 >. }  e.  _V
181179, 180unex 4709 . . . . . . . . . 10  |-  ( (  _I  |`  K )  u.  { <. 1 ,  M >. ,  <. M ,  1
>. } )  e.  _V
18226, 181eqeltri 2508 . . . . . . . . 9  |-  F  e. 
_V
183182, 41coex 5415 . . . . . . . 8  |-  ( F  o.  b )  e. 
_V
184183resex 5188 . . . . . . 7  |-  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  e.  _V
185 f1oeq1 5667 . . . . . . . 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 ) ) ) )
186 fveq1 5729 . . . . . . . . . . 11  |-  ( f  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  ->  (
f `  y )  =  ( ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) `  y
) )
187 fvres 5747 . . . . . . . . . . 11  |-  ( y  e.  ( 2 ... ( N  +  1 ) )  ->  (
( ( F  o.  b )  |`  (
2 ... ( N  + 
1 ) ) ) `
 y )  =  ( ( F  o.  b ) `  y
) )
188186, 187sylan9eq 2490 . . . . . . . . . 10  |-  ( ( f  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
f `  y )  =  ( ( F  o.  b ) `  y ) )
189188neeq1d 2616 . . . . . . . . 9  |-  ( ( f  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( f `  y
)  =/=  y  <->  ( ( F  o.  b ) `  y )  =/=  y
) )
190189ralbidva 2723 . . . . . . . 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
) )
191185, 190anbi12d 693 . . . . . . 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
) ) )
192184, 191, 13elab2 3087 . . . . . 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
) )
193126, 172, 192sylanbrc 647 . . . . 5  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 2 ... ( N  +  1 ) ) )  e.  C )
194193ex 425 . . . 4  |-  ( ph  ->  ( b  e.  B  ->  ( ( F  o.  b )  |`  (
2 ... ( N  + 
1 ) ) )  e.  C ) )
19530adantr 453 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
196 simpr 449 . . . . . . . . . . . 12  |-  ( (
ph  /\  c  e.  C )  ->  c  e.  C )
197 vex 2961 . . . . . . . . . . . . 13  |-  c  e. 
_V
198 f1oeq1 5667 . . . . . . . . . . . . . 14  |-  ( f  =  c  ->  (
f : ( 2 ... ( N  + 
1 ) ) -1-1-onto-> ( 2 ... ( N  + 
1 ) )  <->  c :
( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) ) )
199 fveq1 5729 . . . . . . . . . . . . . . . 16  |-  ( f  =  c  ->  (
f `  y )  =  ( c `  y ) )
200199neeq1d 2616 . . . . . . . . . . . . . . 15  |-  ( f  =  c  ->  (
( f `  y
)  =/=  y  <->  ( c `  y )  =/=  y
) )
201200ralbidv 2727 . . . . . . . . . . . . . 14  |-  ( f  =  c  ->  ( A. y  e.  (
2 ... ( N  + 
1 ) ) ( f `  y )  =/=  y  <->  A. y  e.  ( 2 ... ( N  +  1 ) ) ( c `  y )  =/=  y
) )
202198, 201anbi12d 693 . . . . . . . . . . . . 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
) ) )
203197, 202, 13elab2 3087 . . . . . . . . . . . 12  |-  ( c  e.  C  <->  ( c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  /\  A. y  e.  ( 2 ... ( N  +  1 ) ) ( c `  y )  =/=  y
) )
204196, 203sylib 190 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  (
c : ( 2 ... ( N  + 
1 ) ) -1-1-onto-> ( 2 ... ( N  + 
1 ) )  /\  A. y  e.  ( 2 ... ( N  + 
1 ) ) ( c `  y )  =/=  y ) )
205204simpld 447 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) )
206 f1oun 5696 . . . . . . . . . . 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 ) ) ) )
207114, 114, 206mpanr12 668 . . . . . . . . . 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 ) ) ) )
20864, 205, 207sylancr 646 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  ( { <. 1 ,  1
>. }  u.  c ) : ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) ) -1-1-onto-> ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) )
209 f1oeq2 5668 . . . . . . . . . . . 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 ) ) ) ) )
210 f1oeq3 5669 . . . . . . . . . . . 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 ) ) ) )
211209, 210bitrd 246 . . . . . . . . . . 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 ) ) ) )
212102, 211syl 16 . . . . . . . . . 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 ) ) ) )
213212biimpa 472 . . . . . . . . 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 ) ) )
214208, 213syldan 458 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  ( { <. 1 ,  1
>. }  u.  c ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
215 f1oco 5700 . . . . . . . 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 ) ) )
216195, 214, 215syl2anc 644 . . . . . . 7  |-  ( (
ph  /\  c  e.  C )  ->  ( F  o.  ( { <. 1 ,  1 >. }  u.  c )
) : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) ) )
217 f1of 5676 . . . . . . . . . . 11  |-  ( ( { <. 1 ,  1
>. }  u.  c ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  ( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
218214, 217syl 16 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  ( { <. 1 ,  1
>. }  u.  c ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
219 fvco3 5802 . . . . . . . . . 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 ) ) )
220218, 219sylan 459 . . . . . . . . 9  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  y )  =  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) ) )
221136ad2antrr 708 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( `' F `  y )  =  ( F `  y ) )
222 simpr 449 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  y  e.  ( 1 ... ( N  +  1 ) ) )
223102ad2antrr 708 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  =  ( 1 ... ( N  +  1 ) ) )
224222, 223eleqtrrd 2515 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  y  e.  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) )
225 elun 3490 . . . . . . . . . . . . 13  |-  ( y  e.  ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) )  <-> 
( y  e.  {
1 }  \/  y  e.  ( 2 ... ( N  +  1 ) ) ) )
226224, 225sylib 190 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
y  e.  { 1 }  \/  y  e.  ( 2 ... ( N  +  1 ) ) ) )
227 nelne2 2696 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  e.  ( 2 ... ( N  + 
1 ) )  /\  -.  1  e.  (
2 ... ( N  + 
1 ) ) )  ->  M  =/=  1
)
22823, 111, 227sylancl 645 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  =/=  1 )
229228adantr 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  C )  ->  M  =/=  1 )
23029simp2d 971 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( F `  1
)  =  M )
231230adantr 453 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  1 )  =  M )
232 f1ofun 5678 . . . . . . . . . . . . . . . . . . 19  |-  ( ( { <. 1 ,  1
>. }  u.  c ) : ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) ) -1-1-onto-> ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  ->  Fun  ( { <. 1 ,  1
>. }  u.  c ) )
233208, 232syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  c  e.  C )  ->  Fun  ( { <. 1 ,  1
>. }  u.  c ) )
234 ssun1 3512 . . . . . . . . . . . . . . . . . . 19  |-  { <. 1 ,  1 >. } 
C_  ( { <. 1 ,  1 >. }  u.  c )
23563snid 3843 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  { 1 }
23663dmsnop 5346 . . . . . . . . . . . . . . . . . . . 20  |-  dom  { <. 1 ,  1 >. }  =  { 1 }
237235, 236eleqtrri 2511 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  dom  { <. 1 ,  1 >. }
238 funssfv 5748 . . . . . . . . . . . . . . . . . . 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 ) )
239234, 237, 238mp3an23 1272 . . . . . . . . . . . . . . . . . 18  |-  ( Fun  ( { <. 1 ,  1 >. }  u.  c )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  1
)  =  ( {
<. 1 ,  1
>. } `  1 ) )
240233, 239syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  c  e.  C )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  1
)  =  ( {
<. 1 ,  1
>. } `  1 ) )
24163, 63fvsn 5928 . . . . . . . . . . . . . . . . 17  |-  ( {
<. 1 ,  1
>. } `  1 )  =  1
242240, 241syl6eq 2486 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  C )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  1
)  =  1 )
243229, 231, 2423netr4d 2630 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  1 )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) )
244 elsni 3840 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  { 1 }  ->  y  =  1 )
245244fveq2d 5734 . . . . . . . . . . . . . . . 16  |-  ( y  e.  { 1 }  ->  ( F `  y )  =  ( F `  1 ) )
246244fveq2d 5734 . . . . . . . . . . . . . . . 16  |-  ( y  e.  { 1 }  ->  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) )
247245, 246neeq12d 2618 . . . . . . . . . . . . . . 15  |-  ( y  e.  { 1 }  ->  ( ( F `
 y )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) `  y )  <->  ( F `  1 )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) ) )
248243, 247syl5ibrcom 215 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  C )  ->  (
y  e.  { 1 }  ->  ( F `  y )  =/=  (
( { <. 1 ,  1 >. }  u.  c ) `  y
) ) )
249248imp 420 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  { 1 } )  ->  ( F `  y )  =/=  (
( { <. 1 ,  1 >. }  u.  c ) `  y
) )
250233adantr 453 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  Fun  ( { <. 1 ,  1
>. }  u.  c ) )
251 ssun2 3513 . . . . . . . . . . . . . . . . 17  |-  c  C_  ( { <. 1 ,  1
>. }  u.  c )
252251a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  c  C_  ( { <. 1 ,  1 >. }  u.  c ) )
253 f1odm 5680 . . . . . . . . . . . . . . . . . . 19  |-  ( c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  ->  dom  c  =  ( 2 ... ( N  +  1 ) ) )
254205, 253syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  c  e.  C )  ->  dom  c  =  ( 2 ... ( N  + 
1 ) ) )
255254eleq2d 2505 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  c  e.  C )  ->  (
y  e.  dom  c  <->  y  e.  ( 2 ... ( N  +  1 ) ) ) )
256255biimpar 473 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  y  e.  dom  c )
257 funssfv 5748 . . . . . . . . . . . . . . . 16  |-  ( ( Fun  ( { <. 1 ,  1 >. }  u.  c )  /\  c  C_  ( { <. 1 ,  1 >. }  u.  c )  /\  y  e.  dom  c )  ->  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 y )  =  ( c `  y
) )
258250, 252, 256, 257syl3anc 1185 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  =  ( c `
 y ) )
259 f1of 5676 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  ->  c :
( 2 ... ( N  +  1 ) ) --> ( 2 ... ( N  +  1 ) ) )
260205, 259syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  c  e.  C )  ->  c : ( 2 ... ( N  +  1 ) ) --> ( 2 ... ( N  + 
1 ) ) )
26123adantr 453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  c  e.  C )  ->  M  e.  ( 2 ... ( N  +  1 ) ) )
262260, 261ffvelrnd 5873 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  c  e.  C )  ->  (
c `  M )  e.  ( 2 ... ( N  +  1 ) ) )
263 nelne2 2696 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( c `  M
)  e.  ( 2 ... ( N  + 
1 ) )  /\  -.  1  e.  (
2 ... ( N  + 
1 ) ) )  ->  ( c `  M )  =/=  1
)
264262, 111, 263sylancl 645 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  c  e.  C )  ->  (
c `  M )  =/=  1 )
265264adantr 453 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
c `  M )  =/=  1 )
26681ad2antrr 708 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( F `  M )  =  1 )
267265, 266neeqtrrd 2627 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
c `  M )  =/=  ( F `  M
) )
268 fveq2 5730 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  M  ->  (
c `  y )  =  ( c `  M ) )
269268, 142neeq12d 2618 . . . . . . . . . . . . . . . . 17  |-  ( y  =  M  ->  (
( c `  y
)  =/=  ( F `
 y )  <->  ( c `  M )  =/=  ( F `  M )
) )
270267, 269syl5ibrcom 215 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
y  =  M  -> 
( c `  y
)  =/=  ( F `
 y ) ) )
271204simprd 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  c  e.  C )  ->  A. y  e.  ( 2 ... ( N  +  1 ) ) ( c `  y )  =/=  y
)
272271r19.21bi 2806 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
c `  y )  =/=  y )
273272adantrr 699 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  C )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( c `  y )  =/=  y
)
274157adantlr 697 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  C )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( F `  y )  =  y )
275273, 274neeqtrrd 2627 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  c  e.  C )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( c `  y )  =/=  ( F `  y )
)
276275expr 600 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
y  =/=  M  -> 
( c `  y
)  =/=  ( F `
 y ) ) )
277270, 276pm2.61dne 2683 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
c `  y )  =/=  ( F `  y
) )
278258, 277eqnetrd 2621 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  =/=  ( F `
 y ) )
279278necomd 2689 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( F `  y )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) )
280249, 279jaodan 762 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  C )  /\  (
y  e.  { 1 }  \/  y  e.  ( 2 ... ( N  +  1 ) ) ) )  -> 
( F `  y
)  =/=  ( ( { <. 1 ,  1
>. }  u.  c ) `
 y ) )
281226, 280syldan 458 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( F `  y )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) )
282221, 281eqnetrd 2621 . . . . . . . . . 10  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( `' F `  y )  =/=  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 y ) )
283195adantr 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
284218ffvelrnda 5872 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  e.  ( 1 ... ( N  + 
1 ) ) )
285 f1ocnvfv 6018 . . . . . . . . . . . 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 ) ) )
286283, 284, 285syl2anc 644 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( F `  (
( { <. 1 ,  1 >. }  u.  c ) `  y
) )  =  y  ->  ( `' F `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
) ) )
287286necon3d 2641 . . . . . . . . . 10  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( `' F `  y )  =/=  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  ->  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) )  =/=  y ) )
288282, 287mpd 15 . . . . . . . . 9  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( F `  ( ( { <. 1 ,  1
>. }  u.  c ) `
 y ) )  =/=  y )
289220, 288eqnetrd 2621 . . . . . . . 8  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  y )  =/=  y )
290289ralrimiva 2791 . . . . . . 7  |-  ( (
ph  /\  c  e.  C )  ->  A. y  e.  ( 1 ... ( N  +  1 ) ) ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 y )  =/=  y )
291 snex 4407 . . . . . . . . . 10  |-  { <. 1 ,  1 >. }  e.  _V
292291, 197unex 4709 . . . . . . . . 9  |-  ( {
<. 1 ,  1
>. }  u.  c )  e.  _V
293182, 292coex 5415 . . . . . . . 8  |-  ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) )  e.  _V
294 f1oeq1 5667 . . . . . . . . 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 ) ) ) )
295 fveq1 5729 . . . . . . . . . . 11  |-  ( f  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( f `  y )  =  ( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  y ) )
296295neeq1d 2616 . . . . . . . . . 10  |-  ( f  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( (
f `  y )  =/=  y  <->  ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 y )  =/=  y ) )
297296ralbidv 2727 . . . . . . . . 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 ) )
298294, 297anbi12d 693 . . . . . . . 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 ) ) )
299293, 298, 1elab2 3087 . . . . . . 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 ) )
300216, 290, 299sylanbrc 647 . . . . . 6  |-  ( (
ph  /\  c  e.  C )  ->  ( F  o.  ( { <. 1 ,  1 >. }  u.  c )
)  e.  A )
30170adantr 453 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  1  e.  ( 1 ... ( N  +  1 ) ) )
302 fvco3 5802 . . . . . . . . 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 ) ) )
303218, 301, 302syl2anc 644 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  1 )  =  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) ) )
304242fveq2d 5734 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  ( ( { <. 1 ,  1
>. }  u.  c ) `
 1 ) )  =  ( F ` 
1 ) )
305303, 304, 2313eqtrd 2474 . . . . . . 7  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  1 )  =  M )
306130, 23sseldi 3348 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ( 1 ... ( N  + 
1 ) ) )
307306adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  M  e.  ( 1 ... ( N  +  1 ) ) )
308 fvco3 5802 . . . . . . . . . 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 ) ) )
309218, 307, 308syl2anc 644 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M )  =  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) `  M ) ) )
310251a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  c  C_  ( { <. 1 ,  1 >. }  u.  c ) )
311261, 254eleqtrrd 2515 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  M  e.  dom  c )
312 funssfv 5748 . . . . . . . . . . 11  |-  ( ( Fun  ( { <. 1 ,  1 >. }  u.  c )  /\  c  C_  ( { <. 1 ,  1 >. }  u.  c )  /\  M  e.  dom  c )  ->  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 M )  =  ( c `  M
) )
313233, 310, 311, 312syl3anc 1185 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  M
)  =  ( c `
 M ) )
314313fveq2d 5734 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  ( ( { <. 1 ,  1
>. }  u.  c ) `
 M ) )  =  ( F `  ( c `  M
) ) )
315309, 314eqtrd 2470 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M )  =  ( F `  ( c `  M
) ) )
316135fveq1d 5732 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F ` 
1 )  =  ( F `  1 ) )
317316, 230eqtrd 2470 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F ` 
1 )  =  M )
318317adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  ( `' F `  1 )  =  M )
319 id 21 . . . . . . . . . . . . . 14  |-  ( y  =  M  ->  y  =  M )
320268, 319neeq12d 2618 . . . . . . . . . . . . 13  |-  ( y  =  M  ->  (
( c `  y
)  =/=  y  <->  ( c `  M )  =/=  M
) )
321320rspcv 3050 . . . . . . . . . . . 12  |-  ( M  e.  ( 2 ... ( N  +  1 ) )  ->  ( A. y  e.  (
2 ... ( N  + 
1 ) ) ( c `  y )  =/=  y  ->  (
c `  M )  =/=  M ) )
322261, 271, 321sylc 59 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  (
c `  M )  =/=  M )
323322necomd 2689 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  M  =/=  ( c `  M
) )
324318, 323eqnetrd 2621 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  ( `' F `  1 )  =/=  ( c `  M ) )
325130, 262sseldi 3348 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  (
c `  M )  e.  ( 1 ... ( N  +  1 ) ) )
326 f1ocnvfv 6018 . . . . . . . . . . 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 ) ) )
327195, 325, 326syl2anc 644 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  (
( F `  (
c `  M )
)  =  1  -> 
( `' F ` 
1 )  =  ( c `  M ) ) )
328327necon3d 2641 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  (
( `' F ` 
1 )  =/=  (
c `  M )  ->  ( F `  (
c `  M )
)  =/=  1 ) )
329324, 328mpd 15 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  ( c `  M ) )  =/=  1 )
330315, 329eqnetrd 2621 . . . . . . 7  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M )  =/=  1 )
331305, 330jca 520 . . . . . 6  |-  ( (
ph  /\  c  e.  C )  ->  (
( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  1 )  =  M  /\  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M )  =/=  1 ) )
332 fveq1 5729 . . . . . . . . 9  |-  ( g  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( g `  1 )  =  ( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  1 ) )
333332eqeq1d 2446 . . . . . . . 8  |-  ( g  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( (
g `  1 )  =  M  <->  ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 1 )  =  M ) )
334 fveq1 5729 . . . . . . . . 9  |-  ( g  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( g `  M )  =  ( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M ) )
335334neeq1d 2616 . . . . . . . 8  |-  ( g  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( (
g `  M )  =/=  1  <->  ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 M )  =/=  1 ) )
336333, 335anbi12d 693 . . . . . . 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 ) ) )
337336, 6elrab2 3096 . . . . . 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 ) ) )
338300, 331, 337sylanbrc 647 . . . . 5  |-  ( (
ph  /\  c  e.  C )  ->  ( F  o.  ( { <. 1 ,  1 >. }  u.  c )
)  e.  B )
339338ex 425 . . . 4  |-  ( ph  ->  ( c  e.  C  ->  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  e.  B ) )
34030adantr 453 . . . . . . . 8  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
341 f1of1 5675 . . . . . . . 8  |-  ( F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  F :
( 1 ... ( N  +  1 ) ) -1-1-> ( 1 ... ( N  +  1 ) ) )
342340, 341syl 16 . . . . . . 7  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-> ( 1 ... ( N  + 
1 ) ) )
343 f1of 5676 . . . . . . . . 9  |-  ( F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  F :
( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) ) )
344340, 343syl 16 . . . . . . . 8  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  ->  F : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
34575adantrr 699 . . . . . . . 8  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
b : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) ) )
346 fco 5602 . . . . . . . 8  |-  ( ( F : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  b : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) ) )  ->  ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
347344, 345, 346syl2anc 644 . . . . . . 7  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( F  o.  b
) : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) ) )
348218adantrl 698 . . . . . . 7  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) ) )
349 cocan1 6026 . . . . . . 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 ) ) )
350342, 347, 348, 349syl3anc 1185 . . . . . 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 ) ) )
351 coass 5390 . . . . . . . 8  |-  ( ( F  o.  F )  o.  b )  =  ( F  o.  ( F  o.  b )
)
352135coeq1d 5036 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F  o.  F )  =  ( F  o.  F ) )
353 f1ococnv1 5706 . . . . . . . . . . . . 13  |-  ( F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  ( `' F  o.  F )  =  (  _I  |`  (
1 ... ( N  + 
1 ) ) ) )
35430, 353syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F  o.  F )  =  (  _I  |`  ( 1 ... ( N  + 
1 ) ) ) )
355352, 354eqtr3d 2472 . . . . . . . . . . 11  |-  ( ph  ->  ( F  o.  F
)  =  (  _I  |`  ( 1 ... ( N  +  1 ) ) ) )
356355adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( F  o.  F
)  =  (  _I  |`  ( 1 ... ( N  +  1 ) ) ) )
357356coeq1d 5036 . . . . . . . . 9  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  F )  o.  b
)  =  ( (  _I  |`  ( 1 ... ( N  + 
1 ) ) )  o.  b ) )
358 fcoi2 5620 . . . . . . . . . 10  |-  ( b : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) )  -> 
( (  _I  |`  (
1 ... ( N  + 
1 ) ) )  o.  b )  =  b )
359345, 358syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( (  _I  |`  (
1 ... ( N  + 
1 ) ) )  o.  b )  =  b )
360357, 359eqtrd 2470 . . . . . . . 8  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  F )  o.  b
)  =  b )
361351, 360syl5eqr 2484 . . . . . . 7  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( F  o.  ( F  o.  b )
)  =  b )
362361eqeq1d 2446 . . . . . 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 ) ) ) )
36383adantrr 699 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  b ) `  1
)  =  1 )
364242adantrl 698 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 )  =  1 )
365363, 364eqtr4d 2473 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  b ) `  1
)  =  ( ( { <. 1 ,  1
>. }  u.  c ) `
 1 ) )
366 fveq2 5730 . . . . . . . . . . . . . 14  |-  ( y  =  1  ->  (
( F  o.  b
) `  y )  =  ( ( F  o.  b ) ` 
1 ) )
367 fveq2 5730 . . . . . . . . . . . . . 14  |-  ( y  =  1  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  =  ( ( { <. 1 ,  1
>. }  u.  c ) `
 1 ) )
368366, 367eqeq12d 2452 . . . . . . . . . . . . 13  |-  ( y  =  1  ->  (
( ( F  o.  b ) `  y
)  =  ( ( { <. 1 ,  1
>. }  u.  c ) `
 y )  <->  ( ( F  o.  b ) `  1 )  =  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) ) )
36963, 368ralsn 3851 . . . . . . . . . . . 12  |-  ( A. y  e.  { 1 }  ( ( F  o.  b ) `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
)  <->  ( ( F  o.  b ) ` 
1 )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  1
) )
370365, 369sylibr 205 . . . . . . . . . . 11  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  ->  A. y  e.  { 1 }  ( ( F  o.  b ) `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
) )
371370biantrurd 496 . . . . . . . . . 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 ) ) ) )
372 ralunb 3530 . . . . . . . . . 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
) ) )
373371, 372syl6bbr 256 . . . . . . . . 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 ) ) )
374187adantl 454 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
b  e.  B  /\  c  e.  C )
)  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( ( F  o.  b )  |`  (
2 ... ( N  + 
1 ) ) ) `
 y )  =  ( ( F  o.  b ) `  y
) )
375374eqcomd 2443 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
b  e.  B  /\  c  e.  C )
)  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( F  o.  b
) `  y )  =  ( ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) `  y
) )
376258adantlrl 702 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
b  e.  B  /\  c  e.  C )
)  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  =  ( c `
 y ) )
377375, 376eqeq12d 2452 . . . . . . . . . 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 ) ) )
378377ralbidva 2723 . . . . . . . . 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 ) ) )
379102adantr 453 . . . . . . . . . 10  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  =  ( 1 ... ( N  +  1 ) ) )
380379raleqdv 2912 . . . . . . . . 9  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( A. y  e.  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) ( ( F  o.  b
) `  y )  =  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 y )  <->  A. y  e.  ( 1 ... ( N  +  1 ) ) ( ( F  o.  b ) `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
) ) )
381373, 378, 3803bitr3rd 277 . . . . . . . 8  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( A. y  e.  ( 1 ... ( 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 ) ) )
38265adantrr 699 . . . . . . . . 9  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( F  o.  b
)  Fn  ( 1 ... ( N  + 
1 ) ) )
383214adantrl 698 . . . . . . . . . 10  |-  ( (
ph  /\  ( b  e.  B  /\  c