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 Fin f | f : x 1-1 onto x y x f y y
subfac.n S = n 0 D 1 n
subfacp1lem.a A = f | f : 1 N + 1 1-1 onto 1 N + 1 y 1 N + 1 f y y
subfacp1lem1.n φ N
subfacp1lem1.m φ M 2 N + 1
subfacp1lem1.x M V
subfacp1lem1.k K = 2 N + 1 M
subfacp1lem3.b B = g A | g 1 = M g M = 1
subfacp1lem3.c C = f | f : K 1-1 onto K y K f y y
Assertion subfacp1lem3 φ B = S N 1

Proof

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