hashfun - Metamath Proof Explorer

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

Theorem hashfun 12214

Description: A finite set is a function iff it is equinumerous to its domain. (Contributed by Mario Carneiro, 26-Sep-2013.) (Revised by Mario Carneiro, 12-Mar-2015.)

**Assertion**
Ref	Expression
hashfun

Proof of Theorem hashfun Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		funfn 5462	. . 3
2		hashfn 12153	. . 3
3	1, 2	sylbi 195	. 2
4		dmfi 7609	. . . . . . . . . . 11
5		hashcl 12141	. . . . . . . . . . 11
6	4, 5	syl 16	. . . . . . . . . 10
7	6	nn0red 10652	. . . . . . . . 9
8	7	adantr 465	. . . . . . . 8 $/\$
9		df-rel 4862	. . . . . . . . . . . . 13
10		dfss3 3361	. . . . . . . . . . . . 13
11	9, 10	bitri 249	. . . . . . . . . . . 12
12	11	notbii 296	. . . . . . . . . . 11
13		rexnal 2741	. . . . . . . . . . 11
14	12, 13	bitr4i 252	. . . . . . . . . 10
15		dmun 5061	. . . . . . . . . . . . . . . 16 $\$ $\$
16	15	fveq2i 5709	. . . . . . . . . . . . . . 15 $\$ $\$
17		dmsnn0 5319	. . . . . . . . . . . . . . . . . . . . 21
18	17	biimpri 206	. . . . . . . . . . . . . . . . . . . 20
19	18	necon1bi 2669	. . . . . . . . . . . . . . . . . . 19
20	19	3ad2ant3 1011	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
21	20	uneq2d 3525	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
22		un0 3677	. . . . . . . . . . . . . . . . 17 $\$ $\$
23	21, 22	syl6eq 2491	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
24	23	fveq2d 5710	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
25	16, 24	syl5eq 2487	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
26		diffi 7558	. . . . . . . . . . . . . . . . . . 19 $\$
27		dmfi 7609	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
28	26, 27	syl 16	. . . . . . . . . . . . . . . . . 18 $\$
29		hashcl 12141	. . . . . . . . . . . . . . . . . 18 $\$ $\$
30	28, 29	syl 16	. . . . . . . . . . . . . . . . 17 $\$
31	30	nn0red 10652	. . . . . . . . . . . . . . . 16 $\$
32		hashcl 12141	. . . . . . . . . . . . . . . . . 18 $\$ $\$
33	26, 32	syl 16	. . . . . . . . . . . . . . . . 17 $\$
34	33	nn0red 10652	. . . . . . . . . . . . . . . 16 $\$
35		peano2re 9557	. . . . . . . . . . . . . . . . 17 $\$ $\$
36	34, 35	syl 16	. . . . . . . . . . . . . . . 16 $\$
37		fidomdm 7608	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
38	26, 37	syl 16	. . . . . . . . . . . . . . . . 17 $\$ $\$
39		hashdom 12157	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
40	28, 26, 39	syl2anc 661	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$
41	38, 40	mpbird 232	. . . . . . . . . . . . . . . 16 $\$ $\$
42	34	ltp1d 10278	. . . . . . . . . . . . . . . 16 $\$ $\$
43	31, 34, 36, 41, 42	lelttrd 9544	. . . . . . . . . . . . . . 15 $\$ $\$
44	43	3ad2ant1 1009	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
45	25, 44	eqbrtrd 4327	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
46		snfi 7405	. . . . . . . . . . . . . . . . 17
47		incom 3558	. . . . . . . . . . . . . . . . . 18 $\$ $\$
48		disjdif 3766	. . . . . . . . . . . . . . . . . 18 $\$
49	47, 48	eqtri 2463	. . . . . . . . . . . . . . . . 17 $\$
50		hashun 12160	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $\$ $\$ $\$
51	46, 49, 50	mp3an23 1306	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
52	26, 51	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
53		vex 2990	. . . . . . . . . . . . . . . . 17
54		hashsng 12151	. . . . . . . . . . . . . . . . 17
55	53, 54	ax-mp 5	. . . . . . . . . . . . . . . 16
56	55	oveq2i 6117	. . . . . . . . . . . . . . 15 $\$ $\$
57	52, 56	syl6req 2492	. . . . . . . . . . . . . 14 $\$ $\$
58	57	3ad2ant1 1009	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
59	45, 58	breqtrd 4331	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
60		difsnid 4034	. . . . . . . . . . . . . . 15 $\$
61	60	dmeqd 5057	. . . . . . . . . . . . . 14 $\$
62	61	fveq2d 5710	. . . . . . . . . . . . 13 $\$
63	62	3ad2ant2 1010	. . . . . . . . . . . 12 $/\$ $/\$ $\$
64	60	fveq2d 5710	. . . . . . . . . . . . 13 $\$
65	64	3ad2ant2 1010	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66	59, 63, 65	3brtr3d 4336	. . . . . . . . . . 11 $/\$ $/\$
67	66	rexlimdv3a 2858	. . . . . . . . . 10
68	14, 67	syl5bi 217	. . . . . . . . 9
69	68	imp 429	. . . . . . . 8 $/\$
70	8, 69	gtned 9524	. . . . . . 7 $/\$
71	70	ex 434	. . . . . 6
72	71	necon4bd 2688	. . . . 5
73	72	imp 429	. . . 4 $/\$
74		2nalexn 1619	. . . . . . . 8 $/\$ $/\$
75		df-ne 2622	. . . . . . . . . . . . 13
76	75	anbi2i 694	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
77		annim 425	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
78	76, 77	bitri 249	. . . . . . . . . . 11 $/\$ $/\$ $/\$
79	78	exbii 1634	. . . . . . . . . 10 $/\$ $/\$ $/\$
80		exnal 1618	. . . . . . . . . 10 $/\$ $/\$
81	79, 80	bitr2i 250	. . . . . . . . 9 $/\$ $/\$ $/\$
82	81	2exbii 1635	. . . . . . . 8 $/\$ $/\$ $/\$
83	74, 82	bitri 249	. . . . . . 7 $/\$ $/\$ $/\$
84	7	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$
85		2re 10406	. . . . . . . . . . . . 13
86		diffi 7558	. . . . . . . . . . . . . . . . 17 $\$
87		dmfi 7609	. . . . . . . . . . . . . . . . 17 $\$ $\$
88	86, 87	syl 16	. . . . . . . . . . . . . . . 16 $\$
89		hashcl 12141	. . . . . . . . . . . . . . . 16 $\$ $\$
90	88, 89	syl 16	. . . . . . . . . . . . . . 15 $\$
91	90	nn0red 10652	. . . . . . . . . . . . . 14 $\$
92	91	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
93		readdcl 9380	. . . . . . . . . . . . 13 $/\$ $\$ $\$
94	85, 92, 93	sylancr 663	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
95		hashcl 12141	. . . . . . . . . . . . . 14
96	95	nn0red 10652	. . . . . . . . . . . . 13
97	96	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98		1re 9400	. . . . . . . . . . . . . . 15
99		readdcl 9380	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
100	98, 91, 99	sylancr 663	. . . . . . . . . . . . . 14 $\$
101	100	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
102	85, 91, 93	sylancr 663	. . . . . . . . . . . . . 14 $\$
103	102	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
104		dmun 5061	. . . . . . . . . . . . . . . . . 18 $\$ $\$
105		opex 4571	. . . . . . . . . . . . . . . . . . . . 21
106		opex 4571	. . . . . . . . . . . . . . . . . . . . 21
107	105, 106	prss 4042	. . . . . . . . . . . . . . . . . . . 20 $/\$
108		undif 3774	. . . . . . . . . . . . . . . . . . . 20 $\$
109	107, 108	sylbb 197	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
110	109	dmeqd 5057	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
111	104, 110	syl5reqr 2490	. . . . . . . . . . . . . . . . 17 $/\$ $\$
112		vex 2990	. . . . . . . . . . . . . . . . . . . 20
113		vex 2990	. . . . . . . . . . . . . . . . . . . 20
114	112, 113	dmprop 5329	. . . . . . . . . . . . . . . . . . 19
115		dfsn2 3905	. . . . . . . . . . . . . . . . . . 19
116	114, 115	eqtr4i 2466	. . . . . . . . . . . . . . . . . 18
117	116	uneq1i 3521	. . . . . . . . . . . . . . . . 17 $\$ $\$
118	111, 117	syl6eq 2491	. . . . . . . . . . . . . . . 16 $/\$ $\$
119	118	fveq2d 5710	. . . . . . . . . . . . . . 15 $/\$ $\$
120	119	ad2antrl 727	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
121		hashun2 12161	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$ $\$
122	46, 88, 121	sylancr 663	. . . . . . . . . . . . . . . 16 $\$ $\$
123	55	oveq1i 6116	. . . . . . . . . . . . . . . 16 $\$ $\$
124	122, 123	syl6breq 4346	. . . . . . . . . . . . . . 15 $\$ $\$
125	124	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
126	120, 125	eqbrtrd 4327	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
127		1lt2 10503	. . . . . . . . . . . . . . 15
128		ltadd1 9821	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$ $\$
129	98, 85, 128	mp3an12 1304	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
130	91, 129	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
131	127, 130	mpbii 211	. . . . . . . . . . . . . 14 $\$ $\$
132	131	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
133	84, 101, 103, 126, 132	lelttrd 9544	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
134		fidomdm 7608	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
135	86, 134	syl 16	. . . . . . . . . . . . . . . 16 $\$ $\$
136		hashdom 12157	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
137	88, 86, 136	syl2anc 661	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
138	135, 137	mpbird 232	. . . . . . . . . . . . . . 15 $\$ $\$
139		hashcl 12141	. . . . . . . . . . . . . . . . . 18 $\$ $\$
140	86, 139	syl 16	. . . . . . . . . . . . . . . . 17 $\$
141	140	nn0red 10652	. . . . . . . . . . . . . . . 16 $\$
142		leadd2 9823	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
143	85, 142	mp3an3 1303	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
144	91, 141, 143	syl2anc 661	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$
145	138, 144	mpbid 210	. . . . . . . . . . . . . 14 $\$ $\$
146	145	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
147		prfi 7601	. . . . . . . . . . . . . . . . 17
148		disjdif 3766	. . . . . . . . . . . . . . . . 17 $\$
149		hashun 12160	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $\$ $\$
150	147, 148, 149	mp3an13 1305	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
151	86, 150	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
152	151	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
153	109	fveq2d 5710	. . . . . . . . . . . . . . 15 $/\$ $\$
154	153	ad2antrl 727	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
155	53, 112	opth 4581	. . . . . . . . . . . . . . . . . . 19 $/\$
156	155	simprbi 464	. . . . . . . . . . . . . . . . . 18
157	156	necon3i 2665	. . . . . . . . . . . . . . . . 17
158		hashprg 12170	. . . . . . . . . . . . . . . . . 18 $/\$
159	105, 106, 158	mp2an 672	. . . . . . . . . . . . . . . . 17
160	157, 159	sylib 196	. . . . . . . . . . . . . . . 16
161	160	oveq1d 6121	. . . . . . . . . . . . . . 15 $\$ $\$
162	161	ad2antll 728	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
163	152, 154, 162	3eqtr3rd 2484	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
164	146, 163	breqtrd 4331	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
165	84, 94, 97, 133, 164	ltletrd 9546	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	84, 165	gtned 9524	. . . . . . . . . 10 $/\$ $/\$ $/\$
167	166	ex 434	. . . . . . . . 9 $/\$ $/\$
168	167	exlimdv 1690	. . . . . . . 8 $/\$ $/\$
169	168	exlimdvv 1691	. . . . . . 7 $/\$ $/\$
170	83, 169	syl5bi 217	. . . . . 6 $/\$
171	170	necon4bd 2688	. . . . 5 $/\$
172	171	imp 429	. . . 4 $/\$ $/\$
173		dffun4 5445	. . . 4 $/\$ $/\$
174	73, 172, 173	sylanbrc 664	. . 3 $/\$
175	174	ex 434	. 2
176	3, 175	impbid2 204	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 965

wal 1367

wceq 1369

wex 1586

wcel 1756

wne 2620

wral 2730

wrex 2731

cvv 2987 $\$ cdif 3340

cun 3341

cin 3342

wss 3343

c0 3652

csn 3892

cpr 3894

cop 3898 class class class wbr 4307

cxp 4853

cdm 4855

wrel 4860

wfun 5427

wfn 5428

cfv 5433 (class class class)co 6106

cdom 7323

cfn 7325

cr 9296

c1 9298

caddc 9300

clt 9433

cle 9434

c2 10386

cn0 10594

chash 12118

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1591 ax-4 1602 ax-5 1670 ax-6 1708 ax-7 1728 ax-8 1758 ax-9 1760 ax-10 1775 ax-11 1780 ax-12 1792 ax-13 1943 ax-ext 2423 ax-rep 4418 ax-sep 4428 ax-nul 4436 ax-pow 4485 ax-pr 4546 ax-un 6387 ax-cnex 9353 ax-resscn 9354 ax-1cn 9355 ax-icn 9356 ax-addcl 9357 ax-addrcl 9358 ax-mulcl 9359 ax-mulrcl 9360 ax-mulcom 9361 ax-addass 9362 ax-mulass 9363 ax-distr 9364 ax-i2m1 9365 ax-1ne0 9366 ax-1rid 9367 ax-rnegex 9368 ax-rrecex 9369 ax-cnre 9370 ax-pre-lttri 9371 ax-pre-lttrn 9372 ax-pre-ltadd 9373 ax-pre-mulgt0 9374

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1372 df-ex 1587 df-nf 1590 df-sb 1701 df-eu 2257 df-mo 2258 df-clab 2430 df-cleq 2436 df-clel 2439 df-nfc 2577 df-ne 2622 df-nel 2623 df-ral 2735 df-rex 2736 df-reu 2737 df-rmo 2738 df-rab 2739 df-v 2989 df-sbc 3202 df-csb 3304 df-dif 3346 df-un 3348 df-in 3350 df-ss 3357 df-pss 3359 df-nul 3653 df-if 3807 df-pw 3877 df-sn 3893 df-pr 3895 df-tp 3897 df-op 3899 df-uni 4107 df-int 4144 df-iun 4188 df-br 4308 df-opab 4366 df-mpt 4367 df-tr 4401 df-eprel 4647 df-id 4651 df-po 4656 df-so 4657 df-fr 4694 df-we 4696 df-ord 4737 df-on 4738 df-lim 4739 df-suc 4740 df-xp 4861 df-rel 4862 df-cnv 4863 df-co 4864 df-dm 4865 df-rn 4866 df-res 4867 df-ima 4868 df-iota 5396 df-fun 5435 df-fn 5436 df-f 5437 df-f1 5438 df-fo 5439 df-f1o 5440 df-fv 5441 df-riota 6067 df-ov 6109 df-oprab 6110 df-mpt2 6111 df-om 6492 df-1st 6592 df-2nd 6593 df-recs 6847 df-rdg 6881 df-1o 6935 df-oadd 6939 df-er 7116 df-en 7326 df-dom 7327 df-sdom 7328 df-fin 7329 df-card 8124 df-cda 8352 df-pnf 9435 df-mnf 9436 df-xr 9437 df-ltxr 9438 df-le 9439 df-sub 9612 df-neg 9613 df-nn 10338 df-2 10395 df-n0 10595 df-z 10662 df-uz 10877 df-fz 11453 df-hash 12119

This theorem is referenced by: hashfzdm 12217 hashfirdm 12219 cusgrasizeinds 23399

W3C validator