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

Theorem hashbclem 12501
Description: Lemma for hashbc 12502: inductive step. (Contributed by Mario Carneiro, 13-Jul-2014.)
Hypotheses
Ref Expression
hashbc.1
hashbc.2
hashbc.3
hashbc.4
Assertion
Ref Expression
hashbclem
Distinct variable groups:   , , ,   , ,   ,

Proof of Theorem hashbclem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 hashbc.4 . . . . 5
2 hashbc.3 . . . . 5
3 oveq2 6304 . . . . . . 7
4 eqeq2 2472 . . . . . . . . 9
54rabbidv 3101 . . . . . . . 8
65fveq2d 5875 . . . . . . 7
73, 6eqeq12d 2479 . . . . . 6
87rspcv 3206 . . . . 5
91, 2, 8sylc 60 . . . 4
10 ssun1 3666 . . . . . . . . . . . . 13
11 sspwb 4701 . . . . . . . . . . . . 13
1210, 11mpbi 208 . . . . . . . . . . . 12
1312sseli 3499 . . . . . . . . . . 11
1413adantl 466 . . . . . . . . . 10
15 hashbc.2 . . . . . . . . . . 11
16 elpwi 4021 . . . . . . . . . . . 12
1716ssneld 3505 . . . . . . . . . . 11
1815, 17mpan9 469 . . . . . . . . . 10
1914, 18jca 532 . . . . . . . . 9
20 elpwi 4021 . . . . . . . . . . . . . 14
21 uncom 3647 . . . . . . . . . . . . . 14
2220, 21syl6sseq 3549 . . . . . . . . . . . . 13
2322adantr 465 . . . . . . . . . . . 12
24 simpr 461 . . . . . . . . . . . . . 14
25 disjsn 4090 . . . . . . . . . . . . . 14
2624, 25sylibr 212 . . . . . . . . . . . . 13
27 disjssun 3884 . . . . . . . . . . . . 13
2826, 27syl 16 . . . . . . . . . . . 12
2923, 28mpbid 210 . . . . . . . . . . 11
30 vex 3112 . . . . . . . . . . . 12
3130elpw 4018 . . . . . . . . . . 11
3229, 31sylibr 212 . . . . . . . . . 10
3332adantl 466 . . . . . . . . 9
3419, 33impbida 832 . . . . . . . 8
3534anbi1d 704 . . . . . . 7
36 anass 649 . . . . . . 7
3735, 36syl6bb 261 . . . . . 6
3837rabbidva2 3099 . . . . 5
3938fveq2d 5875 . . . 4
409, 39eqtrd 2498 . . 3
41 peano2zm 10932 . . . . . 6
421, 41syl 16 . . . . 5
43 oveq2 6304 . . . . . . 7
44 eqeq2 2472 . . . . . . . . 9
4544rabbidv 3101 . . . . . . . 8
4645fveq2d 5875 . . . . . . 7
4743, 46eqeq12d 2479 . . . . . 6
4847rspcv 3206 . . . . 5
4942, 2, 48sylc 60 . . . 4
50 hashbc.1 . . . . . . . 8
51 pwfi 7835 . . . . . . . 8
5250, 51sylib 196 . . . . . . 7
53 rabexg 4602 . . . . . . 7
5452, 53syl 16 . . . . . 6
55 snfi 7616 . . . . . . . . . 10
56 unfi 7807 . . . . . . . . . 10
5750, 55, 56sylancl 662 . . . . . . . . 9
58 pwfi 7835 . . . . . . . . 9
5957, 58sylib 196 . . . . . . . 8
60 ssrab2 3584 . . . . . . . 8
61 ssfi 7760 . . . . . . . 8
6259, 60, 61sylancl 662 . . . . . . 7
63 elex 3118 . . . . . . 7
6462, 63syl 16 . . . . . 6
65 fveq2 5871 . . . . . . . . 9
6665eqeq1d 2459 . . . . . . . 8
6766elrab 3257 . . . . . . 7
68 elpwi 4021 . . . . . . . . . . . 12
6968ad2antrl 727 . . . . . . . . . . 11
70 unss1 3672 . . . . . . . . . . 11
7169, 70syl 16 . . . . . . . . . 10
72 vex 3112 . . . . . . . . . . . 12
73 snex 4693 . . . . . . . . . . . 12
7472, 73unex 6598 . . . . . . . . . . 11
7574elpw 4018 . . . . . . . . . 10
7671, 75sylibr 212 . . . . . . . . 9
7750adantr 465 . . . . . . . . . . . . 13
78 ssfi 7760 . . . . . . . . . . . . 13
7977, 69, 78syl2anc 661 . . . . . . . . . . . 12
8055a1i 11 . . . . . . . . . . . 12
8115adantr 465 . . . . . . . . . . . . . 14
8269, 81ssneldd 3506 . . . . . . . . . . . . 13
83 disjsn 4090 . . . . . . . . . . . . 13
8482, 83sylibr 212 . . . . . . . . . . . 12
85 hashun 12450 . . . . . . . . . . . 12
8679, 80, 84, 85syl3anc 1228 . . . . . . . . . . 11
87 simprr 757 . . . . . . . . . . . 12
88 vex 3112 . . . . . . . . . . . . . 14
89 hashsng 12438 . . . . . . . . . . . . . 14
9088, 89ax-mp 5 . . . . . . . . . . . . 13
9190a1i 11 . . . . . . . . . . . 12
9287, 91oveq12d 6314 . . . . . . . . . . 11
931adantr 465 . . . . . . . . . . . . 13
9493zcnd 10995 . . . . . . . . . . . 12
95 ax-1cn 9571 . . . . . . . . . . . 12
96 npcan 9852 . . . . . . . . . . . 12
9794, 95, 96sylancl 662 . . . . . . . . . . 11
9886, 92, 973eqtrd 2502 . . . . . . . . . 10
99 ssun2 3667 . . . . . . . . . . 11
10088snss 4154 . . . . . . . . . . 11
10199, 100mpbir 209 . . . . . . . . . 10
10298, 101jctil 537 . . . . . . . . 9
103 eleq2 2530 . . . . . . . . . . 11
104 fveq2 5871 . . . . . . . . . . . 12
105104eqeq1d 2459 . . . . . . . . . . 11
106103, 105anbi12d 710 . . . . . . . . . 10
107106elrab 3257 . . . . . . . . 9
10876, 102, 107sylanbrc 664 . . . . . . . 8
109108ex 434 . . . . . . 7
11067, 109syl5bi 217 . . . . . 6
111 eleq2 2530 . . . . . . . . 9
112 fveq2 5871 . . . . . . . . . 10
113112eqeq1d 2459 . . . . . . . . 9
114111, 113anbi12d 710 . . . . . . . 8
115114elrab 3257 . . . . . . 7
116 elpwi 4021 . . . . . . . . . . . . 13
117116ad2antrl 727 . . . . . . . . . . . 12
118117, 21syl6sseq 3549 . . . . . . . . . . 11
119 ssundif 3911 . . . . . . . . . . 11
120118, 119sylib 196 . . . . . . . . . 10
121 vex 3112 . . . . . . . . . . . 12
122 difexg 4600 . . . . . . . . . . . 12
123121, 122ax-mp 5 . . . . . . . . . . 11
124123elpw 4018 . . . . . . . . . 10
125120, 124sylibr 212 . . . . . . . . 9
12650adantr 465 . . . . . . . . . . . . . 14
127 ssfi 7760 . . . . . . . . . . . . . 14
128126, 120, 127syl2anc 661 . . . . . . . . . . . . 13
129 hashcl 12428 . . . . . . . . . . . . 13
130128, 129syl 16 . . . . . . . . . . . 12
131130nn0cnd 10879 . . . . . . . . . . 11
132 pncan 9849 . . . . . . . . . . 11
133131, 95, 132sylancl 662 . . . . . . . . . 10
134 undif1 3903 . . . . . . . . . . . . . 14
135 simprrl 765 . . . . . . . . . . . . . . . 16
136135snssd 4175 . . . . . . . . . . . . . . 15
137 ssequn2 3676 . . . . . . . . . . . . . . 15
138136, 137sylib 196 . . . . . . . . . . . . . 14
139134, 138syl5eq 2510 . . . . . . . . . . . . 13
140139fveq2d 5875 . . . . . . . . . . . 12
14155a1i 11 . . . . . . . . . . . . . 14
142 incom 3690 . . . . . . . . . . . . . . . 16
143 disjdif 3900 . . . . . . . . . . . . . . . 16
144142, 143eqtri 2486 . . . . . . . . . . . . . . 15
145144a1i 11 . . . . . . . . . . . . . 14
146 hashun 12450 . . . . . . . . . . . . . 14
147128, 141, 145, 146syl3anc 1228 . . . . . . . . . . . . 13
14890oveq2i 6307 . . . . . . . . . . . . 13
149147, 148syl6eq 2514 . . . . . . . . . . . 12
150 simprrr 766 . . . . . . . . . . . 12
151140, 149, 1503eqtr3d 2506 . . . . . . . . . . 11
152151oveq1d 6311 . . . . . . . . . 10
153133, 152eqtr3d 2500 . . . . . . . . 9
154 fveq2 5871 . . . . . . . . . . 11
155154eqeq1d 2459 . . . . . . . . . 10
156155elrab 3257 . . . . . . . . 9
157125, 153, 156sylanbrc 664 . . . . . . . 8
158157ex 434 . . . . . . 7
159115, 158syl5bi 217 . . . . . 6
16067, 115anbi12i 697 . . . . . . 7
161 simp3rl 1069 . . . . . . . . . . . 12
162161snssd 4175 . . . . . . . . . . 11
163 incom 3690 . . . . . . . . . . . 12
164843adant3 1016 . . . . . . . . . . . 12
165163, 164syl5eq 2510 . . . . . . . . . . 11
166 uneqdifeq 3916 . . . . . . . . . . 11
167162, 165, 166syl2anc 661 . . . . . . . . . 10
168167bicomd 201 . . . . . . . . 9
169 eqcom 2466 . . . . . . . . 9
170 eqcom 2466 . . . . . . . . . 10
171 uncom 3647 . . . . . . . . . . 11
172171eqeq1i 2464 . . . . . . . . . 10
173170, 172bitri 249 . . . . . . . . 9
174168, 169, 1733bitr4g 288 . . . . . . . 8
1751743expib 1199 . . . . . . 7
176160, 175syl5bi 217 . . . . . 6
17754, 64, 110, 159, 176en3d 7572 . . . . 5
178 ssrab2 3584 . . . . . . 7
179 ssfi 7760 . . . . . . 7
18052, 178, 179sylancl 662 . . . . . 6
181 hashen 12420 . . . . . 6
182180, 62, 181syl2anc 661 . . . . 5
183177, 182mpbird 232 . . . 4
18449, 183eqtrd 2498 . . 3
18540, 184oveq12d 6314 . 2
18655a1i 11 . . . . . 6
187 disjsn 4090 . . . . . . 7
18815, 187sylibr 212 . . . . . 6
189 hashun 12450 . . . . . 6
19050, 186, 188, 189syl3anc 1228 . . . . 5
19190oveq2i 6307 . . . . 5
192190, 191syl6eq 2514 . . . 4
193192oveq1d 6311 . . 3
194 hashcl 12428 . . . . 5
19550, 194syl 16 . . . 4
196 bcpasc 12399 . . . 4
197195, 1, 196syl2anc 661 . . 3
198193, 197eqtr4d 2501 . 2
199 pm2.1 417 . . . . . . . . 9
200199biantrur 506 . . . . . . . 8
201 andir 868 . . . . . . . 8
202200, 201bitri 249 . . . . . . 7
203202a1i 11 . . . . . 6
204203rabbiia 3098 . . . . 5
205 unrab 3768 . . . . 5
206204, 205eqtr4i 2489 . . . 4
207206fveq2i 5874 . . 3
208 ssrab2 3584 . . . . 5
209 ssfi 7760 . . . . 5
21059, 208, 209sylancl 662 . . . 4
211 inrab 3769 . . . . . 6
212 simprl 756 . . . . . . . . 9
213 simpll 753 . . . . . . . . 9
214212, 213pm2.65i 173 . . . . . . . 8
215214rgenw 2818 . . . . . . 7
216 rabeq0 3807 . . . . . . 7
217215, 216mpbir 209 . . . . . 6 <