Metamath Proof Explorer

Theorem subfacp1lem3

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 that satisfy this for fixed M = ( f1 ) is in bijection with N - 1 derangements, by simply dropping the x = 1 and x = M points from the function to get a derangement on K = ( 1 ... ( N - 1 ) ) \ { 1 , M } . (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 } )
subfacp1lem3.b 
|- B = { g e. A | ( ( g ` 1 ) = M /\ ( g ` M ) = 1 ) }
subfacp1lem3.c 
|- C = { f | ( f : K -1-1-onto-> K /\ A. y e. K ( f ` y ) =/= y ) }
Assertion subfacp1lem3 
|- ( ph -> ( # ` B ) = ( S ` ( N - 1 ) ) )

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 subfacp1lem3.b 
 |-  B = { g e. A | ( ( g ` 1 ) = M /\ ( g ` M ) = 1 ) }
9 subfacp1lem3.c 
 |-  C = { f | ( f : K -1-1-onto-> K /\ A. y e. K ( f ` y ) =/= y ) }
10 fzfi 
 |-  ( 1 ... ( N + 1 ) ) e. Fin
11 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 )
12 10 11 ax-mp 
 |-  { f | ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) } e. Fin
13 3 12 eqeltri 
 |-  A e. Fin
14 8 ssrab3 
 |-  B C_ A
15 ssfi 
 |-  ( ( A e. Fin /\ B C_ A ) -> B e. Fin )
16 13 14 15 mp2an 
 |-  B e. Fin
17 16 elexi 
 |-  B e. _V
18 17 a1i 
 |-  ( ph -> B e. _V )
19 eqid 
 |-  ( b e. B |-> ( b |` K ) ) = ( b e. B |-> ( b |` K ) )
20 fveq1 
 |-  ( g = b -> ( g ` 1 ) = ( b ` 1 ) )
21 20 eqeq1d 
 |-  ( g = b -> ( ( g ` 1 ) = M <-> ( b ` 1 ) = M ) )
22 fveq1 
 |-  ( g = b -> ( g ` M ) = ( b ` M ) )
23 22 eqeq1d 
 |-  ( g = b -> ( ( g ` M ) = 1 <-> ( b ` M ) = 1 ) )
24 21 23 anbi12d 
 |-  ( g = b -> ( ( ( g ` 1 ) = M /\ ( g ` M ) = 1 ) <-> ( ( b ` 1 ) = M /\ ( b ` M ) = 1 ) ) )
25 24 8 elrab2 
 |-  ( b e. B <-> ( b e. A /\ ( ( b ` 1 ) = M /\ ( b ` M ) = 1 ) ) )
26 25 bilani 
 |-  ( ( ph /\ b e. B ) -> ( b e. A /\ ( ( b ` 1 ) = M /\ ( b ` M ) = 1 ) ) )
27 26 simpld 
 |-  ( ( ph /\ b e. B ) -> b e. A )
28 vex 
 |-  b e. _V
29 f1oeq1 
 |-  ( f = b -> ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) <-> b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
30 fveq1 
 |-  ( f = b -> ( f ` y ) = ( b ` y ) )
31 30 neeq1d 
 |-  ( f = b -> ( ( f ` y ) =/= y <-> ( b ` y ) =/= y ) )
32 31 ralbidv 
 |-  ( f = b -> ( A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y <-> A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y ) )
33 29 32 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 ) ) )
34 28 33 3 elab2 
 |-  ( b e. A <-> ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y ) )
35 27 34 sylib 
 |-  ( ( ph /\ b e. B ) -> ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y ) )
36 35 simpld 
 |-  ( ( ph /\ b e. B ) -> b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
37 f1of1 
 |-  ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> b : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) )
38 df-f1 
 |-  ( b : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) <-> ( b : ( 1 ... ( N + 1 ) ) --> ( 1 ... ( N + 1 ) ) /\ Fun `' b ) )
39 38 simprbi 
 |-  ( b : ( 1 ... ( N + 1 ) ) -1-1-> ( 1 ... ( N + 1 ) ) -> Fun `' b )
40 36 37 39 3syl 
 |-  ( ( ph /\ b e. B ) -> Fun `' b )
41 f1ofn 
 |-  ( b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> b Fn ( 1 ... ( N + 1 ) ) )
42 36 41 syl 
 |-  ( ( ph /\ b e. B ) -> b Fn ( 1 ... ( N + 1 ) ) )
43 fnresdm 
 |-  ( b Fn ( 1 ... ( N + 1 ) ) -> ( b |` ( 1 ... ( N + 1 ) ) ) = b )
44 f1oeq1 
 |-  ( ( b |` ( 1 ... ( N + 1 ) ) ) = b -> ( ( b |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) <-> b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
45 42 43 44 3syl 
 |-  ( ( ph /\ b e. B ) -> ( ( b |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) <-> b : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
46 36 45 mpbird 
 |-  ( ( ph /\ b e. B ) -> ( b |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
47 f1ofo 
 |-  ( ( b |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( b |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -onto-> ( 1 ... ( N + 1 ) ) )
48 46 47 syl 
 |-  ( ( ph /\ b e. B ) -> ( b |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -onto-> ( 1 ... ( N + 1 ) ) )
49 ssun2 
 |-  { 1 , M } C_ ( K u. { 1 , M } )
50 1 2 3 4 5 6 7 subfacp1lem1 
 |-  ( ph -> ( ( K i^i { 1 , M } ) = (/) /\ ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) /\ ( # ` K ) = ( N - 1 ) ) )
51 50 simp2d 
 |-  ( ph -> ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) )
52 49 51 sseqtrid 
 |-  ( ph -> { 1 , M } C_ ( 1 ... ( N + 1 ) ) )
53 52 adantr 
 |-  ( ( ph /\ b e. B ) -> { 1 , M } C_ ( 1 ... ( N + 1 ) ) )
54 42 53 fnssresd 
 |-  ( ( ph /\ b e. B ) -> ( b |` { 1 , M } ) Fn { 1 , M } )
55 26 simprd 
 |-  ( ( ph /\ b e. B ) -> ( ( b ` 1 ) = M /\ ( b ` M ) = 1 ) )
56 55 simpld 
 |-  ( ( ph /\ b e. B ) -> ( b ` 1 ) = M )
57 6 prid2 
 |-  M e. { 1 , M }
58 56 57 eqeltrdi 
 |-  ( ( ph /\ b e. B ) -> ( b ` 1 ) e. { 1 , M } )
59 55 simprd 
 |-  ( ( ph /\ b e. B ) -> ( b ` M ) = 1 )
60 1ex 
 |-  1 e. _V
61 60 prid1 
 |-  1 e. { 1 , M }
62 59 61 eqeltrdi 
 |-  ( ( ph /\ b e. B ) -> ( b ` M ) e. { 1 , M } )
63 fveq2 
 |-  ( x = 1 -> ( b ` x ) = ( b ` 1 ) )
64 63 eleq1d 
 |-  ( x = 1 -> ( ( b ` x ) e. { 1 , M } <-> ( b ` 1 ) e. { 1 , M } ) )
65 fveq2 
 |-  ( x = M -> ( b ` x ) = ( b ` M ) )
66 65 eleq1d 
 |-  ( x = M -> ( ( b ` x ) e. { 1 , M } <-> ( b ` M ) e. { 1 , M } ) )
67 60 6 64 66 ralpr 
 |-  ( A. x e. { 1 , M } ( b ` x ) e. { 1 , M } <-> ( ( b ` 1 ) e. { 1 , M } /\ ( b ` M ) e. { 1 , M } ) )
68 58 62 67 sylanbrc 
 |-  ( ( ph /\ b e. B ) -> A. x e. { 1 , M } ( b ` x ) e. { 1 , M } )
69 fvres 
 |-  ( x e. { 1 , M } -> ( ( b |` { 1 , M } ) ` x ) = ( b ` x ) )
70 69 eleq1d 
 |-  ( x e. { 1 , M } -> ( ( ( b |` { 1 , M } ) ` x ) e. { 1 , M } <-> ( b ` x ) e. { 1 , M } ) )
71 70 ralbiia 
 |-  ( A. x e. { 1 , M } ( ( b |` { 1 , M } ) ` x ) e. { 1 , M } <-> A. x e. { 1 , M } ( b ` x ) e. { 1 , M } )
72 68 71 sylibr 
 |-  ( ( ph /\ b e. B ) -> A. x e. { 1 , M } ( ( b |` { 1 , M } ) ` x ) e. { 1 , M } )
73 ffnfv 
 |-  ( ( b |` { 1 , M } ) : { 1 , M } --> { 1 , M } <-> ( ( b |` { 1 , M } ) Fn { 1 , M } /\ A. x e. { 1 , M } ( ( b |` { 1 , M } ) ` x ) e. { 1 , M } ) )
74 54 72 73 sylanbrc 
 |-  ( ( ph /\ b e. B ) -> ( b |` { 1 , M } ) : { 1 , M } --> { 1 , M } )
75 fveqeq2 
 |-  ( y = M -> ( ( b ` y ) = 1 <-> ( b ` M ) = 1 ) )
76 75 rspcev 
 |-  ( ( M e. { 1 , M } /\ ( b ` M ) = 1 ) -> E. y e. { 1 , M } ( b ` y ) = 1 )
77 57 59 76 sylancr 
 |-  ( ( ph /\ b e. B ) -> E. y e. { 1 , M } ( b ` y ) = 1 )
78 fveqeq2 
 |-  ( y = 1 -> ( ( b ` y ) = M <-> ( b ` 1 ) = M ) )
79 78 rspcev 
 |-  ( ( 1 e. { 1 , M } /\ ( b ` 1 ) = M ) -> E. y e. { 1 , M } ( b ` y ) = M )
80 61 56 79 sylancr 
 |-  ( ( ph /\ b e. B ) -> E. y e. { 1 , M } ( b ` y ) = M )
81 eqeq2 
 |-  ( x = 1 -> ( ( b ` y ) = x <-> ( b ` y ) = 1 ) )
82 81 rexbidv 
 |-  ( x = 1 -> ( E. y e. { 1 , M } ( b ` y ) = x <-> E. y e. { 1 , M } ( b ` y ) = 1 ) )
83 eqeq2 
 |-  ( x = M -> ( ( b ` y ) = x <-> ( b ` y ) = M ) )
84 83 rexbidv 
 |-  ( x = M -> ( E. y e. { 1 , M } ( b ` y ) = x <-> E. y e. { 1 , M } ( b ` y ) = M ) )
85 60 6 82 84 ralpr 
 |-  ( A. x e. { 1 , M } E. y e. { 1 , M } ( b ` y ) = x <-> ( E. y e. { 1 , M } ( b ` y ) = 1 /\ E. y e. { 1 , M } ( b ` y ) = M ) )
86 77 80 85 sylanbrc 
 |-  ( ( ph /\ b e. B ) -> A. x e. { 1 , M } E. y e. { 1 , M } ( b ` y ) = x )
87 eqcom 
 |-  ( x = ( ( b |` { 1 , M } ) ` y ) <-> ( ( b |` { 1 , M } ) ` y ) = x )
88 fvres 
 |-  ( y e. { 1 , M } -> ( ( b |` { 1 , M } ) ` y ) = ( b ` y ) )
89 88 eqeq1d 
 |-  ( y e. { 1 , M } -> ( ( ( b |` { 1 , M } ) ` y ) = x <-> ( b ` y ) = x ) )
90 87 89 bitrid 
 |-  ( y e. { 1 , M } -> ( x = ( ( b |` { 1 , M } ) ` y ) <-> ( b ` y ) = x ) )
91 90 rexbiia 
 |-  ( E. y e. { 1 , M } x = ( ( b |` { 1 , M } ) ` y ) <-> E. y e. { 1 , M } ( b ` y ) = x )
92 91 ralbii 
 |-  ( A. x e. { 1 , M } E. y e. { 1 , M } x = ( ( b |` { 1 , M } ) ` y ) <-> A. x e. { 1 , M } E. y e. { 1 , M } ( b ` y ) = x )
93 86 92 sylibr 
 |-  ( ( ph /\ b e. B ) -> A. x e. { 1 , M } E. y e. { 1 , M } x = ( ( b |` { 1 , M } ) ` y ) )
94 dffo3 
 |-  ( ( b |` { 1 , M } ) : { 1 , M } -onto-> { 1 , M } <-> ( ( b |` { 1 , M } ) : { 1 , M } --> { 1 , M } /\ A. x e. { 1 , M } E. y e. { 1 , M } x = ( ( b |` { 1 , M } ) ` y ) ) )
95 74 93 94 sylanbrc 
 |-  ( ( ph /\ b e. B ) -> ( b |` { 1 , M } ) : { 1 , M } -onto-> { 1 , M } )
96 resdif 
 |-  ( ( Fun `' b /\ ( b |` ( 1 ... ( N + 1 ) ) ) : ( 1 ... ( N + 1 ) ) -onto-> ( 1 ... ( N + 1 ) ) /\ ( b |` { 1 , M } ) : { 1 , M } -onto-> { 1 , M } ) -> ( b |` ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) )
97 40 48 95 96 syl3anc 
 |-  ( ( ph /\ b e. B ) -> ( b |` ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) )
98 uncom 
 |-  ( { 1 , M } u. K ) = ( K u. { 1 , M } )
99 98 51 eqtrid 
 |-  ( ph -> ( { 1 , M } u. K ) = ( 1 ... ( N + 1 ) ) )
100 incom 
 |-  ( { 1 , M } i^i K ) = ( K i^i { 1 , M } )
101 50 simp1d 
 |-  ( ph -> ( K i^i { 1 , M } ) = (/) )
102 100 101 eqtrid 
 |-  ( ph -> ( { 1 , M } i^i K ) = (/) )
103 uneqdifeq 
 |-  ( ( { 1 , M } C_ ( 1 ... ( N + 1 ) ) /\ ( { 1 , M } i^i K ) = (/) ) -> ( ( { 1 , M } u. K ) = ( 1 ... ( N + 1 ) ) <-> ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) = K ) )
104 52 102 103 syl2anc 
 |-  ( ph -> ( ( { 1 , M } u. K ) = ( 1 ... ( N + 1 ) ) <-> ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) = K ) )
105 99 104 mpbid 
 |-  ( ph -> ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) = K )
106 105 adantr 
 |-  ( ( ph /\ b e. B ) -> ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) = K )
107 reseq2 
 |-  ( ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) = K -> ( b |` ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) ) = ( b |` K ) )
108 107 f1oeq1d 
 |-  ( ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) = K -> ( ( b |` ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) <-> ( b |` K ) : ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) ) )
109 f1oeq2 
 |-  ( ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) = K -> ( ( b |` K ) : ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) <-> ( b |` K ) : K -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) ) )
110 f1oeq3 
 |-  ( ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) = K -> ( ( b |` K ) : K -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) <-> ( b |` K ) : K -1-1-onto-> K ) )
111 108 109 110 3bitrd 
 |-  ( ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) = K -> ( ( b |` ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) <-> ( b |` K ) : K -1-1-onto-> K ) )
112 106 111 syl 
 |-  ( ( ph /\ b e. B ) -> ( ( b |` ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) ) : ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) -1-1-onto-> ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) <-> ( b |` K ) : K -1-1-onto-> K ) )
113 97 112 mpbid 
 |-  ( ( ph /\ b e. B ) -> ( b |` K ) : K -1-1-onto-> K )
114 ssun1 
 |-  K C_ ( K u. { 1 , M } )
115 114 51 sseqtrid 
 |-  ( ph -> K C_ ( 1 ... ( N + 1 ) ) )
116 115 adantr 
 |-  ( ( ph /\ b e. B ) -> K C_ ( 1 ... ( N + 1 ) ) )
117 35 simprd 
 |-  ( ( ph /\ b e. B ) -> A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y )
118 ssralv 
 |-  ( K C_ ( 1 ... ( N + 1 ) ) -> ( A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y -> A. y e. K ( b ` y ) =/= y ) )
119 116 117 118 sylc 
 |-  ( ( ph /\ b e. B ) -> A. y e. K ( b ` y ) =/= y )
120 28 resex 
 |-  ( b |` K ) e. _V
121 f1oeq1 
 |-  ( f = ( b |` K ) -> ( f : K -1-1-onto-> K <-> ( b |` K ) : K -1-1-onto-> K ) )
122 fveq1 
 |-  ( f = ( b |` K ) -> ( f ` y ) = ( ( b |` K ) ` y ) )
123 fvres 
 |-  ( y e. K -> ( ( b |` K ) ` y ) = ( b ` y ) )
124 122 123 sylan9eq 
 |-  ( ( f = ( b |` K ) /\ y e. K ) -> ( f ` y ) = ( b ` y ) )
125 124 neeq1d 
 |-  ( ( f = ( b |` K ) /\ y e. K ) -> ( ( f ` y ) =/= y <-> ( b ` y ) =/= y ) )
126 125 ralbidva 
 |-  ( f = ( b |` K ) -> ( A. y e. K ( f ` y ) =/= y <-> A. y e. K ( b ` y ) =/= y ) )
127 121 126 anbi12d 
 |-  ( f = ( b |` K ) -> ( ( f : K -1-1-onto-> K /\ A. y e. K ( f ` y ) =/= y ) <-> ( ( b |` K ) : K -1-1-onto-> K /\ A. y e. K ( b ` y ) =/= y ) ) )
128 120 127 9 elab2 
 |-  ( ( b |` K ) e. C <-> ( ( b |` K ) : K -1-1-onto-> K /\ A. y e. K ( b ` y ) =/= y ) )
129 113 119 128 sylanbrc 
 |-  ( ( ph /\ b e. B ) -> ( b |` K ) e. C )
130 4 adantr 
 |-  ( ( ph /\ c e. C ) -> N e. NN )
131 5 adantr 
 |-  ( ( ph /\ c e. C ) -> M e. ( 2 ... ( N + 1 ) ) )
132 eqid 
 |-  ( c u. { <. 1 , M >. , <. M , 1 >. } ) = ( c u. { <. 1 , M >. , <. M , 1 >. } )
133 vex 
 |-  c e. _V
134 f1oeq1 
 |-  ( f = c -> ( f : K -1-1-onto-> K <-> c : K -1-1-onto-> K ) )
135 fveq1 
 |-  ( f = c -> ( f ` y ) = ( c ` y ) )
136 135 neeq1d 
 |-  ( f = c -> ( ( f ` y ) =/= y <-> ( c ` y ) =/= y ) )
137 136 ralbidv 
 |-  ( f = c -> ( A. y e. K ( f ` y ) =/= y <-> A. y e. K ( c ` y ) =/= y ) )
138 134 137 anbi12d 
 |-  ( f = c -> ( ( f : K -1-1-onto-> K /\ A. y e. K ( f ` y ) =/= y ) <-> ( c : K -1-1-onto-> K /\ A. y e. K ( c ` y ) =/= y ) ) )
139 133 138 9 elab2 
 |-  ( c e. C <-> ( c : K -1-1-onto-> K /\ A. y e. K ( c ` y ) =/= y ) )
140 139 bilani 
 |-  ( ( ph /\ c e. C ) -> ( c : K -1-1-onto-> K /\ A. y e. K ( c ` y ) =/= y ) )
141 140 simpld 
 |-  ( ( ph /\ c e. C ) -> c : K -1-1-onto-> K )
142 1 2 3 130 131 6 7 132 141 subfacp1lem2a 
 |-  ( ( ph /\ c e. C ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) = M /\ ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) = 1 ) )
143 142 simp1d 
 |-  ( ( ph /\ c e. C ) -> ( c u. { <. 1 , M >. , <. M , 1 >. } ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
144 1 2 3 130 131 6 7 132 141 subfacp1lem2b 
 |-  ( ( ( ph /\ c e. C ) /\ y e. K ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) = ( c ` y ) )
145 140 simprd 
 |-  ( ( ph /\ c e. C ) -> A. y e. K ( c ` y ) =/= y )
146 145 r19.21bi 
 |-  ( ( ( ph /\ c e. C ) /\ y e. K ) -> ( c ` y ) =/= y )
147 144 146 eqnetrd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. K ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y )
148 147 ralrimiva 
 |-  ( ( ph /\ c e. C ) -> A. y e. K ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y )
149 142 simp2d 
 |-  ( ( ph /\ c e. C ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) = M )
150 elfzuz 
 |-  ( M e. ( 2 ... ( N + 1 ) ) -> M e. ( ZZ>= ` 2 ) )
151 eluz2b3 
 |-  ( M e. ( ZZ>= ` 2 ) <-> ( M e. NN /\ M =/= 1 ) )
152 151 simprbi 
 |-  ( M e. ( ZZ>= ` 2 ) -> M =/= 1 )
153 5 150 152 3syl 
 |-  ( ph -> M =/= 1 )
154 153 adantr 
 |-  ( ( ph /\ c e. C ) -> M =/= 1 )
155 149 154 eqnetrd 
 |-  ( ( ph /\ c e. C ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) =/= 1 )
156 142 simp3d 
 |-  ( ( ph /\ c e. C ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) = 1 )
157 154 necomd 
 |-  ( ( ph /\ c e. C ) -> 1 =/= M )
158 156 157 eqnetrd 
 |-  ( ( ph /\ c e. C ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) =/= M )
159 fveq2 
 |-  ( y = 1 -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) )
160 id 
 |-  ( y = 1 -> y = 1 )
161 159 160 neeq12d 
 |-  ( y = 1 -> ( ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y <-> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) =/= 1 ) )
162 fveq2 
 |-  ( y = M -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) )
163 id 
 |-  ( y = M -> y = M )
164 162 163 neeq12d 
 |-  ( y = M -> ( ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y <-> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) =/= M ) )
165 60 6 161 164 ralpr 
 |-  ( A. y e. { 1 , M } ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y <-> ( ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) =/= 1 /\ ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) =/= M ) )
166 155 158 165 sylanbrc 
 |-  ( ( ph /\ c e. C ) -> A. y e. { 1 , M } ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y )
167 ralunb 
 |-  ( A. y e. ( K u. { 1 , M } ) ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y <-> ( A. y e. K ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y /\ A. y e. { 1 , M } ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y ) )
168 148 166 167 sylanbrc 
 |-  ( ( ph /\ c e. C ) -> A. y e. ( K u. { 1 , M } ) ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y )
169 51 adantr 
 |-  ( ( ph /\ c e. C ) -> ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) )
170 168 169 raleqtrdv 
 |-  ( ( ph /\ c e. C ) -> A. y e. ( 1 ... ( N + 1 ) ) ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y )
171 prex 
 |-  { <. 1 , M >. , <. M , 1 >. } e. _V
172 133 171 unex 
 |-  ( c u. { <. 1 , M >. , <. M , 1 >. } ) e. _V
173 f1oeq1 
 |-  ( f = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) <-> ( c u. { <. 1 , M >. , <. M , 1 >. } ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) ) )
174 fveq1 
 |-  ( f = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( f ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) )
175 174 neeq1d 
 |-  ( f = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( ( f ` y ) =/= y <-> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y ) )
176 175 ralbidv 
 |-  ( f = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y <-> A. y e. ( 1 ... ( N + 1 ) ) ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y ) )
177 173 176 anbi12d 
 |-  ( f = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( ( f : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( f ` y ) =/= y ) <-> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y ) ) )
178 172 177 3 elab2 
 |-  ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) e. A <-> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) /\ A. y e. ( 1 ... ( N + 1 ) ) ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y ) )
179 143 170 178 sylanbrc 
 |-  ( ( ph /\ c e. C ) -> ( c u. { <. 1 , M >. , <. M , 1 >. } ) e. A )
180 149 156 jca 
 |-  ( ( ph /\ c e. C ) -> ( ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) = M /\ ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) = 1 ) )
181 fveq1 
 |-  ( g = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( g ` 1 ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) )
182 181 eqeq1d 
 |-  ( g = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( ( g ` 1 ) = M <-> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) = M ) )
183 fveq1 
 |-  ( g = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( g ` M ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) )
184 183 eqeq1d 
 |-  ( g = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( ( g ` M ) = 1 <-> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) = 1 ) )
185 182 184 anbi12d 
 |-  ( g = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( ( ( g ` 1 ) = M /\ ( g ` M ) = 1 ) <-> ( ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) = M /\ ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) = 1 ) ) )
186 185 8 elrab2 
 |-  ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) e. B <-> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) e. A /\ ( ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) = M /\ ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) = 1 ) ) )
187 179 180 186 sylanbrc 
 |-  ( ( ph /\ c e. C ) -> ( c u. { <. 1 , M >. , <. M , 1 >. } ) e. B )
188 56 adantrr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b ` 1 ) = M )
189 149 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) = M )
190 188 189 eqtr4d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b ` 1 ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) )
191 59 adantrr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b ` M ) = 1 )
192 156 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) = 1 )
193 191 192 eqtr4d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b ` M ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) )
194 fveq2 
 |-  ( y = 1 -> ( b ` y ) = ( b ` 1 ) )
195 194 159 eqeq12d 
 |-  ( y = 1 -> ( ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> ( b ` 1 ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) ) )
196 fveq2 
 |-  ( y = M -> ( b ` y ) = ( b ` M ) )
197 196 162 eqeq12d 
 |-  ( y = M -> ( ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> ( b ` M ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) ) )
198 60 6 195 197 ralpr 
 |-  ( A. y e. { 1 , M } ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> ( ( b ` 1 ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) /\ ( b ` M ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) ) )
199 190 193 198 sylanbrc 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> A. y e. { 1 , M } ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) )
200 199 biantrud 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( A. y e. K ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> ( A. y e. K ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) /\ A. y e. { 1 , M } ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) ) ) )
201 ralunb 
 |-  ( A. y e. ( K u. { 1 , M } ) ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> ( A. y e. K ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) /\ A. y e. { 1 , M } ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) ) )
202 200 201 bitr4di 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( A. y e. K ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> A. y e. ( K u. { 1 , M } ) ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) ) )
203 144 eqeq2d 
 |-  ( ( ( ph /\ c e. C ) /\ y e. K ) -> ( ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> ( b ` y ) = ( c ` y ) ) )
204 203 ralbidva 
 |-  ( ( ph /\ c e. C ) -> ( A. y e. K ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> A. y e. K ( b ` y ) = ( c ` y ) ) )
205 204 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( A. y e. K ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> A. y e. K ( b ` y ) = ( c ` y ) ) )
206 51 adantr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) )
207 206 raleqdv 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( A. y e. ( K u. { 1 , M } ) ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) ) )
208 202 205 207 3bitr3rd 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> A. y e. K ( b ` y ) = ( c ` y ) ) )
209 123 eqeq2d 
 |-  ( y e. K -> ( ( c ` y ) = ( ( b |` K ) ` y ) <-> ( c ` y ) = ( b ` y ) ) )
210 eqcom 
 |-  ( ( c ` y ) = ( b ` y ) <-> ( b ` y ) = ( c ` y ) )
211 209 210 bitrdi 
 |-  ( y e. K -> ( ( c ` y ) = ( ( b |` K ) ` y ) <-> ( b ` y ) = ( c ` y ) ) )
212 211 ralbiia 
 |-  ( A. y e. K ( c ` y ) = ( ( b |` K ) ` y ) <-> A. y e. K ( b ` y ) = ( c ` y ) )
213 208 212 bitr4di 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> A. y e. K ( c ` y ) = ( ( b |` K ) ` y ) ) )
214 42 adantrr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> b Fn ( 1 ... ( N + 1 ) ) )
215 143 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( c u. { <. 1 , M >. , <. M , 1 >. } ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
216 f1ofn 
 |-  ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) -> ( c u. { <. 1 , M >. , <. M , 1 >. } ) Fn ( 1 ... ( N + 1 ) ) )
217 215 216 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( c u. { <. 1 , M >. , <. M , 1 >. } ) Fn ( 1 ... ( N + 1 ) ) )
218 eqfnfv 
 |-  ( ( b Fn ( 1 ... ( N + 1 ) ) /\ ( c u. { <. 1 , M >. , <. M , 1 >. } ) Fn ( 1 ... ( N + 1 ) ) ) -> ( b = ( c u. { <. 1 , M >. , <. M , 1 >. } ) <-> A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) ) )
219 214 217 218 syl2anc 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b = ( c u. { <. 1 , M >. , <. M , 1 >. } ) <-> A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) ) )
220 141 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> c : K -1-1-onto-> K )
221 f1ofn 
 |-  ( c : K -1-1-onto-> K -> c Fn K )
222 220 221 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> c Fn K )
223 115 adantr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> K C_ ( 1 ... ( N + 1 ) ) )
224 214 223 fnssresd 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b |` K ) Fn K )
225 eqfnfv 
 |-  ( ( c Fn K /\ ( b |` K ) Fn K ) -> ( c = ( b |` K ) <-> A. y e. K ( c ` y ) = ( ( b |` K ) ` y ) ) )
226 222 224 225 syl2anc 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( c = ( b |` K ) <-> A. y e. K ( c ` y ) = ( ( b |` K ) ` y ) ) )
227 213 219 226 3bitr4d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b = ( c u. { <. 1 , M >. , <. M , 1 >. } ) <-> c = ( b |` K ) ) )
228 19 129 187 227 f1o2d 
 |-  ( ph -> ( b e. B |-> ( b |` K ) ) : B -1-1-onto-> C )
229 18 228 hasheqf1od 
 |-  ( ph -> ( # ` B ) = ( # ` C ) )
230 9 fveq2i 
 |-  ( # ` C ) = ( # ` { f | ( f : K -1-1-onto-> K /\ A. y e. K ( f ` y ) =/= y ) } )
231 fzfi 
 |-  ( 2 ... ( N + 1 ) ) e. Fin
232 diffi 
 |-  ( ( 2 ... ( N + 1 ) ) e. Fin -> ( ( 2 ... ( N + 1 ) ) \ { M } ) e. Fin )
233 231 232 ax-mp 
 |-  ( ( 2 ... ( N + 1 ) ) \ { M } ) e. Fin
234 7 233 eqeltri 
 |-  K e. Fin
235 1 derangval 
 |-  ( K e. Fin -> ( D ` K ) = ( # ` { f | ( f : K -1-1-onto-> K /\ A. y e. K ( f ` y ) =/= y ) } ) )
236 234 235 ax-mp 
 |-  ( D ` K ) = ( # ` { f | ( f : K -1-1-onto-> K /\ A. y e. K ( f ` y ) =/= y ) } )
237 1 2 derangen2 
 |-  ( K e. Fin -> ( D ` K ) = ( S ` ( # ` K ) ) )
238 234 237 ax-mp 
 |-  ( D ` K ) = ( S ` ( # ` K ) )
239 230 236 238 3eqtr2ri 
 |-  ( S ` ( # ` K ) ) = ( # ` C )
240 50 simp3d 
 |-  ( ph -> ( # ` K ) = ( N - 1 ) )
241 240 fveq2d 
 |-  ( ph -> ( S ` ( # ` K ) ) = ( S ` ( N - 1 ) ) )
242 239 241 eqtr3id 
 |-  ( ph -> ( # ` C ) = ( S ` ( N - 1 ) ) )
243 229 242 eqtrd 
 |-  ( ph -> ( # ` B ) = ( S ` ( N - 1 ) ) )