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