Mathbox for Mario Carneiro < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  subfacp1lem3 Structured version   Unicode version

Theorem subfacp1lem3 24868
 Description: Lemma for subfacp1 24872. In subfacp1lem6 24871 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 that satisfy this for fixed is in bijection with derangements, by simply dropping the and points from the function to get a derangement on . (Contributed by Mario Carneiro, 23-Jan-2015.)
Hypotheses
Ref Expression
derang.d
subfac.n
subfacp1lem.a
subfacp1lem1.n
subfacp1lem1.m
subfacp1lem1.x
subfacp1lem1.k
subfacp1lem3.b
subfacp1lem3.c
Assertion
Ref Expression
subfacp1lem3
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,   ,,   ,,   ,   ,,,,   ,,,,   ,,,
Allowed substitution hints:   (,,)   ()   (,,)   (,,,)   (,)   ()   ()

Proof of Theorem subfacp1lem3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 subfacp1lem.a . . . . . . . 8
2 fzfi 11311 . . . . . . . . 9
3 deranglem 24852 . . . . . . . . 9
42, 3ax-mp 8 . . . . . . . 8
51, 4eqeltri 2506 . . . . . . 7
6 subfacp1lem3.b . . . . . . . 8
7 ssrab2 3428 . . . . . . . 8
86, 7eqsstri 3378 . . . . . . 7
9 ssfi 7329 . . . . . . 7
105, 8, 9mp2an 654 . . . . . 6
1110elexi 2965 . . . . 5
1211a1i 11 . . . 4
13 subfacp1lem3.c . . . . . . 7
14 subfacp1lem1.k . . . . . . . . 9
15 fzfi 11311 . . . . . . . . . 10
16 diffi 7339 . . . . . . . . . 10
1715, 16ax-mp 8 . . . . . . . . 9
1814, 17eqeltri 2506 . . . . . . . 8
19 deranglem 24852 . . . . . . . 8
2018, 19ax-mp 8 . . . . . . 7
2113, 20eqeltri 2506 . . . . . 6
2221elexi 2965 . . . . 5
2322a1i 11 . . . 4
24 simpr 448 . . . . . . . . . . . . 13
25 fveq1 5727 . . . . . . . . . . . . . . . 16
2625eqeq1d 2444 . . . . . . . . . . . . . . 15
27 fveq1 5727 . . . . . . . . . . . . . . . 16
2827eqeq1d 2444 . . . . . . . . . . . . . . 15
2926, 28anbi12d 692 . . . . . . . . . . . . . 14
3029, 6elrab2 3094 . . . . . . . . . . . . 13
3124, 30sylib 189 . . . . . . . . . . . 12
3231simpld 446 . . . . . . . . . . 11
33 vex 2959 . . . . . . . . . . . 12
34 f1oeq1 5665 . . . . . . . . . . . . 13
35 fveq1 5727 . . . . . . . . . . . . . . 15
3635neeq1d 2614 . . . . . . . . . . . . . 14
3736ralbidv 2725 . . . . . . . . . . . . 13
3834, 37anbi12d 692 . . . . . . . . . . . 12
3933, 38, 1elab2 3085 . . . . . . . . . . 11
4032, 39sylib 189 . . . . . . . . . 10
4140simpld 446 . . . . . . . . 9
42 f1of1 5673 . . . . . . . . 9
43 df-f1 5459 . . . . . . . . . 10
4443simprbi 451 . . . . . . . . 9
4541, 42, 443syl 19 . . . . . . . 8
46 f1ofn 5675 . . . . . . . . . . . 12
4741, 46syl 16 . . . . . . . . . . 11
48 fnresdm 5554 . . . . . . . . . . 11
49 f1oeq1 5665 . . . . . . . . . . 11
5047, 48, 493syl 19 . . . . . . . . . 10
5141, 50mpbird 224 . . . . . . . . 9
52 f1ofo 5681 . . . . . . . . 9
5351, 52syl 16 . . . . . . . 8
54 ssun2 3511 . . . . . . . . . . . . 13
55 derang.d . . . . . . . . . . . . . . 15
56 subfac.n . . . . . . . . . . . . . . 15
57 subfacp1lem1.n . . . . . . . . . . . . . . 15
58 subfacp1lem1.m . . . . . . . . . . . . . . 15
59 subfacp1lem1.x . . . . . . . . . . . . . . 15
6055, 56, 1, 57, 58, 59, 14subfacp1lem1 24865 . . . . . . . . . . . . . 14
6160simp2d 970 . . . . . . . . . . . . 13
6254, 61syl5sseq 3396 . . . . . . . . . . . 12
6362adantr 452 . . . . . . . . . . 11
64 fnssres 5558 . . . . . . . . . . 11
6547, 63, 64syl2anc 643 . . . . . . . . . 10
6631simprd 450 . . . . . . . . . . . . . 14
6766simpld 446 . . . . . . . . . . . . 13
6859prid2 3913 . . . . . . . . . . . . 13
6967, 68syl6eqel 2524 . . . . . . . . . . . 12
7066simprd 450 . . . . . . . . . . . . 13
71 1ex 9086 . . . . . . . . . . . . . 14
7271prid1 3912 . . . . . . . . . . . . 13
7370, 72syl6eqel 2524 . . . . . . . . . . . 12
74 fveq2 5728 . . . . . . . . . . . . . 14
7574eleq1d 2502 . . . . . . . . . . . . 13
76 fveq2 5728 . . . . . . . . . . . . . 14
7776eleq1d 2502 . . . . . . . . . . . . 13
7871, 59, 75, 77ralpr 3861 . . . . . . . . . . . 12
7969, 73, 78sylanbrc 646 . . . . . . . . . . 11
80 fvres 5745 . . . . . . . . . . . . 13
8180eleq1d 2502 . . . . . . . . . . . 12
8281ralbiia 2737 . . . . . . . . . . 11
8379, 82sylibr 204 . . . . . . . . . 10
84 ffnfv 5894 . . . . . . . . . 10
8565, 83, 84sylanbrc 646 . . . . . . . . 9
86 fveq2 5728 . . . . . . . . . . . . . 14
8786eqeq1d 2444 . . . . . . . . . . . . 13
8887rspcev 3052 . . . . . . . . . . . 12
8968, 70, 88sylancr 645 . . . . . . . . . . 11
90 fveq2 5728 . . . . . . . . . . . . . 14
9190eqeq1d 2444 . . . . . . . . . . . . 13
9291rspcev 3052 . . . . . . . . . . . 12
9372, 67, 92sylancr 645 . . . . . . . . . . 11
94 eqeq2 2445 . . . . . . . . . . . . 13
9594rexbidv 2726 . . . . . . . . . . . 12
96 eqeq2 2445 . . . . . . . . . . . . 13
9796rexbidv 2726 . . . . . . . . . . . 12
9871, 59, 95, 97ralpr 3861 . . . . . . . . . . 11
9989, 93, 98sylanbrc 646 . . . . . . . . . 10
100 eqcom 2438 . . . . . . . . . . . . 13
101 fvres 5745 . . . . . . . . . . . . . 14
102101eqeq1d 2444 . . . . . . . . . . . . 13
103100, 102syl5bb 249 . . . . . . . . . . . 12
104103rexbiia 2738 . . . . . . . . . . 11
105104ralbii 2729 . . . . . . . . . 10
10699, 105sylibr 204 . . . . . . . . 9
107 dffo3 5884 . . . . . . . . 9
10885, 106, 107sylanbrc 646 . . . . . . . 8
109 resdif 5696 . . . . . . . 8
11045, 53, 108, 109syl3anc 1184 . . . . . . 7
111 uncom 3491 . . . . . . . . . . 11
112111, 61syl5eq 2480 . . . . . . . . . 10
113 incom 3533 . . . . . . . . . . . 12
11460simp1d 969 . . . . . . . . . . . 12
115113, 114syl5eq 2480 . . . . . . . . . . 11
116 uneqdifeq 3716 . . . . . . . . . . 11
11762, 115, 116syl2anc 643 . . . . . . . . . 10
118112, 117mpbid 202 . . . . . . . . 9
119118adantr 452 . . . . . . . 8
120 reseq2 5141 . . . . . . . . . 10
121 f1oeq1 5665 . . . . . . . . . 10
122120, 121syl 16 . . . . . . . . 9
123 f1oeq2 5666 . . . . . . . . 9
124 f1oeq3 5667 . . . . . . . . 9
125122, 123, 1243bitrd 271 . . . . . . . 8
126119, 125syl 16 . . . . . . 7
127110, 126mpbid 202 . . . . . 6
128 ssun1 3510 . . . . . . . . 9
129128, 61syl5sseq 3396 . . . . . . . 8
130129adantr 452 . . . . . . 7
13140simprd 450 . . . . . . 7
132 ssralv 3407 . . . . . . 7
133130, 131, 132sylc 58 . . . . . 6
13433resex 5186 . . . . . . 7
135 f1oeq1 5665 . . . . . . . 8
136 fveq1 5727 . . . . . . . . . . 11
137 fvres 5745 . . . . . . . . . . 11
138136, 137sylan9eq 2488 . . . . . . . . . 10
139138neeq1d 2614 . . . . . . . . 9
140139ralbidva 2721 . . . . . . . 8
141135, 140anbi12d 692 . . . . . . 7
142134, 141, 13elab2 3085 . . . . . 6
143127, 133, 142sylanbrc 646 . . . . 5
144143ex 424 . . . 4
14557adantr 452 . . . . . . . . 9
14658adantr 452 . . . . . . . . 9
147 eqid 2436 . . . . . . . . 9
148 simpr 448 . . . . . . . . . . 11
149 vex 2959 . . . . . . . . . . . 12
150 f1oeq1 5665 . . . . . . . . . . . . 13
151 fveq1 5727 . . . . . . . . . . . . . . 15
152151neeq1d 2614 . . . . . . . . . . . . . 14
153152ralbidv 2725 . . . . . . . . . . . . 13
154150, 153anbi12d 692 . . . . . . . . . . . 12
155149, 154, 13elab2 3085 . . . . . . . . . . 11
156148, 155sylib 189 . . . . . . . . . 10
157156simpld 446 . . . . . . . . 9
15855, 56, 1, 145, 146, 59, 14, 147, 157subfacp1lem2a 24866 . . . . . . . 8
159158simp1d 969 . . . . . . 7
16055, 56, 1, 145, 146, 59, 14, 147, 157subfacp1lem2b 24867 . . . . . . . . . . 11
161156simprd 450 . . . . . . . . . . . 12
162161r19.21bi 2804 . . . . . . . . . . 11
163160, 162eqnetrd 2619 . . . . . . . . . 10
164163ralrimiva 2789 . . . . . . . . 9
165158simp2d 970 . . . . . . . . . . 11
166 elfzuz 11055 . . . . . . . . . . . . 13
167 eluz2b3 10549 . . . . . . . . . . . . . 14
168167simprbi 451 . . . . . . . . . . . . 13
16958, 166, 1683syl 19 . . . . . . . . . . . 12
170169adantr 452 . . . . . . . . . . 11
171165, 170eqnetrd 2619 . . . . . . . . . 10
172158simp3d 971 . . . . . . . . . . 11
173170necomd 2687 . . . . . . . . . . 11
174172, 173eqnetrd 2619 . . . . . . . . . 10
175 fveq2 5728 . . . . . . . . . . . 12
176 id 20 . . . . . . . . . . . 12
177175, 176neeq12d 2616 . . . . . . . . . . 11
178 fveq2 5728 . . . . . . . . . . . 12
179 id 20 . . . . . . . . . . . 12
180178, 179neeq12d 2616 . . . . . . . . . . 11
18171, 59, 177, 180ralpr 3861 . . . . . . . . . 10
182171, 174, 181sylanbrc 646 . . . . . . . . 9
183 ralunb 3528 . . . . . . . . 9
184164, 182, 183sylanbrc 646 . . . . . . . 8
18561adantr 452 . . . . . . . . 9
186185raleqdv 2910 . . . . . . . 8
187184, 186mpbid 202 . . . . . . 7
188 prex 4406 . . . . . . . . 9
189149, 188unex 4707 . . . . . . . 8
190 f1oeq1 5665 . . . . . . . . 9
191 fveq1 5727 . . . . . . . . . . 11
192191neeq1d 2614 . . . . . . . . . 10
193192ralbidv 2725 . . . . . . . . 9
194190, 193anbi12d 692 . . . . . . . 8
195189, 194, 1elab2 3085 . . . . . . 7
196159, 187, 195sylanbrc 646 . . . . . 6
197165, 172jca 519 . . . . . 6
198 fveq1 5727 . . . . . . . . 9
199198eqeq1d 2444 . . . . . . . 8
200 fveq1 5727 . . . . . . . . 9
201200eqeq1d 2444 . . . . . . . 8
202199, 201anbi12d 692 . . . . . . 7
203202, 6elrab2 3094 . . . . . 6
204196, 197, 203sylanbrc 646 . . . . 5
205204ex 424 . . . 4
20667adantrr 698 . . . . . . . . . . . 12
207165adantrl 697 . . . . . . . . . . . 12
208206, 207eqtr4d 2471 . . . . . . . . . . 11
20970adantrr 698 . . . . . . . . . . . 12
210172adantrl 697 . . . . . . . . . . . 12
211209, 210eqtr4d 2471 . . . . . . . . . . 11
21290, 175eqeq12d 2450 . . . . . . . . . . . 12
21386, 178eqeq12d 2450 . . . . . . . . . . . 12
21471, 59, 212, 213ralpr 3861 . . . . . . . . . . 11
215208, 211, 214sylanbrc 646 . . . . . . . . . 10
216215biantrud 494 . . . . . . . . 9
217 ralunb 3528 . . . . . . . . 9
218216, 217syl6bbr 255 . . . . . . . 8
219160eqeq2d 2447 . . . . . . . . . 10
220219ralbidva 2721 . . . . . . . . 9
221220adantrl 697 . . . . . . . 8
22261adantr 452 . . . . . . . . 9
223222raleqdv 2910 . . . . . . . 8
224218, 221, 2233bitr3rd 276 . . . . . . 7
225137eqeq2d 2447 . . . . . . . . 9
226 eqcom 2438 . . . . . . . . 9
227225, 226syl6bb 253 . . . . . . . 8
228227ralbiia 2737 . . . . . . 7
229224, 228syl6bbr 255 . . . . . 6
23047adantrr 698 . . . . . . 7
231159adantrl 697 . . . . . . . 8
232 f1ofn 5675 . . . . . . . 8
233231, 232syl 16 . . . . . . 7
234 eqfnfv 5827 . . . . . . 7
235230, 233, 234syl2anc 643 . . . . . 6
236157adantrl 697 . . . . . . . 8
237 f1ofn 5675 . . . . . . . 8
238236, 237syl 16 . . . . . . 7
239129adantr 452 . . . . . . . 8
240 fnssres 5558 . . . . . . . 8
241230, 239, 240syl2anc 643 . . . . . . 7
242 eqfnfv 5827 . . . . . . 7
243238, 241, 242syl2anc 643 . . . . . 6
244229, 235, 2433bitr4d 277 . . . . 5
245244ex 424 . . . 4
24612, 23, 144, 205, 245en3d 7144 . . 3
247 hashen 11631 . . . 4
24810, 21, 247mp2an 654 . . 3
249246, 248sylibr 204 . 2
25013fveq2i 5731 . . . 4
25155derangval 24853 . . . . 5
25218, 251ax-mp 8 . . . 4
25355, 56derangen2 24860 . . . . 5
25418, 253ax-mp 8 . . . 4
255250, 252, 2543eqtr2ri 2463 . . 3
25660simp3d 971 . . . 4
257256fveq2d 5732 . . 3
258255, 257syl5eqr 2482 . 2
259249, 258eqtrd 2468 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 177   wa 359   wceq 1652   wcel 1725  cab 2422   wne 2599  wral 2705  wrex 2706  crab 2709  cvv 2956   cdif 3317   cun 3318   cin 3319   wss 3320  c0 3628  csn 3814  cpr 3815  cop 3817   class class class wbr 4212   cmpt 4266  ccnv 4877   cres 4880   wfun 5448   wfn 5449  wf 5450  wf1 5451  wfo 5452  wf1o 5453  cfv 5454  (class class class)co 6081   cen 7106  cfn 7109  c1 8991   caddc 8993   cmin 9291  cn 10000  c2 10049  cn0 10221  cuz 10488  cfz 11043  chash 11618 This theorem is referenced by:  subfacp1lem6  24871 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-rep 4320  ax-sep 4330  ax-nul 4338  ax-pow 4377  ax-pr 4403  ax-un 4701  ax-cnex 9046  ax-resscn 9047  ax-1cn 9048  ax-icn 9049  ax-addcl 9050  ax-addrcl 9051  ax-mulcl 9052  ax-mulrcl 9053  ax-mulcom 9054  ax-addass 9055  ax-mulass 9056  ax-distr 9057  ax-i2m1 9058  ax-1ne0 9059  ax-1rid 9060  ax-rnegex 9061  ax-rrecex 9062  ax-cnre 9063  ax-pre-lttri 9064  ax-pre-lttrn 9065  ax-pre-ltadd 9066  ax-pre-mulgt0 9067 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2285  df-mo 2286  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-nel 2602  df-ral 2710  df-rex 2711  df-reu 2712  df-rmo 2713  df-rab 2714  df-v 2958  df-sbc 3162  df-csb 3252  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-pss 3336  df-nul 3629  df-if 3740  df-pw 3801  df-sn 3820  df-pr 3821  df-tp 3822  df-op 3823  df-uni 4016  df-int 4051  df-iun 4095  df-br 4213  df-opab 4267  df-mpt 4268  df-tr 4303  df-eprel 4494  df-id 4498  df-po 4503  df-so 4504  df-fr 4541  df-we 4543  df-ord 4584  df-on 4585  df-lim 4586  df-suc 4587  df-om 4846  df-xp 4884  df-rel 4885  df-cnv 4886  df-co 4887  df-dm 4888  df-rn 4889  df-res 4890  df-ima 4891  df-iota 5418  df-fun 5456  df-fn 5457  df-f 5458  df-f1 5459  df-fo 5460  df-f1o 5461  df-fv 5462  df-ov 6084  df-oprab 6085  df-mpt2 6086  df-1st 6349  df-2nd 6350  df-riota 6549  df-recs 6633  df-rdg 6668  df-1o 6724  df-2o 6725  df-oadd 6728  df-er 6905  df-map 7020  df-pm 7021  df-en 7110  df-dom 7111  df-sdom 7112  df-fin 7113  df-card 7826  df-cda 8048  df-pnf 9122  df-mnf 9123  df-xr 9124  df-ltxr 9125  df-le 9126  df-sub 9293  df-neg 9294  df-nn 10001  df-2 10058  df-n0 10222  df-z 10283  df-uz 10489  df-fz 11044  df-hash 11619
 Copyright terms: Public domain W3C validator