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

Theorem hashf1lem2 12505
Description: Lemma for hashf1 12506. (Contributed by Mario Carneiro, 17-Apr-2015.)
Hypotheses
Ref Expression
hashf1lem2.1
hashf1lem2.2
hashf1lem2.3
hashf1lem2.4
Assertion
Ref Expression
hashf1lem2
Distinct variable groups:   ,   ,   ,   ,

Proof of Theorem hashf1lem2
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssid 3522 . 2
2 hashf1lem2.2 . . . . 5
3 hashf1lem2.1 . . . . 5
4 mapfi 7836 . . . . 5
52, 3, 4syl2anc 661 . . . 4
6 f1f 5786 . . . . . 6
72, 3elmapd 7453 . . . . . 6
86, 7syl5ibr 221 . . . . 5
98abssdv 3573 . . . 4
10 ssfi 7760 . . . 4
115, 9, 10syl2anc 661 . . 3
12 sseq1 3524 . . . . . 6
13 eleq2 2530 . . . . . . . . . . . . 13
14 noel 3788 . . . . . . . . . . . . . 14
1514pm2.21i 131 . . . . . . . . . . . . 13
1613, 15syl6bi 228 . . . . . . . . . . . 12
1716adantrd 468 . . . . . . . . . . 11
1817abssdv 3573 . . . . . . . . . 10
19 ss0 3816 . . . . . . . . . 10
2018, 19syl 16 . . . . . . . . 9
2120fveq2d 5875 . . . . . . . 8
22 hash0 12437 . . . . . . . 8
2321, 22syl6eq 2514 . . . . . . 7
24 fveq2 5871 . . . . . . . . 9
2524, 22syl6eq 2514 . . . . . . . 8
2625oveq2d 6312 . . . . . . 7
2723, 26eqeq12d 2479 . . . . . 6
2812, 27imbi12d 320 . . . . 5
2928imbi2d 316 . . . 4
30 sseq1 3524 . . . . . 6
31 eleq2 2530 . . . . . . . . . 10
3231anbi1d 704 . . . . . . . . 9
3332abbidv 2593 . . . . . . . 8
3433fveq2d 5875 . . . . . . 7
35 fveq2 5871 . . . . . . . 8
3635oveq2d 6312 . . . . . . 7
3734, 36eqeq12d 2479 . . . . . 6
3830, 37imbi12d 320 . . . . 5
3938imbi2d 316 . . . 4
40 sseq1 3524 . . . . . 6
41 eleq2 2530 . . . . . . . . . 10
4241anbi1d 704 . . . . . . . . 9
4342abbidv 2593 . . . . . . . 8
4443fveq2d 5875 . . . . . . 7
45 fveq2 5871 . . . . . . . 8
4645oveq2d 6312 . . . . . . 7
4744, 46eqeq12d 2479 . . . . . 6
4840, 47imbi12d 320 . . . . 5
4948imbi2d 316 . . . 4
50 sseq1 3524 . . . . . 6
51 f1eq1 5781 . . . . . . . . . . 11
5251cbvabv 2600 . . . . . . . . . 10
5352eqeq2i 2475 . . . . . . . . 9
54 ssun1 3666 . . . . . . . . . . . . . . 15
55 f1ssres 5793 . . . . . . . . . . . . . . 15
5654, 55mpan2 671 . . . . . . . . . . . . . 14
57 vex 3112 . . . . . . . . . . . . . . . 16
5857resex 5322 . . . . . . . . . . . . . . 15
59 f1eq1 5781 . . . . . . . . . . . . . . 15
6058, 59elab 3246 . . . . . . . . . . . . . 14
6156, 60sylibr 212 . . . . . . . . . . . . 13
62 eleq2 2530 . . . . . . . . . . . . 13
6361, 62syl5ibr 221 . . . . . . . . . . . 12
6463pm4.71rd 635 . . . . . . . . . . 11
6564bicomd 201 . . . . . . . . . 10
6665abbidv 2593 . . . . . . . . 9
6753, 66sylbi 195 . . . . . . . 8
6867fveq2d 5875 . . . . . . 7
69 fveq2 5871 . . . . . . . 8
7069oveq2d 6312 . . . . . . 7
7168, 70eqeq12d 2479 . . . . . 6
7250, 71imbi12d 320 . . . . 5
7372imbi2d 316 . . . 4
74 hashcl 12428 . . . . . . . . . 10
752, 74syl 16 . . . . . . . . 9
7675nn0cnd 10879 . . . . . . . 8
77 hashcl 12428 . . . . . . . . . 10
783, 77syl 16 . . . . . . . . 9
7978nn0cnd 10879 . . . . . . . 8
8076, 79subcld 9954 . . . . . . 7
8180mul01d 9800 . . . . . 6
8281eqcomd 2465 . . . . 5
8382a1d 25 . . . 4
84 ssun1 3666 . . . . . . . . 9
85 sstr 3511 . . . . . . . . 9
8684, 85mpan 670 . . . . . . . 8
8786imim1i 58 . . . . . . 7
88 oveq1 6303 . . . . . . . . . 10
89 elun 3644 . . . . . . . . . . . . . . . . . . 19
9058elsnc 4053 . . . . . . . . . . . . . . . . . . . 20
9190orbi2i 519 . . . . . . . . . . . . . . . . . . 19
9289, 91bitri 249 . . . . . . . . . . . . . . . . . 18
9392anbi1i 695 . . . . . . . . . . . . . . . . 17
94 andir 868 . . . . . . . . . . . . . . . . 17
9593, 94bitri 249 . . . . . . . . . . . . . . . 16
9695abbii 2591 . . . . . . . . . . . . . . 15
97 unab 3764 . . . . . . . . . . . . . . 15
9896, 97eqtr4i 2489 . . . . . . . . . . . . . 14
9998fveq2i 5874 . . . . . . . . . . . . 13
100 snfi 7616 . . . . . . . . . . . . . . . . . . 19
101 unfi 7807 . . . . . . . . . . . . . . . . . . 19
1023, 100, 101sylancl 662 . . . . . . . . . . . . . . . . . 18
103 mapvalg 7449 . . . . . . . . . . . . . . . . . 18
1042, 102, 103syl2anc 661 . . . . . . . . . . . . . . . . 17
105 mapfi 7836 . . . . . . . . . . . . . . . . . 18
1062, 102, 105syl2anc 661 . . . . . . . . . . . . . . . . 17
107104, 106eqeltrrd 2546 . . . . . . . . . . . . . . . 16
108 f1f 5786 . . . . . . . . . . . . . . . . . 18
109108adantl 466 . . . . . . . . . . . . . . . . 17
110109ss2abi 3571 . . . . . . . . . . . . . . . 16
111 ssfi 7760 . . . . . . . . . . . . . . . 16
112107, 110, 111sylancl 662 . . . . . . . . . . . . . . 15
113112adantr 465 . . . . . . . . . . . . . 14
114108adantl 466 . . . . . . . . . . . . . . . . 17
115114ss2abi 3571 . . . . . . . . . . . . . . . 16
116 ssfi 7760 . . . . . . . . . . . . . . . 16
117107, 115, 116sylancl 662 . . . . . . . . . . . . . . 15
118117adantr 465 . . . . . . . . . . . . . 14
119 inab 3765 . . . . . . . . . . . . . . 15
120 simprlr 764 . . . . . . . . . . . . . . . 16
121 abn0 3804 . . . . . . . . . . . . . . . . . 18
122 simprl 756 . . . . . . . . . . . . . . . . . . . 20
123 simpll 753 . . . . . . . . . . . . . . . . . . . 20
124122, 123eqeltrrd 2546 . . . . . . . . . . . . . . . . . . 19
125124exlimiv 1722 . . . . . . . . . . . . . . . . . 18
126121, 125sylbi 195 . . . . . . . . . . . . . . . . 17
127126necon1bi 2690 . . . . . . . . . . . . . . . 16
128120, 127syl 16 . . . . . . . . . . . . . . 15
129119, 128syl5eq 2510 . . . . . . . . . . . . . 14
130 hashun 12450 . . . . . . . . . . . . . 14
131113, 118, 129, 130syl3anc 1228 . . . . . . . . . . . . 13
13299, 131syl5eq 2510 . . . . . . . . . . . 12
133 simpr 461 . . . . . . . . . . . . . . . . 17
134133unssbd 3681 . . . . . . . . . . . . . . . 16
135 vex 3112 . . . . . . . . . . . . . . . . 17
136135snss 4154 . . . . . . . . . . . . . . . 16
137134, 136sylibr 212 . . . . . . . . . . . . . . 15
138 f1eq1 5781 . . . . . . . . . . . . . . . 16
139135, 138elab 3246 . . . . . . . . . . . . . . 15
140137, 139sylib 196 . . . . . . . . . . . . . 14
14179adantr 465 . . . . . . . . . . . . . . . 16
142117adantr 465 . . . . . . . . . . . . . . . . . 18
143 hashcl 12428 . . . . . . . . . . . . . . . . . 18
144142, 143syl 16 . . . . . . . . . . . . . . . . 17
145144nn0cnd 10879 . . . . . . . . . . . . . . . 16
146141, 145pncan2d 9956 . . . . . . . . . . . . . . 15