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 syl5eq 
 |-  ( 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 syl5eq 
 |-  ( 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 f1oeq1 
 |-  ( ( b |` ( ( 1 ... ( N + 1 ) ) \ { 1 , M } ) ) = ( b |` 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 108 109 syl 
 |-  ( ( ( 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 } ) ) )
111 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 } ) ) )
112 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 ) )
113 110 111 112 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 ) )
114 107 113 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 ) )
115 98 114 mpbid 
 |-  ( ( ph /\ b e. B ) -> ( b |` K ) : K -1-1-onto-> K )
116 ssun1 
 |-  K C_ ( K u. { 1 , M } )
117 116 52 sseqtrid 
 |-  ( ph -> K C_ ( 1 ... ( N + 1 ) ) )
118 117 adantr 
 |-  ( ( ph /\ b e. B ) -> K C_ ( 1 ... ( N + 1 ) ) )
119 36 simprd 
 |-  ( ( ph /\ b e. B ) -> A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y )
120 ssralv 
 |-  ( K C_ ( 1 ... ( N + 1 ) ) -> ( A. y e. ( 1 ... ( N + 1 ) ) ( b ` y ) =/= y -> A. y e. K ( b ` y ) =/= y ) )
121 118 119 120 sylc 
 |-  ( ( ph /\ b e. B ) -> A. y e. K ( b ` y ) =/= y )
122 29 resex 
 |-  ( b |` K ) e. _V
123 f1oeq1 
 |-  ( f = ( b |` K ) -> ( f : K -1-1-onto-> K <-> ( b |` K ) : K -1-1-onto-> K ) )
124 fveq1 
 |-  ( f = ( b |` K ) -> ( f ` y ) = ( ( b |` K ) ` y ) )
125 fvres 
 |-  ( y e. K -> ( ( b |` K ) ` y ) = ( b ` y ) )
126 124 125 sylan9eq 
 |-  ( ( f = ( b |` K ) /\ y e. K ) -> ( f ` y ) = ( b ` y ) )
127 126 neeq1d 
 |-  ( ( f = ( b |` K ) /\ y e. K ) -> ( ( f ` y ) =/= y <-> ( b ` y ) =/= y ) )
128 127 ralbidva 
 |-  ( f = ( b |` K ) -> ( A. y e. K ( f ` y ) =/= y <-> A. y e. K ( b ` y ) =/= y ) )
129 123 128 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 ) ) )
130 122 129 9 elab2 
 |-  ( ( b |` K ) e. C <-> ( ( b |` K ) : K -1-1-onto-> K /\ A. y e. K ( b ` y ) =/= y ) )
131 115 121 130 sylanbrc 
 |-  ( ( ph /\ b e. B ) -> ( b |` K ) e. C )
132 4 adantr 
 |-  ( ( ph /\ c e. C ) -> N e. NN )
133 5 adantr 
 |-  ( ( ph /\ c e. C ) -> M e. ( 2 ... ( N + 1 ) ) )
134 eqid 
 |-  ( c u. { <. 1 , M >. , <. M , 1 >. } ) = ( c u. { <. 1 , M >. , <. M , 1 >. } )
135 simpr 
 |-  ( ( ph /\ c e. C ) -> c e. C )
136 vex 
 |-  c e. _V
137 f1oeq1 
 |-  ( f = c -> ( f : K -1-1-onto-> K <-> c : K -1-1-onto-> K ) )
138 fveq1 
 |-  ( f = c -> ( f ` y ) = ( c ` y ) )
139 138 neeq1d 
 |-  ( f = c -> ( ( f ` y ) =/= y <-> ( c ` y ) =/= y ) )
140 139 ralbidv 
 |-  ( f = c -> ( A. y e. K ( f ` y ) =/= y <-> A. y e. K ( c ` y ) =/= y ) )
141 137 140 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 ) ) )
142 136 141 9 elab2 
 |-  ( c e. C <-> ( c : K -1-1-onto-> K /\ A. y e. K ( c ` y ) =/= y ) )
143 135 142 sylib 
 |-  ( ( ph /\ c e. C ) -> ( c : K -1-1-onto-> K /\ A. y e. K ( c ` y ) =/= y ) )
144 143 simpld 
 |-  ( ( ph /\ c e. C ) -> c : K -1-1-onto-> K )
145 1 2 3 132 133 6 7 134 144 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 ) )
146 145 simp1d 
 |-  ( ( ph /\ c e. C ) -> ( c u. { <. 1 , M >. , <. M , 1 >. } ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
147 1 2 3 132 133 6 7 134 144 subfacp1lem2b 
 |-  ( ( ( ph /\ c e. C ) /\ y e. K ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) = ( c ` y ) )
148 143 simprd 
 |-  ( ( ph /\ c e. C ) -> A. y e. K ( c ` y ) =/= y )
149 148 r19.21bi 
 |-  ( ( ( ph /\ c e. C ) /\ y e. K ) -> ( c ` y ) =/= y )
150 147 149 eqnetrd 
 |-  ( ( ( ph /\ c e. C ) /\ y e. K ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y )
151 150 ralrimiva 
 |-  ( ( ph /\ c e. C ) -> A. y e. K ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y )
152 145 simp2d 
 |-  ( ( ph /\ c e. C ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) = M )
153 elfzuz 
 |-  ( M e. ( 2 ... ( N + 1 ) ) -> M e. ( ZZ>= ` 2 ) )
154 eluz2b3 
 |-  ( M e. ( ZZ>= ` 2 ) <-> ( M e. NN /\ M =/= 1 ) )
155 154 simprbi 
 |-  ( M e. ( ZZ>= ` 2 ) -> M =/= 1 )
156 5 153 155 3syl 
 |-  ( ph -> M =/= 1 )
157 156 adantr 
 |-  ( ( ph /\ c e. C ) -> M =/= 1 )
158 152 157 eqnetrd 
 |-  ( ( ph /\ c e. C ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) =/= 1 )
159 145 simp3d 
 |-  ( ( ph /\ c e. C ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) = 1 )
160 157 necomd 
 |-  ( ( ph /\ c e. C ) -> 1 =/= M )
161 159 160 eqnetrd 
 |-  ( ( ph /\ c e. C ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) =/= M )
162 fveq2 
 |-  ( y = 1 -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) )
163 id 
 |-  ( y = 1 -> y = 1 )
164 162 163 neeq12d 
 |-  ( y = 1 -> ( ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y <-> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) =/= 1 ) )
165 fveq2 
 |-  ( y = M -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) )
166 id 
 |-  ( y = M -> y = M )
167 165 166 neeq12d 
 |-  ( y = M -> ( ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y <-> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) =/= M ) )
168 61 6 164 167 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 ) )
169 158 161 168 sylanbrc 
 |-  ( ( ph /\ c e. C ) -> A. y e. { 1 , M } ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y )
170 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 ) )
171 151 169 170 sylanbrc 
 |-  ( ( ph /\ c e. C ) -> A. y e. ( K u. { 1 , M } ) ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y )
172 52 adantr 
 |-  ( ( ph /\ c e. C ) -> ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) )
173 172 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 ) )
174 171 173 mpbid 
 |-  ( ( ph /\ c e. C ) -> A. y e. ( 1 ... ( N + 1 ) ) ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y )
175 prex 
 |-  { <. 1 , M >. , <. M , 1 >. } e. _V
176 136 175 unex 
 |-  ( c u. { <. 1 , M >. , <. M , 1 >. } ) e. _V
177 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 ) ) ) )
178 fveq1 
 |-  ( f = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( f ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) )
179 178 neeq1d 
 |-  ( f = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( ( f ` y ) =/= y <-> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) =/= y ) )
180 179 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 ) )
181 177 180 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 ) ) )
182 176 181 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 ) )
183 146 174 182 sylanbrc 
 |-  ( ( ph /\ c e. C ) -> ( c u. { <. 1 , M >. , <. M , 1 >. } ) e. A )
184 152 159 jca 
 |-  ( ( ph /\ c e. C ) -> ( ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) = M /\ ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) = 1 ) )
185 fveq1 
 |-  ( g = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( g ` 1 ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) )
186 185 eqeq1d 
 |-  ( g = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( ( g ` 1 ) = M <-> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) = M ) )
187 fveq1 
 |-  ( g = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( g ` M ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) )
188 187 eqeq1d 
 |-  ( g = ( c u. { <. 1 , M >. , <. M , 1 >. } ) -> ( ( g ` M ) = 1 <-> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) = 1 ) )
189 186 188 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 ) ) )
190 189 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 ) ) )
191 183 184 190 sylanbrc 
 |-  ( ( ph /\ c e. C ) -> ( c u. { <. 1 , M >. , <. M , 1 >. } ) e. B )
192 57 adantrr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b ` 1 ) = M )
193 152 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) = M )
194 192 193 eqtr4d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b ` 1 ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) )
195 60 adantrr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b ` M ) = 1 )
196 159 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) = 1 )
197 195 196 eqtr4d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b ` M ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) )
198 fveq2 
 |-  ( y = 1 -> ( b ` y ) = ( b ` 1 ) )
199 198 162 eqeq12d 
 |-  ( y = 1 -> ( ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> ( b ` 1 ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` 1 ) ) )
200 fveq2 
 |-  ( y = M -> ( b ` y ) = ( b ` M ) )
201 200 165 eqeq12d 
 |-  ( y = M -> ( ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> ( b ` M ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` M ) ) )
202 61 6 199 201 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 ) ) )
203 194 197 202 sylanbrc 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> A. y e. { 1 , M } ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) )
204 203 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 ) ) ) )
205 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 ) ) )
206 204 205 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 ) ) )
207 147 eqeq2d 
 |-  ( ( ( ph /\ c e. C ) /\ y e. K ) -> ( ( b ` y ) = ( ( c u. { <. 1 , M >. , <. M , 1 >. } ) ` y ) <-> ( b ` y ) = ( c ` y ) ) )
208 207 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 ) ) )
209 208 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 ) ) )
210 52 adantr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( K u. { 1 , M } ) = ( 1 ... ( N + 1 ) ) )
211 210 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 ) ) )
212 206 209 211 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 ) ) )
213 125 eqeq2d 
 |-  ( y e. K -> ( ( c ` y ) = ( ( b |` K ) ` y ) <-> ( c ` y ) = ( b ` y ) ) )
214 eqcom 
 |-  ( ( c ` y ) = ( b ` y ) <-> ( b ` y ) = ( c ` y ) )
215 213 214 syl6bb 
 |-  ( y e. K -> ( ( c ` y ) = ( ( b |` K ) ` y ) <-> ( b ` y ) = ( c ` y ) ) )
216 215 ralbiia 
 |-  ( A. y e. K ( c ` y ) = ( ( b |` K ) ` y ) <-> A. y e. K ( b ` y ) = ( c ` y ) )
217 212 216 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 ) ) )
218 43 adantrr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> b Fn ( 1 ... ( N + 1 ) ) )
219 146 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( c u. { <. 1 , M >. , <. M , 1 >. } ) : ( 1 ... ( N + 1 ) ) -1-1-onto-> ( 1 ... ( N + 1 ) ) )
220 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 ) ) )
221 219 220 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( c u. { <. 1 , M >. , <. M , 1 >. } ) Fn ( 1 ... ( N + 1 ) ) )
222 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 ) ) )
223 218 221 222 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 ) ) )
224 144 adantrl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> c : K -1-1-onto-> K )
225 f1ofn 
 |-  ( c : K -1-1-onto-> K -> c Fn K )
226 224 225 syl 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> c Fn K )
227 117 adantr 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> K C_ ( 1 ... ( N + 1 ) ) )
228 218 227 fnssresd 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b |` K ) Fn K )
229 eqfnfv 
 |-  ( ( c Fn K /\ ( b |` K ) Fn K ) -> ( c = ( b |` K ) <-> A. y e. K ( c ` y ) = ( ( b |` K ) ` y ) ) )
230 226 228 229 syl2anc 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( c = ( b |` K ) <-> A. y e. K ( c ` y ) = ( ( b |` K ) ` y ) ) )
231 217 223 230 3bitr4d 
 |-  ( ( ph /\ ( b e. B /\ c e. C ) ) -> ( b = ( c u. { <. 1 , M >. , <. M , 1 >. } ) <-> c = ( b |` K ) ) )
232 19 131 191 231 f1o2d 
 |-  ( ph -> ( b e. B |-> ( b |` K ) ) : B -1-1-onto-> C )
233 18 232 hasheqf1od 
 |-  ( ph -> ( # ` B ) = ( # ` C ) )
234 9 fveq2i 
 |-  ( # ` C ) = ( # ` { f | ( f : K -1-1-onto-> K /\ A. y e. K ( f ` y ) =/= y ) } )
235 fzfi 
 |-  ( 2 ... ( N + 1 ) ) e. Fin
236 diffi 
 |-  ( ( 2 ... ( N + 1 ) ) e. Fin -> ( ( 2 ... ( N + 1 ) ) \ { M } ) e. Fin )
237 235 236 ax-mp 
 |-  ( ( 2 ... ( N + 1 ) ) \ { M } ) e. Fin
238 7 237 eqeltri 
 |-  K e. Fin
239 1 derangval 
 |-  ( K e. Fin -> ( D ` K ) = ( # ` { f | ( f : K -1-1-onto-> K /\ A. y e. K ( f ` y ) =/= y ) } ) )
240 238 239 ax-mp 
 |-  ( D ` K ) = ( # ` { f | ( f : K -1-1-onto-> K /\ A. y e. K ( f ` y ) =/= y ) } )
241 1 2 derangen2 
 |-  ( K e. Fin -> ( D ` K ) = ( S ` ( # ` K ) ) )
242 238 241 ax-mp 
 |-  ( D ` K ) = ( S ` ( # ` K ) )
243 234 240 242 3eqtr2ri 
 |-  ( S ` ( # ` K ) ) = ( # ` C )
244 51 simp3d 
 |-  ( ph -> ( # ` K ) = ( N - 1 ) )
245 244 fveq2d 
 |-  ( ph -> ( S ` ( # ` K ) ) = ( S ` ( N - 1 ) ) )
246 243 245 syl5eqr 
 |-  ( ph -> ( # ` C ) = ( S ` ( N - 1 ) ) )
247 233 246 eqtrd 
 |-  ( ph -> ( # ` B ) = ( S ` ( N - 1 ) ) )