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

Theorem subfacp1lem5 24823
Description: Lemma for subfacp1 24825. In subfacp1lem6 24824 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 11266 . . . . . . . . 9  |-  ( 1 ... ( N  + 
1 ) )  e. 
Fin
3 deranglem 24805 . . . . . . . . 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 2474 . . . . . . 7  |-  A  e. 
Fin
6 subfacp1lem5.b . . . . . . . 8  |-  B  =  { g  e.  A  |  ( ( g `
 1 )  =  M  /\  ( g `
 M )  =/=  1 ) }
7 ssrab2 3388 . . . . . . . 8  |-  { g  e.  A  |  ( ( g `  1
)  =  M  /\  ( g `  M
)  =/=  1 ) }  C_  A
86, 7eqsstri 3338 . . . . . . 7  |-  B  C_  A
9 ssfi 7288 . . . . . . 7  |-  ( ( A  e.  Fin  /\  B  C_  A )  ->  B  e.  Fin )
105, 8, 9mp2an 654 . . . . . 6  |-  B  e. 
Fin
1110elexi 2925 . . . . 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 11266 . . . . . . . 8  |-  ( 2 ... ( N  + 
1 ) )  e. 
Fin
15 deranglem 24805 . . . . . . . 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 2474 . . . . . 6  |-  C  e. 
Fin
1817elexi 2925 . . . . 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 5672 . . . . . . . . . . . . . 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 24819 . . . . . . . . . . . 12  |-  ( ph  ->  ( F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  /\  ( F ` 
1 )  =  M  /\  ( F `  M )  =  1 ) )
3029simp1d 969 . . . . . . . . . . 11  |-  ( ph  ->  F : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) ) )
3130adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  B )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
32 simpr 448 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  b  e.  B )  ->  b  e.  B )
33 fveq1 5686 . . . . . . . . . . . . . . . . 17  |-  ( g  =  b  ->  (
g `  1 )  =  ( b ` 
1 ) )
3433eqeq1d 2412 . . . . . . . . . . . . . . . 16  |-  ( g  =  b  ->  (
( g `  1
)  =  M  <->  ( b `  1 )  =  M ) )
35 fveq1 5686 . . . . . . . . . . . . . . . . 17  |-  ( g  =  b  ->  (
g `  M )  =  ( b `  M ) )
3635neeq1d 2580 . . . . . . . . . . . . . . . 16  |-  ( g  =  b  ->  (
( g `  M
)  =/=  1  <->  (
b `  M )  =/=  1 ) )
3734, 36anbi12d 692 . . . . . . . . . . . . . . 15  |-  ( g  =  b  ->  (
( ( g ` 
1 )  =  M  /\  ( g `  M )  =/=  1
)  <->  ( ( b `
 1 )  =  M  /\  ( b `
 M )  =/=  1 ) ) )
3837, 6elrab2 3054 . . . . . . . . . . . . . 14  |-  ( b  e.  B  <->  ( b  e.  A  /\  (
( b `  1
)  =  M  /\  ( b `  M
)  =/=  1 ) ) )
3932, 38sylib 189 . . . . . . . . . . . . 13  |-  ( (
ph  /\  b  e.  B )  ->  (
b  e.  A  /\  ( ( b ` 
1 )  =  M  /\  ( b `  M )  =/=  1
) ) )
4039simpld 446 . . . . . . . . . . . 12  |-  ( (
ph  /\  b  e.  B )  ->  b  e.  A )
41 vex 2919 . . . . . . . . . . . . 13  |-  b  e. 
_V
42 f1oeq1 5624 . . . . . . . . . . . . . 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 5686 . . . . . . . . . . . . . . . 16  |-  ( f  =  b  ->  (
f `  y )  =  ( b `  y ) )
4443neeq1d 2580 . . . . . . . . . . . . . . 15  |-  ( f  =  b  ->  (
( f `  y
)  =/=  y  <->  ( b `  y )  =/=  y
) )
4544ralbidv 2686 . . . . . . . . . . . . . 14  |-  ( f  =  b  ->  ( A. y  e.  (
1 ... ( N  + 
1 ) ) ( f `  y )  =/=  y  <->  A. y  e.  ( 1 ... ( N  +  1 ) ) ( b `  y )  =/=  y
) )
4642, 45anbi12d 692 . . . . . . . . . . . . 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 3045 . . . . . . . . . . . 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 189 . . . . . . . . . . 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 446 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  B )  ->  b : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
50 f1oco 5657 . . . . . . . . . 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 643 . . . . . . . . 9  |-  ( (
ph  /\  b  e.  B )  ->  ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
52 f1of1 5632 . . . . . . . . 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 5418 . . . . . . . . . 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 451 . . . . . . . . 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 5634 . . . . . . . . . . . 12  |-  ( ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  ( F  o.  b )  Fn  (
1 ... ( N  + 
1 ) ) )
57 fnresdm 5513 . . . . . . . . . . . 12  |-  ( ( F  o.  b )  Fn  ( 1 ... ( N  +  1 ) )  ->  (
( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) )  =  ( F  o.  b
) )
5851, 56, 573syl 19 . . . . . . . . . . 11  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) )  =  ( F  o.  b
) )
59 f1oeq1 5624 . . . . . . . . . . 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 16 . . . . . . . . . 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 224 . . . . . . . . 9  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
62 f1ofo 5640 . . . . . . . . 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 16 . . . . . . . 8  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 1 ... ( N  +  1 ) ) ) : ( 1 ... ( N  +  1 ) ) -onto-> ( 1 ... ( N  +  1 ) ) )
64 1ex 9042 . . . . . . . . . . 11  |-  1  e.  _V
6564, 64f1osn 5674 . . . . . . . . . 10  |-  { <. 1 ,  1 >. } : { 1 } -1-1-onto-> { 1 }
6651, 56syl 16 . . . . . . . . . . . . 13  |-  ( (
ph  /\  b  e.  B )  ->  ( F  o.  b )  Fn  ( 1 ... ( N  +  1 ) ) )
6722peano2nnd 9973 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( N  +  1 )  e.  NN )
68 nnuz 10477 . . . . . . . . . . . . . . . 16  |-  NN  =  ( ZZ>= `  1 )
6967, 68syl6eleq 2494 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( N  +  1 )  e.  ( ZZ>= ` 
1 ) )
70 eluzfz1 11020 . . . . . . . . . . . . . . 15  |-  ( ( N  +  1 )  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... ( N  +  1 ) ) )
7169, 70syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  1  e.  ( 1 ... ( N  + 
1 ) ) )
7271adantr 452 . . . . . . . . . . . . 13  |-  ( (
ph  /\  b  e.  B )  ->  1  e.  ( 1 ... ( N  +  1 ) ) )
73 fnressn 5877 . . . . . . . . . . . . 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 643 . . . . . . . . . . . 12  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  { 1 } )  =  { <. 1 ,  ( ( F  o.  b ) `  1 ) >. } )
75 f1of 5633 . . . . . . . . . . . . . . . . 17  |-  ( b : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  b :
( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) ) )
7649, 75syl 16 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  b  e.  B )  ->  b : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
77 fvco3 5759 . . . . . . . . . . . . . . . 16  |-  ( ( b : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  1  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( ( F  o.  b ) `  1 )  =  ( F `  (
b `  1 )
) )
7876, 72, 77syl2anc 643 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
) `  1 )  =  ( F `  ( b `  1
) ) )
7939simprd 450 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  b  e.  B )  ->  (
( b `  1
)  =  M  /\  ( b `  M
)  =/=  1 ) )
8079simpld 446 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  b  e.  B )  ->  (
b `  1 )  =  M )
8180fveq2d 5691 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  B )  ->  ( F `  ( b `  1 ) )  =  ( F `  M ) )
8229simp3d 971 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  ( F `  M
)  =  1 )
8382adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  B )  ->  ( F `  M )  =  1 )
8478, 81, 833eqtrd 2440 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
) `  1 )  =  1 )
8584opeq2d 3951 . . . . . . . . . . . . 13  |-  ( (
ph  /\  b  e.  B )  ->  <. 1 ,  ( ( F  o.  b ) ` 
1 ) >.  =  <. 1 ,  1 >. )
8685sneqd 3787 . . . . . . . . . . . 12  |-  ( (
ph  /\  b  e.  B )  ->  { <. 1 ,  ( ( F  o.  b ) `  1 ) >. }  =  { <. 1 ,  1 >. } )
8774, 86eqtrd 2436 . . . . . . . . . . 11  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  { 1 } )  =  { <. 1 ,  1 >. } )
88 f1oeq1 5624 . . . . . . . . . . 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 16 . . . . . . . . . 10  |-  ( (
ph  /\  b  e.  B )  ->  (
( ( F  o.  b )  |`  { 1 } ) : {
1 } -1-1-onto-> { 1 }  <->  { <. 1 ,  1 >. } : { 1 } -1-1-onto-> { 1 } ) )
9065, 89mpbiri 225 . . . . . . . . 9  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  { 1 } ) : { 1 } -1-1-onto-> { 1 } )
91 f1ofo 5640 . . . . . . . . 9  |-  ( ( ( F  o.  b
)  |`  { 1 } ) : { 1 } -1-1-onto-> { 1 }  ->  ( ( F  o.  b
)  |`  { 1 } ) : { 1 } -onto-> { 1 } )
9290, 91syl 16 . . . . . . . 8  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  { 1 } ) : { 1 } -onto-> { 1 } )
93 resdif 5655 . . . . . . . 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 1184 . . . . . . 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 11033 . . . . . . . . . . . 12  |-  ( 1  e.  ( 1 ... ( N  +  1 ) )  ->  (
1 ... ( N  + 
1 ) )  =  ( ( 1 ... 1 )  u.  (
( 1  +  1 ) ... ( N  +  1 ) ) ) )
9671, 95syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( 1 ... ( N  +  1 ) )  =  ( ( 1 ... 1 )  u.  ( ( 1  +  1 ) ... ( N  +  1 ) ) ) )
97 1z 10267 . . . . . . . . . . . . 13  |-  1  e.  ZZ
98 fzsn 11050 . . . . . . . . . . . . 13  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
9997, 98ax-mp 8 . . . . . . . . . . . 12  |-  ( 1 ... 1 )  =  { 1 }
100 1p1e2 10050 . . . . . . . . . . . . 13  |-  ( 1  +  1 )  =  2
101100oveq1i 6050 . . . . . . . . . . . 12  |-  ( ( 1  +  1 ) ... ( N  + 
1 ) )  =  ( 2 ... ( N  +  1 ) )
10299, 101uneq12i 3459 . . . . . . . . . . 11  |-  ( ( 1 ... 1 )  u.  ( ( 1  +  1 ) ... ( N  +  1 ) ) )  =  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )
10396, 102syl6req 2453 . . . . . . . . . 10  |-  ( ph  ->  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  =  ( 1 ... ( N  +  1 ) ) )
10471snssd 3903 . . . . . . . . . . 11  |-  ( ph  ->  { 1 }  C_  ( 1 ... ( N  +  1 ) ) )
105 incom 3493 . . . . . . . . . . . 12  |-  ( { 1 }  i^i  (
2 ... ( N  + 
1 ) ) )  =  ( ( 2 ... ( N  + 
1 ) )  i^i 
{ 1 } )
106 1lt2 10098 . . . . . . . . . . . . . . 15  |-  1  <  2
107 1re 9046 . . . . . . . . . . . . . . . 16  |-  1  e.  RR
108 2re 10025 . . . . . . . . . . . . . . . 16  |-  2  e.  RR
109107, 108ltnlei 9150 . . . . . . . . . . . . . . 15  |-  ( 1  <  2  <->  -.  2  <_  1 )
110106, 109mpbi 200 . . . . . . . . . . . . . 14  |-  -.  2  <_  1
111 elfzle1 11016 . . . . . . . . . . . . . 14  |-  ( 1  e.  ( 2 ... ( N  +  1 ) )  ->  2  <_  1 )
112110, 111mto 169 . . . . . . . . . . . . 13  |-  -.  1  e.  ( 2 ... ( N  +  1 ) )
113 disjsn 3828 . . . . . . . . . . . . 13  |-  ( ( ( 2 ... ( N  +  1 ) )  i^i  { 1 } )  =  (/)  <->  -.  1  e.  ( 2 ... ( N  + 
1 ) ) )
114112, 113mpbir 201 . . . . . . . . . . . 12  |-  ( ( 2 ... ( N  +  1 ) )  i^i  { 1 } )  =  (/)
115105, 114eqtri 2424 . . . . . . . . . . 11  |-  ( { 1 }  i^i  (
2 ... ( N  + 
1 ) ) )  =  (/)
116 uneqdifeq 3676 . . . . . . . . . . 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 644 . . . . . . . . . 10  |-  ( ph  ->  ( ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) )  =  ( 1 ... ( N  +  1 ) )  <->  ( (
1 ... ( N  + 
1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) ) ) )
118103, 117mpbid 202 . . . . . . . . 9  |-  ( ph  ->  ( ( 1 ... ( N  +  1 ) )  \  {
1 } )  =  ( 2 ... ( N  +  1 ) ) )
119118adantr 452 . . . . . . . 8  |-  ( (
ph  /\  b  e.  B )  ->  (
( 1 ... ( N  +  1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) ) )
120 reseq2 5100 . . . . . . . . . 10  |-  ( ( ( 1 ... ( N  +  1 ) )  \  { 1 } )  =  ( 2 ... ( N  +  1 ) )  ->  ( ( F  o.  b )  |`  ( ( 1 ... ( N  +  1 ) )  \  {
1 } ) )  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) )
121 f1oeq1 5624 . . . . . . . . . 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 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 } ) ) )
123 f1oeq2 5625 . . . . . . . . 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 5626 . . . . . . . . 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 271 . . . . . . . 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 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 ) ) ) )
12794, 126mpbid 202 . . . . . 6  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 2 ... ( N  +  1 ) ) ) : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) )
12876adantr 452 . . . . . . . . 9  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  b : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
129 fzp1ss 11054 . . . . . . . . . . . 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 3339 . . . . . . . . . 10  |-  ( 2 ... ( N  + 
1 ) )  C_  ( 1 ... ( N  +  1 ) )
132 simpr 448 . . . . . . . . . 10  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  y  e.  ( 2 ... ( N  +  1 ) ) )
133131, 132sseldi 3306 . . . . . . . . 9  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  y  e.  ( 1 ... ( N  +  1 ) ) )
134 fvco3 5759 . . . . . . . . 9  |-  ( ( b : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( ( F  o.  b ) `  y )  =  ( F `  ( b `
 y ) ) )
135128, 133, 134syl2anc 643 . . . . . . . 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 24822 . . . . . . . . . . . 12  |-  ( ph  ->  `' F  =  F
)
137136fveq1d 5689 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F `  y )  =  ( F `  y ) )
138137ad2antrr 707 . . . . . . . . . 10  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( `' F `  y )  =  ( F `  y ) )
13979simprd 450 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  b  e.  B )  ->  (
b `  M )  =/=  1 )
140139, 83neeqtrrd 2591 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  b  e.  B )  ->  (
b `  M )  =/=  ( F `  M
) )
141140adantr 452 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
b `  M )  =/=  ( F `  M
) )
142 fveq2 5687 . . . . . . . . . . . . . 14  |-  ( y  =  M  ->  (
b `  y )  =  ( b `  M ) )
143 fveq2 5687 . . . . . . . . . . . . . 14  |-  ( y  =  M  ->  ( F `  y )  =  ( F `  M ) )
144142, 143neeq12d 2582 . . . . . . . . . . . . 13  |-  ( y  =  M  ->  (
( b `  y
)  =/=  ( F `
 y )  <->  ( b `  M )  =/=  ( F `  M )
) )
145141, 144syl5ibrcom 214 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
y  =  M  -> 
( b `  y
)  =/=  ( F `
 y ) ) )
146131sseli 3304 . . . . . . . . . . . . . . . 16  |-  ( y  e.  ( 2 ... ( N  +  1 ) )  ->  y  e.  ( 1 ... ( N  +  1 ) ) )
14748simprd 450 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  b  e.  B )  ->  A. y  e.  ( 1 ... ( N  +  1 ) ) ( b `  y )  =/=  y
)
148147r19.21bi 2764 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
b `  y )  =/=  y )
149146, 148sylan2 461 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
b `  y )  =/=  y )
150149adantrr 698 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  b  e.  B )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( b `  y )  =/=  y
)
15125eleq2i 2468 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  K  <->  y  e.  ( ( 2 ... ( N  +  1 ) )  \  { M } ) )
152 eldifsn 3887 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  ( ( 2 ... ( N  + 
1 ) )  \  { M } )  <->  ( y  e.  ( 2 ... ( N  +  1 ) )  /\  y  =/= 
M ) )
153151, 152bitri 241 . . . . . . . . . . . . . . . 16  |-  ( y  e.  K  <->  ( y  e.  ( 2 ... ( N  +  1 ) )  /\  y  =/= 
M ) )
15420, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2b 24820 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  K )  ->  ( F `  y )  =  ( (  _I  |`  K ) `  y
) )
155 fvresi 5883 . . . . . . . . . . . . . . . . . 18  |-  ( y  e.  K  ->  (
(  _I  |`  K ) `
 y )  =  y )
156155adantl 453 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  y  e.  K )  ->  (
(  _I  |`  K ) `
 y )  =  y )
157154, 156eqtrd 2436 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  y  e.  K )  ->  ( F `  y )  =  y )
158153, 157sylan2br 463 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( y  e.  ( 2 ... ( N  +  1 ) )  /\  y  =/= 
M ) )  -> 
( F `  y
)  =  y )
159158adantlr 696 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  b  e.  B )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( F `  y )  =  y )
160150, 159neeqtrrd 2591 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  b  e.  B )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( b `  y )  =/=  ( F `  y )
)
161160expr 599 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
y  =/=  M  -> 
( b `  y
)  =/=  ( F `
 y ) ) )
162145, 161pm2.61dne 2644 . . . . . . . . . . 11  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
b `  y )  =/=  ( F `  y
) )
163162necomd 2650 . . . . . . . . . 10  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( F `  y )  =/=  ( b `  y
) )
164138, 163eqnetrd 2585 . . . . . . . . 9  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( `' F `  y )  =/=  ( b `  y ) )
16531adantr 452 . . . . . . . . . . 11  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
166 ffvelrn 5827 . . . . . . . . . . . 12  |-  ( ( b : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( b `  y )  e.  ( 1 ... ( N  +  1 ) ) )
16776, 146, 166syl2an 464 . . . . . . . . . . 11  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
b `  y )  e.  ( 1 ... ( N  +  1 ) ) )
168 f1ocnvfv 5975 . . . . . . . . . . 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 643 . . . . . . . . . 10  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( F `  (
b `  y )
)  =  y  -> 
( `' F `  y )  =  ( b `  y ) ) )
170169necon3d 2605 . . . . . . . . 9  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( `' F `  y )  =/=  (
b `  y )  ->  ( F `  (
b `  y )
)  =/=  y ) )
171164, 170mpd 15 . . . . . . . 8  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( F `  ( b `  y ) )  =/=  y )
172135, 171eqnetrd 2585 . . . . . . 7  |-  ( ( ( ph  /\  b  e.  B )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( F  o.  b
) `  y )  =/=  y )
173172ralrimiva 2749 . . . . . 6  |-  ( (
ph  /\  b  e.  B )  ->  A. y  e.  ( 2 ... ( N  +  1 ) ) ( ( F  o.  b ) `  y )  =/=  y
)
174 f1of 5633 . . . . . . . . . . . . 13  |-  ( (  _I  |`  K ) : K -1-1-onto-> K  ->  (  _I  |`  K ) : K --> K )
17527, 174ax-mp 8 . . . . . . . . . . . 12  |-  (  _I  |`  K ) : K --> K
176 difexg 4311 . . . . . . . . . . . . . 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 2474 . . . . . . . . . . . 12  |-  K  e. 
_V
179 fex 5928 . . . . . . . . . . . 12  |-  ( ( (  _I  |`  K ) : K --> K  /\  K  e.  _V )  ->  (  _I  |`  K )  e.  _V )
180175, 178, 179mp2an 654 . . . . . . . . . . 11  |-  (  _I  |`  K )  e.  _V
181 prex 4366 . . . . . . . . . . 11  |-  { <. 1 ,  M >. , 
<. M ,  1 >. }  e.  _V
182180, 181unex 4666 . . . . . . . . . 10  |-  ( (  _I  |`  K )  u.  { <. 1 ,  M >. ,  <. M ,  1
>. } )  e.  _V
18326, 182eqeltri 2474 . . . . . . . . 9  |-  F  e. 
_V
184183, 41coex 5372 . . . . . . . 8  |-  ( F  o.  b )  e. 
_V
185184resex 5145 . . . . . . 7  |-  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  e.  _V
186 f1oeq1 5624 . . . . . . . 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 5686 . . . . . . . . . . 11  |-  ( f  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  ->  (
f `  y )  =  ( ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) `  y
) )
188 fvres 5704 . . . . . . . . . . 11  |-  ( y  e.  ( 2 ... ( N  +  1 ) )  ->  (
( ( F  o.  b )  |`  (
2 ... ( N  + 
1 ) ) ) `
 y )  =  ( ( F  o.  b ) `  y
) )
189187, 188sylan9eq 2456 . . . . . . . . . 10  |-  ( ( f  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
f `  y )  =  ( ( F  o.  b ) `  y ) )
190189neeq1d 2580 . . . . . . . . 9  |-  ( ( f  =  ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( f `  y
)  =/=  y  <->  ( ( F  o.  b ) `  y )  =/=  y
) )
191190ralbidva 2682 . . . . . . . 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 692 . . . . . . 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 3045 . . . . . 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 646 . . . . 5  |-  ( (
ph  /\  b  e.  B )  ->  (
( F  o.  b
)  |`  ( 2 ... ( N  +  1 ) ) )  e.  C )
195194ex 424 . . . 4  |-  ( ph  ->  ( b  e.  B  ->  ( ( F  o.  b )  |`  (
2 ... ( N  + 
1 ) ) )  e.  C ) )
19630adantr 452 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
197 simpr 448 . . . . . . . . . . . 12  |-  ( (
ph  /\  c  e.  C )  ->  c  e.  C )
198 vex 2919 . . . . . . . . . . . . 13  |-  c  e. 
_V
199 f1oeq1 5624 . . . . . . . . . . . . . 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 5686 . . . . . . . . . . . . . . . 16  |-  ( f  =  c  ->  (
f `  y )  =  ( c `  y ) )
201200neeq1d 2580 . . . . . . . . . . . . . . 15  |-  ( f  =  c  ->  (
( f `  y
)  =/=  y  <->  ( c `  y )  =/=  y
) )
202201ralbidv 2686 . . . . . . . . . . . . . 14  |-  ( f  =  c  ->  ( A. y  e.  (
2 ... ( N  + 
1 ) ) ( f `  y )  =/=  y  <->  A. y  e.  ( 2 ... ( N  +  1 ) ) ( c `  y )  =/=  y
) )
203199, 202anbi12d 692 . . . . . . . . . . . . 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 3045 . . . . . . . . . . . 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 189 . . . . . . . . . . 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 446 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) ) )
207 f1oun 5653 . . . . . . . . . . 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 667 . . . . . . . . . 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 645 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  ( { <. 1 ,  1
>. }  u.  c ) : ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) ) -1-1-onto-> ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) )
210 f1oeq2 5625 . . . . . . . . . . . 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 5626 . . . . . . . . . . . 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 245 . . . . . . . . . . 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 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 ) ) ) )
214213biimpa 471 . . . . . . . . 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 457 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  ( { <. 1 ,  1
>. }  u.  c ) : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
216 f1oco 5657 . . . . . . . 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 643 . . . . . . 7  |-  ( (
ph  /\  c  e.  C )  ->  ( F  o.  ( { <. 1 ,  1 >. }  u.  c )
) : ( 1 ... ( N  + 
1 ) ) -1-1-onto-> ( 1 ... ( N  + 
1 ) ) )
218 f1of 5633 . . . . . . . . . . 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 16 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  ( { <. 1 ,  1
>. }  u.  c ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
220 fvco3 5759 . . . . . . . . . 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 458 . . . . . . . . 9  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  y )  =  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) ) )
222137ad2antrr 707 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( `' F `  y )  =  ( F `  y ) )
223 simpr 448 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  y  e.  ( 1 ... ( N  +  1 ) ) )
224103ad2antrr 707 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  =  ( 1 ... ( N  +  1 ) ) )
225223, 224eleqtrrd 2481 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  y  e.  ( { 1 }  u.  ( 2 ... ( N  +  1 ) ) ) )
226 elun 3448 . . . . . . . . . . . . 13  |-  ( y  e.  ( { 1 }  u.  ( 2 ... ( N  + 
1 ) ) )  <-> 
( y  e.  {
1 }  \/  y  e.  ( 2 ... ( N  +  1 ) ) ) )
227225, 226sylib 189 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
y  e.  { 1 }  \/  y  e.  ( 2 ... ( N  +  1 ) ) ) )
228 nelne2 2657 . . . . . . . . . . . . . . . . . 18  |-  ( ( M  e.  ( 2 ... ( N  + 
1 ) )  /\  -.  1  e.  (
2 ... ( N  + 
1 ) ) )  ->  M  =/=  1
)
22923, 112, 228sylancl 644 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  M  =/=  1 )
230229adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  C )  ->  M  =/=  1 )
23129simp2d 970 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( F `  1
)  =  M )
232231adantr 452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  1 )  =  M )
233 f1ofun 5635 . . . . . . . . . . . . . . . . . . 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 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  c  e.  C )  ->  Fun  ( { <. 1 ,  1
>. }  u.  c ) )
235 ssun1 3470 . . . . . . . . . . . . . . . . . . 19  |-  { <. 1 ,  1 >. } 
C_  ( { <. 1 ,  1 >. }  u.  c )
23664snid 3801 . . . . . . . . . . . . . . . . . . . 20  |-  1  e.  { 1 }
23764dmsnop 5303 . . . . . . . . . . . . . . . . . . . 20  |-  dom  { <. 1 ,  1 >. }  =  { 1 }
238236, 237eleqtrri 2477 . . . . . . . . . . . . . . . . . . 19  |-  1  e.  dom  { <. 1 ,  1 >. }
239 funssfv 5705 . . . . . . . . . . . . . . . . . . 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 1271 . . . . . . . . . . . . . . . . . 18  |-  ( Fun  ( { <. 1 ,  1 >. }  u.  c )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  1
)  =  ( {
<. 1 ,  1
>. } `  1 ) )
241234, 240syl 16 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  c  e.  C )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  1
)  =  ( {
<. 1 ,  1
>. } `  1 ) )
24264, 64fvsn 5885 . . . . . . . . . . . . . . . . 17  |-  ( {
<. 1 ,  1
>. } `  1 )  =  1
243241, 242syl6eq 2452 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c  e.  C )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  1
)  =  1 )
244230, 232, 2433netr4d 2594 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  1 )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) )
245 elsni 3798 . . . . . . . . . . . . . . . . 17  |-  ( y  e.  { 1 }  ->  y  =  1 )
246245fveq2d 5691 . . . . . . . . . . . . . . . 16  |-  ( y  e.  { 1 }  ->  ( F `  y )  =  ( F `  1 ) )
247245fveq2d 5691 . . . . . . . . . . . . . . . 16  |-  ( y  e.  { 1 }  ->  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) )
248246, 247neeq12d 2582 . . . . . . . . . . . . . . 15  |-  ( y  e.  { 1 }  ->  ( ( F `
 y )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) `  y )  <->  ( F `  1 )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) ) )
249244, 248syl5ibrcom 214 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c  e.  C )  ->  (
y  e.  { 1 }  ->  ( F `  y )  =/=  (
( { <. 1 ,  1 >. }  u.  c ) `  y
) ) )
250249imp 419 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  { 1 } )  ->  ( F `  y )  =/=  (
( { <. 1 ,  1 >. }  u.  c ) `  y
) )
251234adantr 452 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  Fun  ( { <. 1 ,  1
>. }  u.  c ) )
252 ssun2 3471 . . . . . . . . . . . . . . . . 17  |-  c  C_  ( { <. 1 ,  1
>. }  u.  c )
253252a1i 11 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  c  C_  ( { <. 1 ,  1 >. }  u.  c ) )
254 f1odm 5637 . . . . . . . . . . . . . . . . . . 19  |-  ( c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  ->  dom  c  =  ( 2 ... ( N  +  1 ) ) )
255206, 254syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  c  e.  C )  ->  dom  c  =  ( 2 ... ( N  + 
1 ) ) )
256255eleq2d 2471 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  c  e.  C )  ->  (
y  e.  dom  c  <->  y  e.  ( 2 ... ( N  +  1 ) ) ) )
257256biimpar 472 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  y  e.  dom  c )
258 funssfv 5705 . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  =  ( c `
 y ) )
260 f1of 5633 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( c : ( 2 ... ( N  +  1 ) ) -1-1-onto-> ( 2 ... ( N  +  1 ) )  ->  c :
( 2 ... ( N  +  1 ) ) --> ( 2 ... ( N  +  1 ) ) )
261206, 260syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  c  e.  C )  ->  c : ( 2 ... ( N  +  1 ) ) --> ( 2 ... ( N  + 
1 ) ) )
26223adantr 452 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (
ph  /\  c  e.  C )  ->  M  e.  ( 2 ... ( N  +  1 ) ) )
263261, 262ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  c  e.  C )  ->  (
c `  M )  e.  ( 2 ... ( N  +  1 ) ) )
264 nelne2 2657 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( c `  M
)  e.  ( 2 ... ( N  + 
1 ) )  /\  -.  1  e.  (
2 ... ( N  + 
1 ) ) )  ->  ( c `  M )  =/=  1
)
265263, 112, 264sylancl 644 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  c  e.  C )  ->  (
c `  M )  =/=  1 )
266265adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
c `  M )  =/=  1 )
26782ad2antrr 707 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( F `  M )  =  1 )
268266, 267neeqtrrd 2591 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
c `  M )  =/=  ( F `  M
) )
269 fveq2 5687 . . . . . . . . . . . . . . . . . 18  |-  ( y  =  M  ->  (
c `  y )  =  ( c `  M ) )
270269, 143neeq12d 2582 . . . . . . . . . . . . . . . . 17  |-  ( y  =  M  ->  (
( c `  y
)  =/=  ( F `
 y )  <->  ( c `  M )  =/=  ( F `  M )
) )
271268, 270syl5ibrcom 214 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
y  =  M  -> 
( c `  y
)  =/=  ( F `
 y ) ) )
272205simprd 450 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  c  e.  C )  ->  A. y  e.  ( 2 ... ( N  +  1 ) ) ( c `  y )  =/=  y
)
273272r19.21bi 2764 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
c `  y )  =/=  y )
274273adantrr 698 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  C )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( c `  y )  =/=  y
)
275158adantlr 696 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  c  e.  C )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( F `  y )  =  y )
276274, 275neeqtrrd 2591 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  c  e.  C )  /\  (
y  e.  ( 2 ... ( N  + 
1 ) )  /\  y  =/=  M ) )  ->  ( c `  y )  =/=  ( F `  y )
)
277276expr 599 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
y  =/=  M  -> 
( c `  y
)  =/=  ( F `
 y ) ) )
278271, 277pm2.61dne 2644 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
c `  y )  =/=  ( F `  y
) )
279259, 278eqnetrd 2585 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  =/=  ( F `
 y ) )
280279necomd 2650 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  ( F `  y )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) )
281250, 280jaodan 761 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  C )  /\  (
y  e.  { 1 }  \/  y  e.  ( 2 ... ( N  +  1 ) ) ) )  -> 
( F `  y
)  =/=  ( ( { <. 1 ,  1
>. }  u.  c ) `
 y ) )
282227, 281syldan 457 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( F `  y )  =/=  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) )
283222, 282eqnetrd 2585 . . . . . . . . . 10  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( `' F `  y )  =/=  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 y ) )
284196adantr 452 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
285219ffvelrnda 5829 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  e.  ( 1 ... ( N  + 
1 ) ) )
286 f1ocnvfv 5975 . . . . . . . . . . . 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 ) ) )
287284, 285, 286syl2anc 643 . . . . . . . . . . 11  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( F `  (
( { <. 1 ,  1 >. }  u.  c ) `  y
) )  =  y  ->  ( `' F `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
) ) )
288287necon3d 2605 . . . . . . . . . 10  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( `' F `  y )  =/=  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  ->  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) `  y ) )  =/=  y ) )
289283, 288mpd 15 . . . . . . . . 9  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  ( F `  ( ( { <. 1 ,  1
>. }  u.  c ) `
 y ) )  =/=  y )
290221, 289eqnetrd 2585 . . . . . . . 8  |-  ( ( ( ph  /\  c  e.  C )  /\  y  e.  ( 1 ... ( N  +  1 ) ) )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  y )  =/=  y )
291290ralrimiva 2749 . . . . . . 7  |-  ( (
ph  /\  c  e.  C )  ->  A. y  e.  ( 1 ... ( N  +  1 ) ) ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 y )  =/=  y )
292 snex 4365 . . . . . . . . . 10  |-  { <. 1 ,  1 >. }  e.  _V
293292, 198unex 4666 . . . . . . . . 9  |-  ( {
<. 1 ,  1
>. }  u.  c )  e.  _V
294183, 293coex 5372 . . . . . . . 8  |-  ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) )  e.  _V
295 f1oeq1 5624 . . . . . . . . 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 ) ) ) )
296 fveq1 5686 . . . . . . . . . . 11  |-  ( f  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( f `  y )  =  ( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  y ) )
297296neeq1d 2580 . . . . . . . . . 10  |-  ( f  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( (
f `  y )  =/=  y  <->  ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 y )  =/=  y ) )
298297ralbidv 2686 . . . . . . . . 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 ) )
299295, 298anbi12d 692 . . . . . . . 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 ) ) )
300294, 299, 1elab2 3045 . . . . . . 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 ) )
301217, 291, 300sylanbrc 646 . . . . . 6  |-  ( (
ph  /\  c  e.  C )  ->  ( F  o.  ( { <. 1 ,  1 >. }  u.  c )
)  e.  A )
30271adantr 452 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  1  e.  ( 1 ... ( N  +  1 ) ) )
303 fvco3 5759 . . . . . . . . 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 ) ) )
304219, 302, 303syl2anc 643 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  1 )  =  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) ) )
305243fveq2d 5691 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  ( ( { <. 1 ,  1
>. }  u.  c ) `
 1 ) )  =  ( F ` 
1 ) )
306304, 305, 2323eqtrd 2440 . . . . . . 7  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  1 )  =  M )
307131, 23sseldi 3306 . . . . . . . . . . 11  |-  ( ph  ->  M  e.  ( 1 ... ( N  + 
1 ) ) )
308307adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  M  e.  ( 1 ... ( N  +  1 ) ) )
309 fvco3 5759 . . . . . . . . . 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 ) ) )
310219, 308, 309syl2anc 643 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M )  =  ( F `  ( ( { <. 1 ,  1 >. }  u.  c ) `  M ) ) )
311252a1i 11 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  c  C_  ( { <. 1 ,  1 >. }  u.  c ) )
312262, 255eleqtrrd 2481 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  M  e.  dom  c )
313 funssfv 5705 . . . . . . . . . . 11  |-  ( ( Fun  ( { <. 1 ,  1 >. }  u.  c )  /\  c  C_  ( { <. 1 ,  1 >. }  u.  c )  /\  M  e.  dom  c )  ->  ( ( {
<. 1 ,  1
>. }  u.  c ) `
 M )  =  ( c `  M
) )
314234, 311, 312, 313syl3anc 1184 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  M
)  =  ( c `
 M ) )
315314fveq2d 5691 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  ( ( { <. 1 ,  1
>. }  u.  c ) `
 M ) )  =  ( F `  ( c `  M
) ) )
316310, 315eqtrd 2436 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M )  =  ( F `  ( c `  M
) ) )
317136fveq1d 5689 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F ` 
1 )  =  ( F `  1 ) )
318317, 231eqtrd 2436 . . . . . . . . . . 11  |-  ( ph  ->  ( `' F ` 
1 )  =  M )
319318adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  ( `' F `  1 )  =  M )
320 id 20 . . . . . . . . . . . . . 14  |-  ( y  =  M  ->  y  =  M )
321269, 320neeq12d 2582 . . . . . . . . . . . . 13  |-  ( y  =  M  ->  (
( c `  y
)  =/=  y  <->  ( c `  M )  =/=  M
) )
322321rspcv 3008 . . . . . . . . . . . 12  |-  ( M  e.  ( 2 ... ( N  +  1 ) )  ->  ( A. y  e.  (
2 ... ( N  + 
1 ) ) ( c `  y )  =/=  y  ->  (
c `  M )  =/=  M ) )
323262, 272, 322sylc 58 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  (
c `  M )  =/=  M )
324323necomd 2650 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  M  =/=  ( c `  M
) )
325319, 324eqnetrd 2585 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  ( `' F `  1 )  =/=  ( c `  M ) )
326131, 263sseldi 3306 . . . . . . . . . . 11  |-  ( (
ph  /\  c  e.  C )  ->  (
c `  M )  e.  ( 1 ... ( N  +  1 ) ) )
327 f1ocnvfv 5975 . . . . . . . . . . 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 ) ) )
328196, 326, 327syl2anc 643 . . . . . . . . . 10  |-  ( (
ph  /\  c  e.  C )  ->  (
( F `  (
c `  M )
)  =  1  -> 
( `' F ` 
1 )  =  ( c `  M ) ) )
329328necon3d 2605 . . . . . . . . 9  |-  ( (
ph  /\  c  e.  C )  ->  (
( `' F ` 
1 )  =/=  (
c `  M )  ->  ( F `  (
c `  M )
)  =/=  1 ) )
330325, 329mpd 15 . . . . . . . 8  |-  ( (
ph  /\  c  e.  C )  ->  ( F `  ( c `  M ) )  =/=  1 )
331316, 330eqnetrd 2585 . . . . . . 7  |-  ( (
ph  /\  c  e.  C )  ->  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M )  =/=  1 )
332306, 331jca 519 . . . . . 6  |-  ( (
ph  /\  c  e.  C )  ->  (
( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  1 )  =  M  /\  (
( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M )  =/=  1 ) )
333 fveq1 5686 . . . . . . . . 9  |-  ( g  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( g `  1 )  =  ( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  1 ) )
334333eqeq1d 2412 . . . . . . . 8  |-  ( g  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( (
g `  1 )  =  M  <->  ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 1 )  =  M ) )
335 fveq1 5686 . . . . . . . . 9  |-  ( g  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( g `  M )  =  ( ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) ) `  M ) )
336335neeq1d 2580 . . . . . . . 8  |-  ( g  =  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  ->  ( (
g `  M )  =/=  1  <->  ( ( F  o.  ( { <. 1 ,  1 >. }  u.  c ) ) `
 M )  =/=  1 ) )
337334, 336anbi12d 692 . . . . . . 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 ) ) )
338337, 6elrab2 3054 . . . . . 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 ) ) )
339301, 332, 338sylanbrc 646 . . . . 5  |-  ( (
ph  /\  c  e.  C )  ->  ( F  o.  ( { <. 1 ,  1 >. }  u.  c )
)  e.  B )
340339ex 424 . . . 4  |-  ( ph  ->  ( c  e.  C  ->  ( F  o.  ( { <. 1 ,  1
>. }  u.  c ) )  e.  B ) )
34130adantr 452 . . . . . . . 8  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) ) )
342 f1of1 5632 . . . . . . . 8  |-  ( F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  F :
( 1 ... ( N  +  1 ) ) -1-1-> ( 1 ... ( N  +  1 ) ) )
343341, 342syl 16 . . . . . . 7  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  ->  F : ( 1 ... ( N  +  1 ) ) -1-1-> ( 1 ... ( N  + 
1 ) ) )
344 f1of 5633 . . . . . . . . 9  |-  ( F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  F :
( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) ) )
345341, 344syl 16 . . . . . . . 8  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  ->  F : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
34676adantrr 698 . . . . . . . 8  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
b : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) ) )
347 fco 5559 . . . . . . . 8  |-  ( ( F : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) )  /\  b : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) ) )  ->  ( F  o.  b ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) ) )
348345, 346, 347syl2anc 643 . . . . . . 7  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( F  o.  b
) : ( 1 ... ( N  + 
1 ) ) --> ( 1 ... ( N  +  1 ) ) )
349219adantrl 697 . . . . . . 7  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( { <. 1 ,  1 >. }  u.  c ) : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  +  1 ) ) )
350 cocan1 5983 . . . . . . 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 ) ) )
351343, 348, 349, 350syl3anc 1184 . . . . . 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 ) ) )
352 coass 5347 . . . . . . . 8  |-  ( ( F  o.  F )  o.  b )  =  ( F  o.  ( F  o.  b )
)
353136coeq1d 4993 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F  o.  F )  =  ( F  o.  F ) )
354 f1ococnv1 5663 . . . . . . . . . . . . 13  |-  ( F : ( 1 ... ( N  +  1 ) ) -1-1-onto-> ( 1 ... ( N  +  1 ) )  ->  ( `' F  o.  F )  =  (  _I  |`  (
1 ... ( N  + 
1 ) ) ) )
35530, 354syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( `' F  o.  F )  =  (  _I  |`  ( 1 ... ( N  + 
1 ) ) ) )
356353, 355eqtr3d 2438 . . . . . . . . . . 11  |-  ( ph  ->  ( F  o.  F
)  =  (  _I  |`  ( 1 ... ( N  +  1 ) ) ) )
357356adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( F  o.  F
)  =  (  _I  |`  ( 1 ... ( N  +  1 ) ) ) )
358357coeq1d 4993 . . . . . . . . 9  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  F )  o.  b
)  =  ( (  _I  |`  ( 1 ... ( N  + 
1 ) ) )  o.  b ) )
359 fcoi2 5577 . . . . . . . . . 10  |-  ( b : ( 1 ... ( N  +  1 ) ) --> ( 1 ... ( N  + 
1 ) )  -> 
( (  _I  |`  (
1 ... ( N  + 
1 ) ) )  o.  b )  =  b )
360346, 359syl 16 . . . . . . . . 9  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( (  _I  |`  (
1 ... ( N  + 
1 ) ) )  o.  b )  =  b )
361358, 360eqtrd 2436 . . . . . . . 8  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  F )  o.  b
)  =  b )
362352, 361syl5eqr 2450 . . . . . . 7  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( F  o.  ( F  o.  b )
)  =  b )
363362eqeq1d 2412 . . . . . 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 ) ) ) )
36484adantrr 698 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  b ) `  1
)  =  1 )
365243adantrl 697 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 )  =  1 )
366364, 365eqtr4d 2439 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( ( F  o.  b ) `  1
)  =  ( ( { <. 1 ,  1
>. }  u.  c ) `
 1 ) )
367 fveq2 5687 . . . . . . . . . . . . . 14  |-  ( y  =  1  ->  (
( F  o.  b
) `  y )  =  ( ( F  o.  b ) ` 
1 ) )
368 fveq2 5687 . . . . . . . . . . . . . 14  |-  ( y  =  1  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  =  ( ( { <. 1 ,  1
>. }  u.  c ) `
 1 ) )
369367, 368eqeq12d 2418 . . . . . . . . . . . . 13  |-  ( y  =  1  ->  (
( ( F  o.  b ) `  y
)  =  ( ( { <. 1 ,  1
>. }  u.  c ) `
 y )  <->  ( ( F  o.  b ) `  1 )  =  ( ( { <. 1 ,  1 >. }  u.  c ) ` 
1 ) ) )
37064, 369ralsn 3809 . . . . . . . . . . . 12  |-  ( A. y  e.  { 1 }  ( ( F  o.  b ) `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
)  <->  ( ( F  o.  b ) ` 
1 )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  1
) )
371366, 370sylibr 204 . . . . . . . . . . 11  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  ->  A. y  e.  { 1 }  ( ( F  o.  b ) `  y )  =  ( ( { <. 1 ,  1 >. }  u.  c ) `  y
) )
372371biantrurd 495 . . . . . . . . . 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 ) ) ) )
373 ralunb 3488 . . . . . . . . . 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
) ) )
374372, 373syl6bbr 255 . . . . . . . . 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 ) ) )
375188adantl 453 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  (
b  e.  B  /\  c  e.  C )
)  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( ( F  o.  b )  |`  (
2 ... ( N  + 
1 ) ) ) `
 y )  =  ( ( F  o.  b ) `  y
) )
376375eqcomd 2409 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
b  e.  B  /\  c  e.  C )
)  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( F  o.  b
) `  y )  =  ( ( ( F  o.  b )  |`  ( 2 ... ( N  +  1 ) ) ) `  y
) )
377259adantlrl 701 . . . . . . . . . . 11  |-  ( ( ( ph  /\  (
b  e.  B  /\  c  e.  C )
)  /\  y  e.  ( 2 ... ( N  +  1 ) ) )  ->  (
( { <. 1 ,  1 >. }  u.  c ) `  y
)  =  ( c `
 y ) )
378376, 377eqeq12d 2418 . . . . . . . . . 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 ) ) )
379378ralbidva 2682 . . . . . . . . 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 ) ) )
380103adantr 452 . . . . . . . . . 10  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.  C ) )  -> 
( { 1 }  u.  ( 2 ... ( N  +  1 ) ) )  =  ( 1 ... ( N  +  1 ) ) )
381380raleqdv 2870 . . . . . . . . 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
) ) )
382374, 379, 3813bitr3rd 276 . . . . . . . 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 ) ) )
38366adantrr 698 . . . . . . . . 9  |-  ( (
ph  /\  ( b  e.  B  /\  c  e.