Metamath Proof Explorer

Theorem subfacp1lem5

Description: Lemma for subfacp1 . In subfacp1lem6 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( f1 ) ) = 1 . In this lemma, we show that the subset of all N + 1 derangements with ( f( f1 ) ) =/= 1 for fixed M = ( f1 ) 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 ( f1 ) = 1 and ( fx ) =/= 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)

Ref Expression
Hypotheses 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 subfacp1lem5 
|- ( ph -> ( # ` B ) = ( S ` N ) )

Proof

Step Hyp Ref Expression
1 derang.d 
 |-  D = ( x e. Fin |-> ( # ` { f | ( f : x -1-1-onto-> x /\ A. y e. x ( f ` y ) =/= y ) } ) )
2 subfac.n 
 |-  S = ( n e. NN0 |-> ( D ` ( 1 ... n ) ) )
3 subfacp1lem.a 
 |-  A = { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) }
4 subfacp1lem1.n 
 |-  ( ph -> N e. NN )
5 subfacp1lem1.m 
 |-  ( ph -> M e. ( 2 ... ( N + 1 ) ) )
6 subfacp1lem1.x 
 |-  M e. _V
7 subfacp1lem1.k 
 |-  K = ( ( 2 ... ( N + 1 ) ) \ { M } )
8 subfacp1lem5.b 
 |-  B = { g e. A | ( ( g ` 1 ) = M /\ ( g ` M ) =/= 1 ) }
9 subfacp1lem5.f 
 |-  F = ( ( _I |` K ) u. { <. 1 , M >. , <. M , 1 >. } )
10 subfacp1lem5.c 
 |-  C = { f | ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) }
11 fzfi 
 |-  ( 1 ... ( N + 1 ) ) e. Fin
12 deranglem 
 |-  ( ( 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 )
13 11 12 ax-mp 
 |-  { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) } e. Fin
14 3 13 eqeltri 
 |-  A e. Fin
15 8 ssrab3 
 |-  B C_ A
16 ssfi 
 |-  ( ( A e. Fin /\ B C_ A ) -> B e. Fin )
17 14 15 16 mp2an 
 |-  B e. Fin
18 17 elexi 
 |-  B e. _V
19 18 a1i 
 |-  ( ph -> B e. _V )
20 eqid 
 |-  ( b e. B |-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ) = ( b e. B |-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) )
21 f1oi 
 |-  ( _I |` K ) : K -1-1-onto-> K
22 21 a1i 
 |-  ( ph -> ( _I |` K ) : K -1-1-onto-> K )
23 1 2 3 4 5 6 7 9 22 subfacp1lem2a 
 |-  ( ph -> ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( F ` 1 ) = M /\ ( F ` M ) = 1 ) )
24 23 simp1d 
 |-  ( ph -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
25 simpr 
 |-  ( ( ph /\ b e. B ) -> b e. B )
26 fveq1 
 |-  ( g = b -> ( g ` 1 ) = ( b ` 1 ) )
27 26 eqeq1d 
 |-  ( g = b -> ( ( g ` 1 ) = M <-> ( b ` 1 ) = M ) )
28 fveq1 
 |-  ( g = b -> ( g ` M ) = ( b ` M ) )
29 28 neeq1d 
 |-  ( g = b -> ( ( g ` M ) =/= 1 <-> ( b ` M ) =/= 1 ) )
30 27 29 anbi12d 
 |-  ( g = b -> ( ( ( g ` 1 ) = M /\ ( g ` M ) =/= 1 ) <-> ( ( b ` 1 ) = M /\ ( b ` M ) =/= 1 ) ) )
31 30 8 elrab2 
 |-  ( b e. B <-> ( b e. A /\ ( ( b ` 1 ) = M /\ ( b ` M ) =/= 1 ) ) )
32 25 31 sylib 
 |-  ( ( ph /\ b e. B ) -> ( b e. A /\ ( ( b ` 1 ) = M /\ ( b ` M ) =/= 1 ) ) )
33 32 simpld 
 |-  ( ( ph /\ b e. B ) -> b e. A )
34 vex 
 |-  b e. _V
35 f1oeq1 
 |-  ( f = b -> ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) <-> b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
36 fveq1 
 |-  ( f = b -> ( f ` y ) = ( b ` y ) )
37 36 neeq1d 
 |-  ( f = b -> ( ( f ` y ) =/= y <-> ( b ` y ) =/= y ) )
38 37 ralbidv 
 |-  ( f = b -> ( A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y <-> A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y ) )
39 35 38 anbi12d 
 |-  ( 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 ) ) )
40 34 39 3 elab2 
 |-  ( b e. A <-> ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y ) )
41 33 40 sylib 
 |-  ( ( ph /\ b e. B ) -> ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y ) )
42 41 simpld 
 |-  ( ( ph /\ b e. B ) -> b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
43 f1oco 
 |-  ( ( 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 ) ) )
44 24 42 43 syl2an2r 
 |-  ( ( ph /\ b e. B ) -> ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
45 f1of1 
 |-  ( ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) )
46 df-f1 
 |-  ( ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) <-> ( ( F o. b ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ Fun `' ( F o. b ) ) )
47 46 simprbi 
 |-  ( ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) -> Fun `' ( F o. b ) )
48 44 45 47 3syl 
 |-  ( ( ph /\ b e. B ) -> Fun `' ( F o. b ) )
49 f1ofn 
 |-  ( ( F o. b ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( F o. b ) Fn ( 1 ... ( N + 1 ) ) )
50 fnresdm 
 |-  ( ( F o. b ) Fn ( 1 ... ( N + 1 ) ) -> ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) = ( F o. b ) )
51 f1oeq1 
 |-  ( ( ( 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 ) ) ) )
52 44 49 50 51 4syl 
 |-  ( ( 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 ) ) ) )
53 44 52 mpbird 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
54 f1ofo 
 |-  ( ( ( 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 ) ) )
55 53 54 syl 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -onto-> ( 1 ... ( N + 1 ) ) )
56 1ex 
 |-  1 e. _V
57 56 56 f1osn 
 |-  { <. 1 , 1 >. } : { 1 } -1-1-onto-> { 1 }
58 44 49 syl 
 |-  ( ( ph /\ b e. B ) -> ( F o. b ) Fn ( 1 ... ( N + 1 ) ) )
59 4 peano2nnd 
 |-  ( ph -> ( N + 1 ) e. NN )
60 nnuz 
 |-  NN = ( ZZ>= ` 1 )
61 59 60 eleqtrdi 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` 1 ) )
62 eluzfz1 
 |-  ( ( N + 1 ) e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... ( N + 1 ) ) )
63 61 62 syl 
 |-  ( ph -> 1 e. ( 1 ... ( N + 1 ) ) )
64 63 adantr 
 |-  ( ( ph /\ b e. B ) -> 1 e. ( 1 ... ( N + 1 ) ) )
65 fnressn 
 |-  ( ( ( F o. b ) Fn ( 1 ... ( N + 1 ) ) /\ 1 e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. b ) |` { 1 } ) = { <. 1 , ( ( F o. b ) ` 1 ) >. } )
66 58 64 65 syl2anc 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` { 1 } ) = { <. 1 , ( ( F o. b ) ` 1 ) >. } )
67 f1of 
 |-  ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
68 42 67 syl 
 |-  ( ( ph /\ b e. B ) -> b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
69 68 64 fvco3d 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) ` 1 ) = ( F ` ( b ` 1 ) ) )
70 32 simprd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) = M /\ ( b ` M ) =/= 1 ) )
71 70 simpld 
 |-  ( ( ph /\ b e. B ) -> ( b ` 1 ) = M )
72 71 fveq2d 
 |-  ( ( ph /\ b e. B ) -> ( F ` ( b ` 1 ) ) = ( F ` M ) )
73 23 simp3d 
 |-  ( ph -> ( F ` M ) = 1 )
74 73 adantr 
 |-  ( ( ph /\ b e. B ) -> ( F ` M ) = 1 )
75 69 72 74 3eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) ` 1 ) = 1 )
76 75 opeq2d 
 |-  ( ( ph /\ b e. B ) -> <. 1 , ( ( F o. b ) ` 1 ) >. = <. 1 , 1 >. )
77 76 sneqd 
 |-  ( ( ph /\ b e. B ) -> { <. 1 , ( ( F o. b ) ` 1 ) >. } = { <. 1 , 1 >. } )
78 66 77 eqtrd 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` { 1 } ) = { <. 1 , 1 >. } )
79 f1oeq1 
 |-  ( ( ( F o. b ) |` { 1 } ) = { <. 1 , 1 >. } -> ( ( ( F o. b ) |` { 1 } ) : { 1 } -1-1-onto-> { 1 } <-> { <. 1 , 1 >. } : { 1 } -1-1-onto-> { 1 } ) )
80 78 79 syl 
 |-  ( ( ph /\ b e. B ) -> ( ( ( F o. b ) |` { 1 } ) : { 1 } -1-1-onto-> { 1 } <-> { <. 1 , 1 >. } : { 1 } -1-1-onto-> { 1 } ) )
81 57 80 mpbiri 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` { 1 } ) : { 1 } -1-1-onto-> { 1 } )
82 f1ofo 
 |-  ( ( ( F o. b ) |` { 1 } ) : { 1 } -1-1-onto-> { 1 } -> ( ( F o. b ) |` { 1 } ) : { 1 } -onto-> { 1 } )
83 81 82 syl 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` { 1 } ) : { 1 } -onto-> { 1 } )
84 resdif 
 |-  ( ( 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 } ) )
85 48 55 83 84 syl3anc 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) )
86 fzsplit 
 |-  ( 1 e. ( 1 ... ( N + 1 ) ) -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... ( N + 1 ) ) ) )
87 63 86 syl 
 |-  ( ph -> ( 1 ... ( N + 1 ) ) = ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... ( N + 1 ) ) ) )
88 1z 
 |-  1 e. ZZ
89 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
90 88 89 ax-mp 
 |-  ( 1 ... 1 ) = { 1 }
91 1p1e2 
 |-  ( 1 + 1 ) = 2
92 91 oveq1i 
 |-  ( ( 1 + 1 ) ... ( N + 1 ) ) = ( 2 ... ( N + 1 ) )
93 90 92 uneq12i 
 |-  ( ( 1 ... 1 ) u. ( ( 1 + 1 ) ... ( N + 1 ) ) ) = ( { 1 } u. ( 2 ... ( N + 1 ) ) )
94 87 93 eqtr2di 
 |-  ( ph -> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) )
95 63 snssd 
 |-  ( ph -> { 1 } C_ ( 1 ... ( N + 1 ) ) )
96 incom 
 |-  ( { 1 } i^i ( 2 ... ( N + 1 ) ) ) = ( ( 2 ... ( N + 1 ) ) i^i { 1 } )
97 1lt2 
 |-  1 < 2
98 1re 
 |-  1 e. RR
99 2re 
 |-  2 e. RR
100 98 99 ltnlei 
 |-  ( 1 < 2 <-> -. 2 <_ 1 )
101 97 100 mpbi 
 |-  -. 2 <_ 1
102 elfzle1 
 |-  ( 1 e. ( 2 ... ( N + 1 ) ) -> 2 <_ 1 )
103 101 102 mto 
 |-  -. 1 e. ( 2 ... ( N + 1 ) )
104 disjsn 
 |-  ( ( ( 2 ... ( N + 1 ) ) i^i { 1 } ) = (/) <-> -. 1 e. ( 2 ... ( N + 1 ) ) )
105 103 104 mpbir 
 |-  ( ( 2 ... ( N + 1 ) ) i^i { 1 } ) = (/)
106 96 105 eqtri 
 |-  ( { 1 } i^i ( 2 ... ( N + 1 ) ) ) = (/)
107 uneqdifeq 
 |-  ( ( { 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 ) ) ) )
108 95 106 107 sylancl 
 |-  ( ph -> ( ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) <-> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) ) )
109 94 108 mpbid 
 |-  ( ph -> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) )
110 109 adantr 
 |-  ( ( ph /\ b e. B ) -> ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) )
111 reseq2 
 |-  ( ( ( 1 ... ( N + 1 ) ) \ { 1 } ) = ( 2 ... ( N + 1 ) ) -> ( ( F o. b ) |` ( ( 1 ... ( N + 1 ) ) \ { 1 } ) ) = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) )
112 f1oeq1 
 |-  ( ( ( 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 } ) ) )
113 111 112 syl 
 |-  ( ( ( 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 } ) ) )
114 f1oeq2 
 |-  ( ( ( 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 } ) ) )
115 f1oeq3 
 |-  ( ( ( 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 ) ) ) )
116 113 114 115 3bitrd 
 |-  ( ( ( 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 ) ) ) )
117 110 116 syl 
 |-  ( ( 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 ) ) ) )
118 85 117 mpbid 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) )
119 68 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
120 fzp1ss 
 |-  ( 1 e. ZZ -> ( ( 1 + 1 ) ... ( N + 1 ) ) C_ ( 1 ... ( N + 1 ) ) )
121 88 120 ax-mp 
 |-  ( ( 1 + 1 ) ... ( N + 1 ) ) C_ ( 1 ... ( N + 1 ) )
122 92 121 eqsstrri 
 |-  ( 2 ... ( N + 1 ) ) C_ ( 1 ... ( N + 1 ) )
123 simpr 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> y e. ( 2 ... ( N + 1 ) ) )
124 122 123 sseldi 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> y e. ( 1 ... ( N + 1 ) ) )
125 119 124 fvco3d 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( F o. b ) ` y ) = ( F ` ( b ` y ) ) )
126 1 2 3 4 5 6 7 8 9 subfacp1lem4 
 |-  ( ph -> `' F = F )
127 126 fveq1d 
 |-  ( ph -> ( `' F ` y ) = ( F ` y ) )
128 127 ad2antrr 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( `' F ` y ) = ( F ` y ) )
129 70 simprd 
 |-  ( ( ph /\ b e. B ) -> ( b ` M ) =/= 1 )
130 129 74 neeqtrrd 
 |-  ( ( ph /\ b e. B ) -> ( b ` M ) =/= ( F ` M ) )
131 130 adantr 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( b ` M ) =/= ( F ` M ) )
132 fveq2 
 |-  ( y = M -> ( b ` y ) = ( b ` M ) )
133 fveq2 
 |-  ( y = M -> ( F ` y ) = ( F ` M ) )
134 132 133 neeq12d 
 |-  ( y = M -> ( ( b ` y ) =/= ( F ` y ) <-> ( b ` M ) =/= ( F ` M ) ) )
135 131 134 syl5ibrcom 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( y = M -> ( b ` y ) =/= ( F ` y ) ) )
136 122 sseli 
 |-  ( y e. ( 2 ... ( N + 1 ) ) -> y e. ( 1 ... ( N + 1 ) ) )
137 41 simprd 
 |-  ( ( ph /\ b e. B ) -> A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y )
138 137 r19.21bi 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( b ` y ) =/= y )
139 136 138 sylan2 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( b ` y ) =/= y )
140 139 adantrr 
 |-  ( ( ( ph /\ b e. B ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( b ` y ) =/= y )
141 7 eleq2i 
 |-  ( y e. K <-> y e. ( ( 2 ... ( N + 1 ) ) \ { M } ) )
142 eldifsn 
 |-  ( y e. ( ( 2 ... ( N + 1 ) ) \ { M } ) <-> ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) )
143 141 142 bitri 
 |-  ( y e. K <-> ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) )
144 1 2 3 4 5 6 7 9 22 subfacp1lem2b 
 |-  ( ( ph /\ y e. K ) -> ( F ` y ) = ( ( _I |` K ) ` y ) )
145 fvresi 
 |-  ( y e. K -> ( ( _I |` K ) ` y ) = y )
146 145 adantl 
 |-  ( ( ph /\ y e. K ) -> ( ( _I |` K ) ` y ) = y )
147 144 146 eqtrd 
 |-  ( ( ph /\ y e. K ) -> ( F ` y ) = y )
148 143 147 sylan2br 
 |-  ( ( ph /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( F ` y ) = y )
149 148 adantlr 
 |-  ( ( ( ph /\ b e. B ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( F ` y ) = y )
150 140 149 neeqtrrd 
 |-  ( ( ( ph /\ b e. B ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( b ` y ) =/= ( F ` y ) )
151 150 expr 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( y =/= M -> ( b ` y ) =/= ( F ` y ) ) )
152 135 151 pm2.61dne 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( b ` y ) =/= ( F ` y ) )
153 152 necomd 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( F ` y ) =/= ( b ` y ) )
154 128 153 eqnetrd 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( `' F ` y ) =/= ( b ` y ) )
155 24 adantr 
 |-  ( ( ph /\ b e. B ) -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
156 ffvelrn 
 |-  ( ( b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( b ` y ) e. ( 1 ... ( N + 1 ) ) )
157 68 136 156 syl2an 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( b ` y ) e. ( 1 ... ( N + 1 ) ) )
158 f1ocnvfv 
 |-  ( ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( b ` y ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( F ` ( b ` y ) ) = y -> ( `' F ` y ) = ( b ` y ) ) )
159 155 157 158 syl2an2r 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( F ` ( b ` y ) ) = y -> ( `' F ` y ) = ( b ` y ) ) )
160 159 necon3d 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( `' F ` y ) =/= ( b ` y ) -> ( F ` ( b ` y ) ) =/= y ) )
161 154 160 mpd 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( F ` ( b ` y ) ) =/= y )
162 125 161 eqnetrd 
 |-  ( ( ( ph /\ b e. B ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( F o. b ) ` y ) =/= y )
163 162 ralrimiva 
 |-  ( ( ph /\ b e. B ) -> A. y e. ( 2 ... ( N + 1 ) ) ( ( F o. b ) ` y ) =/= y )
164 f1of 
 |-  ( ( _I |` K ) : K -1-1-onto-> K -> ( _I |` K ) : K --> K )
165 21 164 ax-mp 
 |-  ( _I |` K ) : K --> K
166 fzfi 
 |-  ( 2 ... ( N + 1 ) ) e. Fin
167 difexg 
 |-  ( ( 2 ... ( N + 1 ) ) e. Fin -> ( ( 2 ... ( N + 1 ) ) \ { M } ) e. _V )
168 166 167 ax-mp 
 |-  ( ( 2 ... ( N + 1 ) ) \ { M } ) e. _V
169 7 168 eqeltri 
 |-  K e. _V
170 fex 
 |-  ( ( ( _I |` K ) : K --> K /\ K e. _V ) -> ( _I |` K ) e. _V )
171 165 169 170 mp2an 
 |-  ( _I |` K ) e. _V
172 prex 
 |-  { <. 1 , M >. , <. M , 1 >. } e. _V
173 171 172 unex 
 |-  ( ( _I |` K ) u. { <. 1 , M >. , <. M , 1 >. } ) e. _V
174 9 173 eqeltri 
 |-  F e. _V
175 174 34 coex 
 |-  ( F o. b ) e. _V
176 175 resex 
 |-  ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) e. _V
177 f1oeq1 
 |-  ( 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 ) ) ) )
178 fveq1 
 |-  ( f = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) -> ( f ` y ) = ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) )
179 fvres 
 |-  ( y e. ( 2 ... ( N + 1 ) ) -> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) = ( ( F o. b ) ` y ) )
180 178 179 sylan9eq 
 |-  ( ( f = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( f ` y ) = ( ( F o. b ) ` y ) )
181 180 neeq1d 
 |-  ( ( f = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( f ` y ) =/= y <-> ( ( F o. b ) ` y ) =/= y ) )
182 181 ralbidva 
 |-  ( 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 ) )
183 177 182 anbi12d 
 |-  ( 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 ) ) )
184 176 183 10 elab2 
 |-  ( ( ( 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 ) )
185 118 163 184 sylanbrc 
 |-  ( ( ph /\ b e. B ) -> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) e. C )
186 simpr 
 |-  ( ( ph /\ c e. C ) -> c e. C )
187 vex 
 |-  c e. _V
188 f1oeq1 
 |-  ( f = c -> ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) <-> c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) ) )
189 fveq1 
 |-  ( f = c -> ( f ` y ) = ( c ` y ) )
190 189 neeq1d 
 |-  ( f = c -> ( ( f ` y ) =/= y <-> ( c ` y ) =/= y ) )
191 190 ralbidv 
 |-  ( f = c -> ( A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y <-> A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y ) )
192 188 191 anbi12d 
 |-  ( 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 ) ) )
193 187 192 10 elab2 
 |-  ( c e. C <-> ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y ) )
194 186 193 sylib 
 |-  ( ( ph /\ c e. C ) -> ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y ) )
195 194 simpld 
 |-  ( ( ph /\ c e. C ) -> c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) )
196 f1oun 
 |-  ( ( ( { <. 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 ) ) ) )
197 106 106 196 mpanr12 
 |-  ( ( { <. 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 ) ) ) )
198 57 195 197 sylancr 
 |-  ( ( ph /\ c e. C ) -> ( { <. 1 , 1 >. } u. c ) : ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) )
199 f1oeq2 
 |-  ( ( { 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 ) ) ) ) )
200 f1oeq3 
 |-  ( ( { 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 ) ) ) )
201 199 200 bitrd 
 |-  ( ( { 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 ) ) ) )
202 94 201 syl 
 |-  ( 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 ) ) ) )
203 202 biimpa 
 |-  ( ( 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 ) ) )
204 198 203 syldan 
 |-  ( ( ph /\ c e. C ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
205 f1oco 
 |-  ( ( 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 ) ) )
206 24 204 205 syl2an2r 
 |-  ( ( ph /\ c e. C ) -> ( F o. ( { <. 1 , 1 >. } u. c ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
207 f1of 
 |-  ( ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
208 204 207 syl 
 |-  ( ( ph /\ c e. C ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
209 fvco3 
 |-  ( ( ( { <. 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 ) ) )
210 208 209 sylan 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) = ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
211 127 ad2antrr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( `' F ` y ) = ( F ` y ) )
212 simpr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> y e. ( 1 ... ( N + 1 ) ) )
213 94 ad2antrr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) )
214 212 213 eleqtrrd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> y e. ( { 1 } u. ( 2 ... ( N + 1 ) ) ) )
215 elun 
 |-  ( y e. ( { 1 } u. ( 2 ... ( N + 1 ) ) ) <-> ( y e. { 1 } \/ y e. ( 2 ... ( N + 1 ) ) ) )
216 214 215 sylib 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( y e. { 1 } \/ y e. ( 2 ... ( N + 1 ) ) ) )
217 nelne2 
 |-  ( ( M e. ( 2 ... ( N + 1 ) ) /\ -. 1 e. ( 2 ... ( N + 1 ) ) ) -> M =/= 1 )
218 5 103 217 sylancl 
 |-  ( ph -> M =/= 1 )
219 218 adantr 
 |-  ( ( ph /\ c e. C ) -> M =/= 1 )
220 23 simp2d 
 |-  ( ph -> ( F ` 1 ) = M )
221 220 adantr 
 |-  ( ( ph /\ c e. C ) -> ( F ` 1 ) = M )
222 f1ofun 
 |-  ( ( { <. 1 , 1 >. } u. c ) : ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -1-1-onto-> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) -> Fun ( { <. 1 , 1 >. } u. c ) )
223 198 222 syl 
 |-  ( ( ph /\ c e. C ) -> Fun ( { <. 1 , 1 >. } u. c ) )
224 ssun1 
 |-  { <. 1 , 1 >. } C_ ( { <. 1 , 1 >. } u. c )
225 56 snid 
 |-  1 e. { 1 }
226 56 dmsnop 
 |-  dom { <. 1 , 1 >. } = { 1 }
227 225 226 eleqtrri 
 |-  1 e. dom { <. 1 , 1 >. }
228 funssfv 
 |-  ( ( 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 ) )
229 224 227 228 mp3an23 
 |-  ( Fun ( { <. 1 , 1 >. } u. c ) -> ( ( { <. 1 , 1 >. } u. c ) ` 1 ) = ( { <. 1 , 1 >. } ` 1 ) )
230 223 229 syl 
 |-  ( ( ph /\ c e. C ) -> ( ( { <. 1 , 1 >. } u. c ) ` 1 ) = ( { <. 1 , 1 >. } ` 1 ) )
231 56 56 fvsn 
 |-  ( { <. 1 , 1 >. } ` 1 ) = 1
232 230 231 eqtrdi 
 |-  ( ( ph /\ c e. C ) -> ( ( { <. 1 , 1 >. } u. c ) ` 1 ) = 1 )
233 219 221 232 3netr4d 
 |-  ( ( ph /\ c e. C ) -> ( F ` 1 ) =/= ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
234 elsni 
 |-  ( y e. { 1 } -> y = 1 )
235 234 fveq2d 
 |-  ( y e. { 1 } -> ( F ` y ) = ( F ` 1 ) )
236 234 fveq2d 
 |-  ( y e. { 1 } -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
237 235 236 neeq12d 
 |-  ( y e. { 1 } -> ( ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> ( F ` 1 ) =/= ( ( { <. 1 , 1 >. } u. c ) ` 1 ) ) )
238 233 237 syl5ibrcom 
 |-  ( ( ph /\ c e. C ) -> ( y e. { 1 } -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
239 238 imp 
 |-  ( ( ( ph /\ c e. C ) /\ y e. { 1 } ) -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
240 223 adantr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> Fun ( { <. 1 , 1 >. } u. c ) )
241 ssun2 
 |-  c C_ ( { <. 1 , 1 >. } u. c )
242 241 a1i 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> c C_ ( { <. 1 , 1 >. } u. c ) )
243 f1odm 
 |-  ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) -> dom c = ( 2 ... ( N + 1 ) ) )
244 195 243 syl 
 |-  ( ( ph /\ c e. C ) -> dom c = ( 2 ... ( N + 1 ) ) )
245 244 eleq2d 
 |-  ( ( ph /\ c e. C ) -> ( y e. dom c <-> y e. ( 2 ... ( N + 1 ) ) ) )
246 245 biimpar 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> y e. dom c )
247 funssfv 
 |-  ( ( Fun ( { <. 1 , 1 >. } u. c ) /\ c C_ ( { <. 1 , 1 >. } u. c ) /\ y e. dom c ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( c ` y ) )
248 240 242 246 247 syl3anc 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( c ` y ) )
249 f1of 
 |-  ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) -> c : ( 2 ... ( N + 1 ) ) --> ( 2 ... ( N + 1 ) ) )
250 195 249 syl 
 |-  ( ( ph /\ c e. C ) -> c : ( 2 ... ( N + 1 ) ) --> ( 2 ... ( N + 1 ) ) )
251 5 adantr 
 |-  ( ( ph /\ c e. C ) -> M e. ( 2 ... ( N + 1 ) ) )
252 250 251 ffvelrnd 
 |-  ( ( ph /\ c e. C ) -> ( c ` M ) e. ( 2 ... ( N + 1 ) ) )
253 nelne2 
 |-  ( ( ( c ` M ) e. ( 2 ... ( N + 1 ) ) /\ -. 1 e. ( 2 ... ( N + 1 ) ) ) -> ( c ` M ) =/= 1 )
254 252 103 253 sylancl 
 |-  ( ( ph /\ c e. C ) -> ( c ` M ) =/= 1 )
255 254 adantr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( c ` M ) =/= 1 )
256 73 ad2antrr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( F ` M ) = 1 )
257 255 256 neeqtrrd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( c ` M ) =/= ( F ` M ) )
258 fveq2 
 |-  ( y = M -> ( c ` y ) = ( c ` M ) )
259 258 133 neeq12d 
 |-  ( y = M -> ( ( c ` y ) =/= ( F ` y ) <-> ( c ` M ) =/= ( F ` M ) ) )
260 257 259 syl5ibrcom 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( y = M -> ( c ` y ) =/= ( F ` y ) ) )
261 194 simprd 
 |-  ( ( ph /\ c e. C ) -> A. y e. ( 2 ... ( N + 1 ) ) ( c ` y ) =/= y )
262 261 r19.21bi 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( c ` y ) =/= y )
263 262 adantrr 
 |-  ( ( ( ph /\ c e. C ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( c ` y ) =/= y )
264 148 adantlr 
 |-  ( ( ( ph /\ c e. C ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( F ` y ) = y )
265 263 264 neeqtrrd 
 |-  ( ( ( ph /\ c e. C ) /\ ( y e. ( 2 ... ( N + 1 ) ) /\ y =/= M ) ) -> ( c ` y ) =/= ( F ` y ) )
266 265 expr 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( y =/= M -> ( c ` y ) =/= ( F ` y ) ) )
267 260 266 pm2.61dne 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( c ` y ) =/= ( F ` y ) )
268 248 267 eqnetrd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) =/= ( F ` y ) )
269 268 necomd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
270 239 269 jaodan 
 |-  ( ( ( ph /\ c e. C ) /\ ( y e. { 1 } \/ y e. ( 2 ... ( N + 1 ) ) ) ) -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
271 216 270 syldan 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
272 211 271 eqnetrd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( `' F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) )
273 24 adantr 
 |-  ( ( ph /\ c e. C ) -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
274 208 ffvelrnda 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) e. ( 1 ... ( N + 1 ) ) )
275 f1ocnvfv 
 |-  ( ( 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 ) ) )
276 273 274 275 syl2an2r 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) = y -> ( `' F ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
277 276 necon3d 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( `' F ` y ) =/= ( ( { <. 1 , 1 >. } u. c ) ` y ) -> ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) =/= y ) )
278 272 277 mpd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( F ` ( ( { <. 1 , 1 >. } u. c ) ` y ) ) =/= y )
279 210 278 eqnetrd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. ( 1 ... ( N + 1 ) ) ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) =/= y )
280 279 ralrimiva 
 |-  ( ( ph /\ c e. C ) -> A. y e. ( 1 ... ( N + 1 ) ) ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) =/= y )
281 snex 
 |-  { <. 1 , 1 >. } e. _V
282 281 187 unex 
 |-  ( { <. 1 , 1 >. } u. c ) e. _V
283 174 282 coex 
 |-  ( F o. ( { <. 1 , 1 >. } u. c ) ) e. _V
284 f1oeq1 
 |-  ( 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 ) ) ) )
285 fveq1 
 |-  ( f = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( f ` y ) = ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) )
286 285 neeq1d 
 |-  ( f = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( ( f ` y ) =/= y <-> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` y ) =/= y ) )
287 286 ralbidv 
 |-  ( 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 ) )
288 284 287 anbi12d 
 |-  ( 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 ) ) )
289 283 288 3 elab2 
 |-  ( ( 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 ) )
290 206 280 289 sylanbrc 
 |-  ( ( ph /\ c e. C ) -> ( F o. ( { <. 1 , 1 >. } u. c ) ) e. A )
291 63 adantr 
 |-  ( ( ph /\ c e. C ) -> 1 e. ( 1 ... ( N + 1 ) ) )
292 208 291 fvco3d 
 |-  ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = ( F ` ( ( { <. 1 , 1 >. } u. c ) ` 1 ) ) )
293 232 fveq2d 
 |-  ( ( ph /\ c e. C ) -> ( F ` ( ( { <. 1 , 1 >. } u. c ) ` 1 ) ) = ( F ` 1 ) )
294 292 293 221 3eqtrd 
 |-  ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = M )
295 122 5 sseldi 
 |-  ( ph -> M e. ( 1 ... ( N + 1 ) ) )
296 295 adantr 
 |-  ( ( ph /\ c e. C ) -> M e. ( 1 ... ( N + 1 ) ) )
297 208 296 fvco3d 
 |-  ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) = ( F ` ( ( { <. 1 , 1 >. } u. c ) ` M ) ) )
298 241 a1i 
 |-  ( ( ph /\ c e. C ) -> c C_ ( { <. 1 , 1 >. } u. c ) )
299 251 244 eleqtrrd 
 |-  ( ( ph /\ c e. C ) -> M e. dom c )
300 funssfv 
 |-  ( ( Fun ( { <. 1 , 1 >. } u. c ) /\ c C_ ( { <. 1 , 1 >. } u. c ) /\ M e. dom c ) -> ( ( { <. 1 , 1 >. } u. c ) ` M ) = ( c ` M ) )
301 223 298 299 300 syl3anc 
 |-  ( ( ph /\ c e. C ) -> ( ( { <. 1 , 1 >. } u. c ) ` M ) = ( c ` M ) )
302 301 fveq2d 
 |-  ( ( ph /\ c e. C ) -> ( F ` ( ( { <. 1 , 1 >. } u. c ) ` M ) ) = ( F ` ( c ` M ) ) )
303 297 302 eqtrd 
 |-  ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) = ( F ` ( c ` M ) ) )
304 126 fveq1d 
 |-  ( ph -> ( `' F ` 1 ) = ( F ` 1 ) )
305 304 220 eqtrd 
 |-  ( ph -> ( `' F ` 1 ) = M )
306 305 adantr 
 |-  ( ( ph /\ c e. C ) -> ( `' F ` 1 ) = M )
307 id 
 |-  ( y = M -> y = M )
308 258 307 neeq12d 
 |-  ( y = M -> ( ( c ` y ) =/= y <-> ( c ` M ) =/= M ) )
309 308 261 251 rspcdva 
 |-  ( ( ph /\ c e. C ) -> ( c ` M ) =/= M )
310 309 necomd 
 |-  ( ( ph /\ c e. C ) -> M =/= ( c ` M ) )
311 306 310 eqnetrd 
 |-  ( ( ph /\ c e. C ) -> ( `' F ` 1 ) =/= ( c ` M ) )
312 122 252 sseldi 
 |-  ( ( ph /\ c e. C ) -> ( c ` M ) e. ( 1 ... ( N + 1 ) ) )
313 f1ocnvfv 
 |-  ( ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( c ` M ) e. ( 1 ... ( N + 1 ) ) ) -> ( ( F ` ( c ` M ) ) = 1 -> ( `' F ` 1 ) = ( c ` M ) ) )
314 24 312 313 syl2an2r 
 |-  ( ( ph /\ c e. C ) -> ( ( F ` ( c ` M ) ) = 1 -> ( `' F ` 1 ) = ( c ` M ) ) )
315 314 necon3d 
 |-  ( ( ph /\ c e. C ) -> ( ( `' F ` 1 ) =/= ( c ` M ) -> ( F ` ( c ` M ) ) =/= 1 ) )
316 311 315 mpd 
 |-  ( ( ph /\ c e. C ) -> ( F ` ( c ` M ) ) =/= 1 )
317 303 316 eqnetrd 
 |-  ( ( ph /\ c e. C ) -> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) =/= 1 )
318 294 317 jca 
 |-  ( ( ph /\ c e. C ) -> ( ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = M /\ ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) =/= 1 ) )
319 fveq1 
 |-  ( g = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( g ` 1 ) = ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) )
320 319 eqeq1d 
 |-  ( g = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( ( g ` 1 ) = M <-> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` 1 ) = M ) )
321 fveq1 
 |-  ( g = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( g ` M ) = ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) )
322 321 neeq1d 
 |-  ( g = ( F o. ( { <. 1 , 1 >. } u. c ) ) -> ( ( g ` M ) =/= 1 <-> ( ( F o. ( { <. 1 , 1 >. } u. c ) ) ` M ) =/= 1 ) )
323 320 322 anbi12d 
 |-  ( 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 ) ) )
324 323 8 elrab2 
 |-  ( ( 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 ) ) )
325 290 318 324 sylanbrc 
 |-  ( ( ph /\ c e. C ) -> ( F o. ( { <. 1 , 1 >. } u. c ) ) e. B )
326 24 adantr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
327 f1of1 
 |-  ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> F : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) )
328 326 327 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> F : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) )
329 f1of 
 |-  ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> F : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
330 326 329 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> F : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
331 68 adantrr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
332 330 331 fcod 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( F o. b ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
333 208 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) )
334 cocan1 
 |-  ( ( 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 ) ) )
335 328 332 333 334 syl3anc 
 |-  ( ( 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 ) ) )
336 coass 
 |-  ( ( F o. F ) o. b ) = ( F o. ( F o. b ) )
337 126 coeq1d 
 |-  ( ph -> ( `' F o. F ) = ( F o. F ) )
338 f1ococnv1 
 |-  ( F : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( `' F o. F ) = ( _I |` ( 1 ... ( N + 1 ) ) ) )
339 24 338 syl 
 |-  ( ph -> ( `' F o. F ) = ( _I |` ( 1 ... ( N + 1 ) ) ) )
340 337 339 eqtr3d 
 |-  ( ph -> ( F o. F ) = ( _I |` ( 1 ... ( N + 1 ) ) ) )
341 340 adantr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( F o. F ) = ( _I |` ( 1 ... ( N + 1 ) ) ) )
342 341 coeq1d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. F ) o. b ) = ( ( _I |` ( 1 ... ( N + 1 ) ) ) o. b ) )
343 fcoi2 
 |-  ( b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) -> ( ( _I |` ( 1 ... ( N + 1 ) ) ) o. b ) = b )
344 331 343 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( _I |` ( 1 ... ( N + 1 ) ) ) o. b ) = b )
345 342 344 eqtrd 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. F ) o. b ) = b )
346 336 345 eqtr3id 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( F o. ( F o. b ) ) = b )
347 346 eqeq1d 
 |-  ( ( 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 ) ) ) )
348 75 adantrr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) ` 1 ) = 1 )
349 232 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` 1 ) = 1 )
350 348 349 eqtr4d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) ` 1 ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
351 fveq2 
 |-  ( y = 1 -> ( ( F o. b ) ` y ) = ( ( F o. b ) ` 1 ) )
352 fveq2 
 |-  ( y = 1 -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
353 351 352 eqeq12d 
 |-  ( y = 1 -> ( ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> ( ( F o. b ) ` 1 ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) ) )
354 56 353 ralsn 
 |-  ( A. y e. { 1 } ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) <-> ( ( F o. b ) ` 1 ) = ( ( { <. 1 , 1 >. } u. c ) ` 1 ) )
355 350 354 sylibr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> A. y e. { 1 } ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) )
356 355 biantrurd 
 |-  ( ( 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 ) ) ) )
357 ralunb 
 |-  ( 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 ) ) )
358 356 357 bitr4di 
 |-  ( ( 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 ) ) )
359 179 adantl 
 |-  ( ( ( ph /\ ( b e. B /\ c e. C ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) = ( ( F o. b ) ` y ) )
360 359 eqcomd 
 |-  ( ( ( ph /\ ( b e. B /\ c e. C ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( F o. b ) ` y ) = ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) )
361 248 adantlrl 
 |-  ( ( ( ph /\ ( b e. B /\ c e. C ) ) /\ y e. ( 2 ... ( N + 1 ) ) ) -> ( ( { <. 1 , 1 >. } u. c ) ` y ) = ( c ` y ) )
362 360 361 eqeq12d 
 |-  ( ( ( 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 ) ) )
363 362 ralbidva 
 |-  ( ( 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 ) ) )
364 94 adantr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( { 1 } u. ( 2 ... ( N + 1 ) ) ) = ( 1 ... ( N + 1 ) ) )
365 364 raleqdv 
 |-  ( ( 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 ) ) )
366 358 363 365 3bitr3rd 
 |-  ( ( 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 ) ) )
367 58 adantrr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( F o. b ) Fn ( 1 ... ( N + 1 ) ) )
368 204 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
369 f1ofn 
 |-  ( ( { <. 1 , 1 >. } u. c ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( { <. 1 , 1 >. } u. c ) Fn ( 1 ... ( N + 1 ) ) )
370 368 369 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( { <. 1 , 1 >. } u. c ) Fn ( 1 ... ( N + 1 ) ) )
371 eqfnfv 
 |-  ( ( ( F o. b ) Fn ( 1 ... ( N + 1 ) ) /\ ( { <. 1 , 1 >. } u. c ) Fn ( 1 ... ( N + 1 ) ) ) -> ( ( F o. b ) = ( { <. 1 , 1 >. } u. c ) <-> A. y e. ( 1 ... ( N + 1 ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
372 367 370 371 syl2anc 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) = ( { <. 1 , 1 >. } u. c ) <-> A. y e. ( 1 ... ( N + 1 ) ) ( ( F o. b ) ` y ) = ( ( { <. 1 , 1 >. } u. c ) ` y ) ) )
373 fnssres 
 |-  ( ( ( F o. b ) Fn ( 1 ... ( N + 1 ) ) /\ ( 2 ... ( N + 1 ) ) C_ ( 1 ... ( N + 1 ) ) ) -> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) Fn ( 2 ... ( N + 1 ) ) )
374 367 122 373 sylancl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) Fn ( 2 ... ( N + 1 ) ) )
375 195 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) )
376 f1ofn 
 |-  ( c : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) -> c Fn ( 2 ... ( N + 1 ) ) )
377 375 376 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> c Fn ( 2 ... ( N + 1 ) ) )
378 eqfnfv 
 |-  ( ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) Fn ( 2 ... ( N + 1 ) ) /\ c Fn ( 2 ... ( N + 1 ) ) ) -> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) = c <-> A. y e. ( 2 ... ( N + 1 ) ) ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) = ( c ` y ) ) )
379 374 377 378 syl2anc 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) = c <-> A. y e. ( 2 ... ( N + 1 ) ) ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ` y ) = ( c ` y ) ) )
380 366 372 379 3bitr4d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) = ( { <. 1 , 1 >. } u. c ) <-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) = c ) )
381 eqcom 
 |-  ( ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) = c <-> c = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) )
382 380 381 bitrdi 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( F o. b ) = ( { <. 1 , 1 >. } u. c ) <-> c = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ) )
383 335 347 382 3bitr3d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b = ( F o. ( { <. 1 , 1 >. } u. c ) ) <-> c = ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ) )
384 20 185 325 383 f1o2d 
 |-  ( ph -> ( b e. B |-> ( ( F o. b ) |` ( 2 ... ( N + 1 ) ) ) ) : B -1-1-onto-> C )
385 19 384 hasheqf1od 
 |-  ( ph -> ( # ` B ) = ( # ` C ) )
386 1 2 derangen2 
 |-  ( ( 2 ... ( N + 1 ) ) e. Fin -> ( D ` ( 2 ... ( N + 1 ) ) ) = ( S ` ( # ` ( 2 ... ( N + 1 ) ) ) ) )
387 1 derangval 
 |-  ( ( 2 ... ( N + 1 ) ) e. Fin -> ( D ` ( 2 ... ( N + 1 ) ) ) = ( # ` { f | ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) } ) )
388 10 fveq2i 
 |-  ( # ` C ) = ( # ` { f | ( f : ( 2 ... ( N + 1 ) ) -1-1-onto-> ( 2 ... ( N + 1 ) ) /\ A. y e. ( 2 ... ( N + 1 ) ) ( f ` y ) =/= y ) } )
389 387 388 eqtr4di 
 |-  ( ( 2 ... ( N + 1 ) ) e. Fin -> ( D ` ( 2 ... ( N + 1 ) ) ) = ( # ` C ) )
390 386 389 eqtr3d 
 |-  ( ( 2 ... ( N + 1 ) ) e. Fin -> ( S ` ( # ` ( 2 ... ( N + 1 ) ) ) ) = ( # ` C ) )
391 166 390 ax-mp 
 |-  ( S ` ( # ` ( 2 ... ( N + 1 ) ) ) ) = ( # ` C )
392 4 60 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
393 eluzp1p1 
 |-  ( N e. ( ZZ>= ` 1 ) -> ( N + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
394 392 393 syl 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` ( 1 + 1 ) ) )
395 df-2 
 |-  2 = ( 1 + 1 )
396 395 fveq2i 
 |-  ( ZZ>= ` 2 ) = ( ZZ>= ` ( 1 + 1 ) )
397 394 396 eleqtrrdi 
 |-  ( ph -> ( N + 1 ) e. ( ZZ>= ` 2 ) )
398 hashfz 
 |-  ( ( N + 1 ) e. ( ZZ>= ` 2 ) -> ( # ` ( 2 ... ( N + 1 ) ) ) = ( ( ( N + 1 ) - 2 ) + 1 ) )
399 397 398 syl 
 |-  ( ph -> ( # ` ( 2 ... ( N + 1 ) ) ) = ( ( ( N + 1 ) - 2 ) + 1 ) )
400 59 nncnd 
 |-  ( ph -> ( N + 1 ) e. CC )
401 2cnd 
 |-  ( ph -> 2 e. CC )
402 1cnd 
 |-  ( ph -> 1 e. CC )
403 400 401 402 subsubd 
 |-  ( ph -> ( ( N + 1 ) - ( 2 - 1 ) ) = ( ( ( N + 1 ) - 2 ) + 1 ) )
404 2m1e1 
 |-  ( 2 - 1 ) = 1
405 404 oveq2i 
 |-  ( ( N + 1 ) - ( 2 - 1 ) ) = ( ( N + 1 ) - 1 )
406 4 nncnd 
 |-  ( ph -> N e. CC )
407 ax-1cn 
 |-  1 e. CC
408 pncan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N + 1 ) - 1 ) = N )
409 406 407 408 sylancl 
 |-  ( ph -> ( ( N + 1 ) - 1 ) = N )
410 405 409 syl5eq 
 |-  ( ph -> ( ( N + 1 ) - ( 2 - 1 ) ) = N )
411 399 403 410 3eqtr2d 
 |-  ( ph -> ( # ` ( 2 ... ( N + 1 ) ) ) = N )
412 411 fveq2d 
 |-  ( ph -> ( S ` ( # ` ( 2 ... ( N + 1 ) ) ) ) = ( S ` N ) )
413 391 412 eqtr3id 
 |-  ( ph -> ( # ` C ) = ( S ` N ) )
414 385 413 eqtrd 
 |-  ( ph -> ( # ` B ) = ( S ` N ) )