Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  subfacp1lem5 Unicode version

Theorem subfacp1lem5 25130
Description: Lemma for subfacp1 25132. In subfacp1lem6 25131 we cut up the set of all derangements on first according to the value at , and then by whether or not . In this lemma, we show that the subset of all derangements with for fixed is in bijection with derangements of , because pre-composing with the function swaps and and turns the function into a bijection with and for all other , so dropping the point at yields a derangement on the remaining points. (Contributed by Mario Carneiro, 23-Jan-2015.)
Hypotheses
Ref Expression
derang.d
subfac.n
subfacp1lem.a
subfacp1lem1.n
subfacp1lem1.m
subfacp1lem1.x
subfacp1lem1.k
subfacp1lem5.b
subfacp1lem5.f
subfacp1lem5.c
Assertion
Ref Expression
subfacp1lem5
Distinct variable groups:   , , , , ,   , , , ,   ,N, , , ,   , , , ,   , ,   , ,   ,   , , , ,   ,M, , ,   S, , ,
Allowed substitution hints:   ( , , )   ( )   ( , , )   ( , , , )   S( , )   ( )   ( )   M( )

Proof of Theorem subfacp1lem5
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 subfacp1lem.a . . . . . . . 8
2 fzfi 11366 . . . . . . . . 9
3 deranglem 25112 . . . . . . . . 9
42, 3ax-mp 5 . . . . . . . 8
51, 4eqeltri 2517 . . . . . . 7
6 subfacp1lem5.b . . . . . . . 8
7 ssrab2 3421 . . . . . . . 8
86, 7eqsstri 3371 . . . . . . 7
9 ssfi 7382 . . . . . . 7
105, 8, 9mp2an 655 . . . . . 6
1110elexi 2978 . . . . 5
1211a1i 11 . . . 4
13 subfacp1lem5.c . . . . . . 7
14 fzfi 11366 . . . . . . . 8
15 deranglem 25112 . . . . . . . 8
1614, 15ax-mp 5 . . . . . . 7
1713, 16eqeltri 2517 . . . . . 6
1817elexi 2978 . . . . 5
1918a1i 11 . . . 4
20 derang.d . . . . . . . . . . . . 13
21 subfac.n . . . . . . . . . . . . 13
22 subfacp1lem1.n . . . . . . . . . . . . 13
23 subfacp1lem1.m . . . . . . . . . . . . 13
24 subfacp1lem1.x . . . . . . . . . . . . 13
25 subfacp1lem1.k . . . . . . . . . . . . 13
26 subfacp1lem5.f . . . . . . . . . . . . 13
27 f1oi 5764 . . . . . . . . . . . . . 14
2827a1i 11 . . . . . . . . . . . . 13
2920, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2a 25126 . . . . . . . . . . . 12
3029simp1d 970 . . . . . . . . . . 11
3130adantr 453 . . . . . . . . . 10
32 simpr 449 . . . . . . . . . . . . . 14
33 fveq1 5778 . . . . . . . . . . . . . . . . 17
3433eqeq1d 2455 . . . . . . . . . . . . . . . 16
35 fveq1 5778 . . . . . . . . . . . . . . . . 17
3635neeq1d 2625 . . . . . . . . . . . . . . . 16
3734, 36anbi12d 693 . . . . . . . . . . . . . . 15
3837, 6elrab2 3107 . . . . . . . . . . . . . 14
3932, 38sylib 190 . . . . . . . . . . . . 13
4039simpld 447 . . . . . . . . . . . 12
41 vex 2972 . . . . . . . . . . . . 13
42 f1oeq1 5716 . . . . . . . . . . . . . 14
43 fveq1 5778 . . . . . . . . . . . . . . . 16
4443neeq1d 2625 . . . . . . . . . . . . . . 15
4544ralbidv 2736 . . . . . . . . . . . . . 14
4642, 45anbi12d 693 . . . . . . . . . . . . 13
4741, 46, 1elab2 3098 . . . . . . . . . . . 12
4840, 47sylib 190 . . . . . . . . . . 11
4948simpld 447 . . . . . . . . . 10
50 f1oco 5749 . . . . . . . . . 10
5131, 49, 50syl2anc 644 . . . . . . . . 9
52 f1of1 5724 . . . . . . . . 9
53 df-f1 5510 . . . . . . . . . 10
5453simprbi 452 . . . . . . . . 9
5551, 52, 543syl 19 . . . . . . . 8
56 f1ofn 5726 . . . . . . . . . . 11
57 fnresdm 5605 . . . . . . . . . . 11
58 f1oeq1 5716 . . . . . . . . . . 11
5951, 56, 57, 584syl 20 . . . . . . . . . 10
6051, 59mpbird 225 . . . . . . . . 9
61 f1ofo 5732 . . . . . . . . 9
6260, 61syl 16 . . . . . . . 8
63 1ex 9141 . . . . . . . . . . 11
6463, 63f1osn 5766 . . . . . . . . . 10
6551, 56syl 16 . . . . . . . . . . . . 13
6622peano2nnd 10072 . . . . . . . . . . . . . . . 16
67 nnuz 10576 . . . . . . . . . . . . . . . 16
6866, 67syl6eleq 2537 . . . . . . . . . . . . . . 15
69 eluzfz1 11119 . . . . . . . . . . . . . . 15
7068, 69syl 16 . . . . . . . . . . . . . 14
7170adantr 453 . . . . . . . . . . . . 13
72 fnressn 5970 . . . . . . . . . . . . 13
7365, 71, 72syl2anc 644 . . . . . . . . . . . 12
74 f1of 5725 . . . . . . . . . . . . . . . . 17
7549, 74syl 16 . . . . . . . . . . . . . . . 16
76 fvco3 5852 . . . . . . . . . . . . . . . 16
7775, 71, 76syl2anc 644 . . . . . . . . . . . . . . 15
7839simprd 451 . . . . . . . . . . . . . . . . 17
7978simpld 447 . . . . . . . . . . . . . . . 16
8079fveq2d 5783 . . . . . . . . . . . . . . 15
8129simp3d 972 . . . . . . . . . . . . . . . 16
8281adantr 453 . . . . . . . . . . . . . . 15
8377, 80, 823eqtrd 2483 . . . . . . . . . . . . . 14
8483opeq2d 4023 . . . . . . . . . . . . 13
8584sneqd 3858 . . . . . . . . . . . 12
8673, 85eqtrd 2479 . . . . . . . . . . 11
87 f1oeq1 5716 . . . . . . . . . . 11
8886, 87syl 16 . . . . . . . . . 10
8964, 88mpbiri 226 . . . . . . . . 9
90 f1ofo 5732 . . . . . . . . 9
9189, 90syl 16 . . . . . . . 8
92 resdif 5747 . . . . . . . 8
9355, 62, 91, 92syl3anc 1185 . . . . . . 7
94 fzsplit 11132 . . . . . . . . . . . 12
9570, 94syl 16 . . . . . . . . . . 11
96 1z 10366 . . . . . . . . . . . . 13
97 fzsn 11149 . . . . . . . . . . . . 13
9896, 97ax-mp 5 . . . . . . . . . . . 12
99 1p1e2 10149 . . . . . . . . . . . . 13
10099oveq1i 6143 . . . . . . . . . . . 12
10198, 100uneq12i 3492 . . . . . . . . . . 11
10295, 101syl6req 2496 . . . . . . . . . 10
10370snssd 3975 . . . . . . . . . . 11
104 incom 3526 . . . . . . . . . . . 12
105 1lt2 10197 . . . . . . . . . . . . . . 15
106 1re 9145 . . . . . . . . . . . . . . . 16
107 2re 10124 . . . . . . . . . . . . . . . 16
108106, 107ltnlei 9249 . . . . . . . . . . . . . . 15
109105, 108mpbi 201 . . . . . . . . . . . . . 14
110 elfzle1 11115 . . . . . . . . . . . . . 14
111109, 110mto 170 . . . . . . . . . . . . 13
112 disjsn 3900 . . . . . . . . . . . . 13
113111, 112mpbir 202 . . . . . . . . . . . 12
114104, 113eqtri 2467 . . . . . . . . . . 11
115 uneqdifeq 3746 . . . . . . . . . . 11
116103, 114, 115sylancl 645 . . . . . . . . . 10
117102, 116mpbid 203 . . . . . . . . 9
118117adantr 453 . . . . . . . 8
119 reseq2 5188 . . . . . . . . . 10
120 f1oeq1 5716 . . . . . . . . . 10
121119, 120syl 16 . . . . . . . . 9
122 f1oeq2 5717 . . . . . . . . 9
123 f1oeq3 5718 . . . . . . . . 9
124121, 122, 1233bitrd 272 . . . . . . . 8
125118, 124syl 16 . . . . . . 7
12693, 125mpbid 203 . . . . . 6
12775adantr 453 . . . . . . . . 9
128 fzp1ss 11153 . . . . . . . . . . . 12
12996, 128ax-mp 5 . . . . . . . . . . 11
130100, 129eqsstr3i 3372 . . . . . . . . . 10
131 simpr 449 . . . . . . . . . 10
132130, 131sseldi 3339 . . . . . . . . 9
133 fvco3 5852 . . . . . . . . 9
134127, 132, 133syl2anc 644 . . . . . . . 8
13520, 21, 1, 22, 23, 24, 25, 6, 26subfacp1lem4 25129 . . . . . . . . . . . 12
136135fveq1d 5781 . . . . . . . . . . 11
137136ad2antrr 708 . . . . . . . . . 10
13878simprd 451 . . . . . . . . . . . . . . 15
139138, 82neeqtrrd 2636 . . . . . . . . . . . . . 14
140139adantr 453 . . . . . . . . . . . . 13
141 fveq2 5779 . . . . . . . . . . . . . 14
142 fveq2 5779 . . . . . . . . . . . . . 14
143141, 142neeq12d 2627 . . . . . . . . . . . . 13
144140, 143syl5ibrcom 215 . . . . . . . . . . . 12
145130sseli 3337 . . . . . . . . . . . . . . . 16
14648simprd 451 . . . . . . . . . . . . . . . . 17
147146r19.21bi 2815 . . . . . . . . . . . . . . . 16
148145, 147sylan2 462 . . . . . . . . . . . . . . 15
149148adantrr 699 . . . . . . . . . . . . . 14
15025eleq2i 2511 . . . . . . . . . . . . . . . . 17
151 eldifsn 3959 . . . . . . . . . . . . . . . . 17
152150, 151bitri 242 . . . . . . . . . . . . . . . 16
15320, 21, 1, 22, 23, 24, 25, 26, 28subfacp1lem2b 25127 . . . . . . . . . . . . . . . . 17
154 fvresi 5976 . . . . . . . . . . . . . . . . . 18
155154adantl 454 . . . . . . . . . . . . . . . . 17
156153, 155eqtrd 2479 . . . . . . . . . . . . . . . 16
157152, 156sylan2br 464 . . . . . . . . . . . . . . 15
158157adantlr 697 . . . . . . . . . . . . . 14
159149, 158neeqtrrd 2636 . . . . . . . . . . . . 13
160159expr 600 . . . . . . . . . . . 12
161144, 160pm2.61dne 2692 . . . . . . . . . . 11
162161necomd 2698 . . . . . . . . . 10
163137, 162eqnetrd 2630 . . . . . . . . 9
16431adantr 453 . . . . . . . . . . 11
165 ffvelrn 5920 . . . . . . . . . . . 12
16675, 145, 165syl2an 465 . . . . . . . . . . 11
167 f1ocnvfv 6068 . . . . . . . . . . 11
168164, 166, 167syl2anc 644 . . . . . . . . . 10
169168necon3d 2650 . . . . . . . . 9
170163, 169mpd 15 . . . . . . . 8
171134, 170eqnetrd 2630 . . . . . . 7
172171ralrimiva 2800 . . . . . 6
173 f1of 5725 . . . . . . . . . . . . 13
17427, 173ax-mp 5 . . . . . . . . . . . 12
175 difexg 4394 . . . . . . . . . . . . . 14
17614, 175ax-mp 5 . . . . . . . . . . . . 13
17725, 176eqeltri 2517 . . . . . . . . . . . 12
178 fex 6021 . . . . . . . . . . . 12
179174, 177, 178mp2an 655 . . . . . . . . . . 11
180 prex 4449 . . . . . . . . . . 11
181179, 180unex 4752 . . . . . . . . . 10
18226, 181eqeltri 2517 . . . . . . . . 9
183182, 41coex 5463 . . . . . . . 8
184183resex 5234 . . . . . . 7
185 f1oeq1 5716 . . . . . . . 8
186 fveq1 5778 . . . . . . . . . . 11
187 fvres 5792 . . . . . . . . . . 11
188186, 187sylan9eq 2499 . . . . . . . . . 10
189188neeq1d 2625 . . . . . . . . 9
190189ralbidva 2732 . . . . . . . 8
191185, 190anbi12d 693 . . . . . . 7
192184, 191, 13elab2 3098 . . . . . 6
193126, 172, 192sylanbrc 647 . . . . 5
194193ex 425 . . . 4
19530adantr 453 . . . . . . . 8
196 simpr 449 . . . . . . . . . . . 12
197 vex 2972 . . . . . . . . . . . . 13
198 f1oeq1 5716 . . . . . . . . . . . . . 14
199 fveq1 5778 . . . . . . . . . . . . . . . 16
200199neeq1d 2625 . . . . . . . . . . . . . . 15
201200ralbidv 2736 . . . . . . . . . . . . . 14
202198, 201anbi12d 693 . . . . . . . . . . . . 13