Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  hashf1lem1 Unicode version

Theorem hashf1lem1 11393
 Description: Lemma for hashf1 11395. (Contributed by Mario Carneiro, 17-Apr-2015.)
Hypotheses
Ref Expression
hashf1lem2.1
hashf1lem2.2
hashf1lem2.3
hashf1lem2.4
hashf1lem1.5
Assertion
Ref Expression
hashf1lem1
Distinct variable groups:   ,   ,   ,   ,   ,
Allowed substitution hints:   ()   ()   ()   ()

Proof of Theorem hashf1lem1
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 f1f 5437 . . . . . 6
21adantl 452 . . . . 5
3 hashf1lem2.2 . . . . . 6
4 hashf1lem2.1 . . . . . . 7
5 snfi 6941 . . . . . . 7
6 unfi 7124 . . . . . . 7
74, 5, 6sylancl 643 . . . . . 6
8 elmapg 6785 . . . . . 6
93, 7, 8syl2anc 642 . . . . 5
102, 9syl5ibr 212 . . . 4
1110abssdv 3247 . . 3
12 ovex 5883 . . 3
13 ssexg 4160 . . 3
1411, 12, 13sylancl 643 . 2
15 difexg 4162 . . 3
163, 15syl 15 . 2
17 vex 2791 . . . 4
18 reseq1 4949 . . . . . 6
1918eqeq1d 2291 . . . . 5
20 f1eq1 5432 . . . . 5
2119, 20anbi12d 691 . . . 4
2217, 21elab 2914 . . 3
23 f1f 5437 . . . . . . 7
2423ad2antll 709 . . . . . 6
25 ssun2 3339 . . . . . . 7
26 vex 2791 . . . . . . . 8
2726snss 3748 . . . . . . 7
2825, 27mpbir 200 . . . . . 6
29 ffvelrn 5663 . . . . . 6
3024, 28, 29sylancl 643 . . . . 5
31 hashf1lem2.3 . . . . . . 7
3231adantr 451 . . . . . 6
33 df-ima 4702 . . . . . . . . 9
34 simprl 732 . . . . . . . . . 10
3534rneqd 4906 . . . . . . . . 9
3633, 35syl5eq 2327 . . . . . . . 8
3736eleq2d 2350 . . . . . . 7
38 simprr 733 . . . . . . . 8
3928a1i 10 . . . . . . . 8
40 ssun1 3338 . . . . . . . . 9
4140a1i 10 . . . . . . . 8
42 f1elima 5787 . . . . . . . 8
4338, 39, 41, 42syl3anc 1182 . . . . . . 7
4437, 43bitr3d 246 . . . . . 6
4532, 44mtbird 292 . . . . 5
46 eldif 3162 . . . . 5
4730, 45, 46sylanbrc 645 . . . 4
4847ex 423 . . 3
4922, 48syl5bi 208 . 2
50 hashf1lem1.5 . . . . . . 7
51 f1f 5437 . . . . . . 7
5250, 51syl 15 . . . . . 6
5352adantr 451 . . . . 5
54 vex 2791 . . . . . . . 8
5526, 54f1osn 5513 . . . . . . 7
56 f1of 5472 . . . . . . 7
5755, 56ax-mp 8 . . . . . 6
58 eldifi 3298 . . . . . . . 8
5958adantl 452 . . . . . . 7
6059snssd 3760 . . . . . 6
61 fss 5397 . . . . . 6
6257, 60, 61sylancr 644 . . . . 5
63 res0 4959 . . . . . . 7
64 res0 4959 . . . . . . 7
6563, 64eqtr4i 2306 . . . . . 6
66 disjsn 3693 . . . . . . . . 9
6731, 66sylibr 203 . . . . . . . 8
6867adantr 451 . . . . . . 7
6968reseq2d 4955 . . . . . 6
7068reseq2d 4955 . . . . . 6
7165, 69, 703eqtr4a 2341 . . . . 5
72 fresaunres1 5414 . . . . 5
7353, 62, 71, 72syl3anc 1182 . . . 4
74 f1f1orn 5483 . . . . . . . . 9
7550, 74syl 15 . . . . . . . 8
7675adantr 451 . . . . . . 7
7755a1i 10 . . . . . . 7
78 eldifn 3299 . . . . . . . . 9
7978adantl 452 . . . . . . . 8
80 disjsn 3693 . . . . . . . 8
8179, 80sylibr 203 . . . . . . 7
82 f1oun 5492 . . . . . . 7
8376, 77, 68, 81, 82syl22anc 1183 . . . . . 6
84 f1of1 5471 . . . . . 6
8583, 84syl 15 . . . . 5
86 frn 5395 . . . . . . 7
8753, 86syl 15 . . . . . 6
8887, 60unssd 3351 . . . . 5
89 f1ss 5442 . . . . 5
9085, 88, 89syl2anc 642 . . . 4
91 fex 5749 . . . . . . . 8
9252, 4, 91syl2anc 642 . . . . . . 7
9392adantr 451 . . . . . 6
94 snex 4216 . . . . . 6
95 unexg 4521 . . . . . 6
9693, 94, 95sylancl 643 . . . . 5
97 reseq1 4949 . . . . . . . 8
9897eqeq1d 2291 . . . . . . 7
99 f1eq1 5432 . . . . . . 7
10098, 99anbi12d 691 . . . . . 6
101100elabg 2915 . . . . 5
10296, 101syl 15 . . . 4
10373, 90, 102mpbir2and 888 . . 3
104103ex 423 . 2
10522anbi1i 676 . . 3
106 simprlr 739 . . . . . . 7
107 f1fn 5438 . . . . . . 7
108106, 107syl 15 . . . . . 6
10983adantrl 696 . . . . . . 7
110 f1ofn 5473 . . . . . . 7
111109, 110syl 15 . . . . . 6
112 eqfnfv 5622 . . . . . 6
113108, 111, 112syl2anc 642 . . . . 5
114 fvres 5542 . . . . . . . . . . 11
115114eqcomd 2288 . . . . . . . . . 10
116 simprll 738 . . . . . . . . . . 11
117116fveq1d 5527 . . . . . . . . . 10
118115, 117sylan9eqr 2337 . . . . . . . . 9
11950ad2antrr 706 . . . . . . . . . . 11
120 f1fn 5438 . . . . . . . . . . 11
121119, 120syl 15 . . . . . . . . . 10
12226, 54fnsn 5304 . . . . . . . . . . 11
123122a1i 10 . . . . . . . . . 10
12467ad2antrr 706 . . . . . . . . . 10
125 simpr 447 . . . . . . . . . 10
126 fvun1 5590 . . . . . . . . . 10
127121, 123, 124, 125, 126syl112anc 1186 . . . . . . . . 9
128118, 127eqtr4d 2318 . . . . . . . 8
129128ralrimiva 2626 . . . . . . 7
130129biantrurd 494 . . . . . 6
131 ralunb 3356 . . . . . 6
132130, 131syl6bbr 254 . . . . 5
13326a1i 10 . . . . . . . 8
13454a1i 10 . . . . . . . 8
135 fdm 5393 . . . . . . . . . . . 12
13652, 135syl 15 . . . . . . . . . . 11
137136eleq2d 2350 . . . . . . . . . 10
13831, 137mtbird 292 . . . . . . . . 9
139138adantr 451 . . . . . . . 8
140 fsnunfv 5720 . . . . . . . 8
141133, 134, 139, 140syl3anc 1182 . . . . . . 7
142141eqeq2d 2294 . . . . . 6
143 fveq2 5525 . . . . . . . 8
144 fveq2 5525 . . . . . . . 8
145143, 144eqeq12d 2297 . . . . . . 7
14626, 145ralsn 3674 . . . . . 6
147 eqcom 2285 . . . . . 6
148142, 146, 1473bitr4g 279 . . . . 5
149113, 132, 1483bitr2d 272 . . . 4
150149ex 423 . . 3
151105, 150syl5bi 208 . 2
15214, 16, 49, 104, 151en3d 6898 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wa 358   wceq 1623   wcel 1684  cab 2269  wral 2543  cvv 2788   cdif 3149   cun 3150   cin 3151   wss 3152  c0 3455  csn 3640  cop 3643   class class class wbr 4023   cdm 4689   crn 4690   cres 4691  cima 4692   wfn 5250  wf 5251  wf1 5252  wf1o 5254  cfv 5255  (class class class)co 5858   cmap 6772   cen 6860  cfn 6863  c1 8738   caddc 8740   cle 8868  chash 11337 This theorem is referenced by:  hashf1lem2  11394 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-recs 6388  df-rdg 6423  df-1o 6479  df-oadd 6483  df-er 6660  df-map 6774  df-en 6864  df-fin 6867
 Copyright terms: Public domain W3C validator