Theorem hashf1lem1 12504

Description: Lemma for hashf1 12506. (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:   ,   ,   ,   ,   ,

Proof of Theorem hashf1lem1

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		f1f 5786	. . . . . 6
2	1	adantl 466	. . . . 5
3		hashf1lem2.2	. . . . . 6
4		hashf1lem2.1	. . . . . . 7
5		snfi 7616	. . . . . . 7
6		unfi 7807	. . . . . . 7
7	4, 5, 6	sylancl 662	. . . . . 6
8	3, 7	elmapd 7453	. . . . 5
9	2, 8	syl5ibr 221	. . . 4
10	9	abssdv 3573	. . 3
11		ovex 6324	. . 3
12		ssexg 4598	. . 3
13	10, 11, 12	sylancl 662	. 2
14		difexg 4600	. . 3
15	3, 14	syl 16	. 2
16		vex 3112	. . . 4
17		reseq1 5272	. . . . . 6
18	17	eqeq1d 2459	. . . . 5
19		f1eq1 5781	. . . . 5
20	18, 19	anbi12d 710	. . . 4
21	16, 20	elab 3246	. . 3
22		f1f 5786	. . . . . . 7
23	22	ad2antll 728	. . . . . 6
24		ssun2 3667	. . . . . . 7
25		vex 3112	. . . . . . . 8
26	25	snss 4154	. . . . . . 7
27	24, 26	mpbir 209	. . . . . 6
28		ffvelrn 6029	. . . . . 6
29	23, 27, 28	sylancl 662	. . . . 5
30		hashf1lem2.3	. . . . . . 7
31	30	adantr 465	. . . . . 6
32		df-ima 5017	. . . . . . . . 9
33		simprl 756	. . . . . . . . . 10
34	33	rneqd 5235	. . . . . . . . 9
35	32, 34	syl5eq 2510	. . . . . . . 8
36	35	eleq2d 2527	. . . . . . 7
37		simprr 757	. . . . . . . 8
38	27	a1i 11	. . . . . . . 8
39		ssun1 3666	. . . . . . . . 9
40	39	a1i 11	. . . . . . . 8
41		f1elima 6171	. . . . . . . 8
42	37, 38, 40, 41	syl3anc 1228	. . . . . . 7
43	36, 42	bitr3d 255	. . . . . 6
44	31, 43	mtbird 301	. . . . 5
45	29, 44	eldifd 3486	. . . 4
46	45	ex 434	. . 3
47	21, 46	syl5bi 217	. 2
48		hashf1lem1.5	. . . . . . 7
49		f1f 5786	. . . . . . 7
50	48, 49	syl 16	. . . . . 6
51	50	adantr 465	. . . . 5
52		vex 3112	. . . . . . . 8
53	25, 52	f1osn 5858	. . . . . . 7
54		f1of 5821	. . . . . . 7
55	53, 54	ax-mp 5	. . . . . 6
56		eldifi 3625	. . . . . . . 8
57	56	adantl 466	. . . . . . 7
58	57	snssd 4175	. . . . . 6
59		fss 5744	. . . . . 6
60	55, 58, 59	sylancr 663	. . . . 5
61		res0 5283	. . . . . . 7
62		res0 5283	. . . . . . 7
63	61, 62	eqtr4i 2489	. . . . . 6
64		disjsn 4090	. . . . . . . . 9
65	30, 64	sylibr 212	. . . . . . . 8
66	65	adantr 465	. . . . . . 7
67	66	reseq2d 5278	. . . . . 6
68	66	reseq2d 5278	. . . . . 6
69	63, 67, 68	3eqtr4a 2524	. . . . 5
70		fresaunres1 5763	. . . . 5
71	51, 60, 69, 70	syl3anc 1228	. . . 4
72		f1f1orn 5832	. . . . . . . . 9
73	48, 72	syl 16	. . . . . . . 8
74	73	adantr 465	. . . . . . 7
75	53	a1i 11	. . . . . . 7
76		eldifn 3626	. . . . . . . . 9
77	76	adantl 466	. . . . . . . 8
78		disjsn 4090	. . . . . . . 8
79	77, 78	sylibr 212	. . . . . . 7
80		f1oun 5840	. . . . . . 7
81	74, 75, 66, 79, 80	syl22anc 1229	. . . . . 6
82		f1of1 5820	. . . . . 6
83	81, 82	syl 16	. . . . 5
84		frn 5742	. . . . . . 7
85	51, 84	syl 16	. . . . . 6
86	85, 58	unssd 3679	. . . . 5
87		f1ss 5791	. . . . 5
88	83, 86, 87	syl2anc 661	. . . 4
89		fex 6145	. . . . . . . 8
90	50, 4, 89	syl2anc 661	. . . . . . 7
91	90	adantr 465	. . . . . 6
92		snex 4693	. . . . . 6
93		unexg 6601	. . . . . 6
94	91, 92, 93	sylancl 662	. . . . 5
95		reseq1 5272	. . . . . . . 8
96	95	eqeq1d 2459	. . . . . . 7
97		f1eq1 5781	. . . . . . 7
98	96, 97	anbi12d 710	. . . . . 6
99	98	elabg 3247	. . . . 5
100	94, 99	syl 16	. . . 4
101	71, 88, 100	mpbir2and 922	. . 3
102	101	ex 434	. 2
103	21	anbi1i 695	. . 3
104		simprlr 764	. . . . . . 7
105		f1fn 5787	. . . . . . 7
106	104, 105	syl 16	. . . . . 6
107	81	adantrl 715	. . . . . . 7
108		f1ofn 5822	. . . . . . 7
109	107, 108	syl 16	. . . . . 6
110		eqfnfv 5981	. . . . . 6
111	106, 109, 110	syl2anc 661	. . . . 5
112		fvres 5885	. . . . . . . . . . 11
113	112	eqcomd 2465	. . . . . . . . . 10
114		simprll 763	. . . . . . . . . . 11
115	114	fveq1d 5873	. . . . . . . . . 10
116	113, 115	sylan9eqr 2520	. . . . . . . . 9
117	48	ad2antrr 725	. . . . . . . . . . 11
118		f1fn 5787	. . . . . . . . . . 11
119	117, 118	syl 16	. . . . . . . . . 10
120	25, 52	fnsn 5646	. . . . . . . . . . 11
121	120	a1i 11	. . . . . . . . . 10
122	65	ad2antrr 725	. . . . . . . . . 10
123		simpr 461	. . . . . . . . . 10
124		fvun1 5944	. . . . . . . . . 10
125	119, 121, 122, 123, 124	syl112anc 1232	. . . . . . . . 9
126	116, 125	eqtr4d 2501	. . . . . . . 8
127	126	ralrimiva 2871	. . . . . . 7
128	127	biantrurd 508	. . . . . 6
129		ralunb 3684	. . . . . 6
130	128, 129	syl6bbr 263	. . . . 5
131	25	a1i 11	. . . . . . . 8
132	52	a1i 11	. . . . . . . 8
133		fdm 5740	. . . . . . . . . . . 12
134	50, 133	syl 16	. . . . . . . . . . 11
135	134	eleq2d 2527	. . . . . . . . . 10
136	30, 135	mtbird 301	. . . . . . . . 9
137	136	adantr 465	. . . . . . . 8
138		fsnunfv 6111	. . . . . . . 8
139	131, 132, 137, 138	syl3anc 1228	. . . . . . 7
140	139	eqeq2d 2471	. . . . . 6
141		fveq2 5871	. . . . . . . 8
142		fveq2 5871	. . . . . . . 8
143	141, 142	eqeq12d 2479	. . . . . . 7
144	25, 143	ralsn 4068	. . . . . 6
145		eqcom 2466	. . . . . 6
146	140, 144, 145	3bitr4g 288	. . . . 5
147	111, 130, 146	3bitr2d 281	. . . 4
148	147	ex 434	. . 3
149	103, 148	syl5bi 217	. 2
150	13, 15, 47, 102, 149	en3d 7572	1

Syntax hints:  -.wn 3  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818  {cab 2442  A.wral 2807  cvv 3109  \cdif 3472  u.cun 3473  i^icin 3474  C_wss 3475  c0 3784  {csn 4029  <.cop 4035   class class class wbr 4452  domcdm 5004  rancrn 5005  |`cres 5006  "cima 5007  Fnwfn 5588  -->wf 5589  -1-1->wf1 5590  -1-1-onto->wf1o 5592  `cfv 5593  (class class class)co 6296  cmap 7439  cen 7533  cfn 7536  1c1 9514  caddc 9516  cle 9650  chash 12405

This theorem is referenced by:  hashf1lem2  12505

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-8 1820  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-rep 4563  ax-sep 4573  ax-nul 4581  ax-pow 4630  ax-pr 4691  ax-un 6592

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-reu 2814  df-rab 2816  df-v 3111  df-sbc 3328  df-csb 3435  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-pss 3491  df-nul 3785  df-if 3942  df-pw 4014  df-sn 4030  df-pr 4032  df-tp 4034  df-op 4036  df-uni 4250  df-int 4287  df-iun 4332  df-br 4453  df-opab 4511  df-mpt 4512  df-tr 4546  df-eprel 4796  df-id 4800  df-po 4805  df-so 4806  df-fr 4843  df-we 4845  df-ord 4886  df-on 4887  df-lim 4888  df-suc 4889  df-xp 5010  df-rel 5011  df-cnv 5012  df-co 5013  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017  df-iota 5556  df-fun 5595  df-fn 5596  df-f 5597  df-f1 5598  df-fo 5599  df-f1o 5600  df-fv 5601  df-ov 6299  df-oprab 6300  df-mpt2 6301  df-om 6701  df-recs 7061  df-rdg 7095  df-1o 7149  df-oadd 7153  df-er 7330  df-map 7441  df-en 7537  df-fin 7540