hashfun - Metamath Proof Explorer

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

Theorem hashfun 12477

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 5607	. . 3
2		hashfn 12425	. . 3
3	1, 2	sylbi 195	. 2
4		dmfi 7805	. . . . . . . . . . 11
5		hashcl 12410	. . . . . . . . . . 11
6	4, 5	syl 16	. . . . . . . . . 10
7	6	nn0red 10860	. . . . . . . . 9
8	7	adantr 465	. . . . . . . 8 $/\$
9		df-rel 4996	. . . . . . . . . . . . 13
10		dfss3 3479	. . . . . . . . . . . . 13
11	9, 10	bitri 249	. . . . . . . . . . . 12
12	11	notbii 296	. . . . . . . . . . 11
13		rexnal 2891	. . . . . . . . . . 11
14	12, 13	bitr4i 252	. . . . . . . . . 10
15		dmun 5199	. . . . . . . . . . . . . . . 16 $\$ $\$
16	15	fveq2i 5859	. . . . . . . . . . . . . . 15 $\$ $\$
17		dmsnn0 5463	. . . . . . . . . . . . . . . . . . . . 21
18	17	biimpri 206	. . . . . . . . . . . . . . . . . . . 20
19	18	necon1bi 2676	. . . . . . . . . . . . . . . . . . 19
20	19	3ad2ant3 1020	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
21	20	uneq2d 3643	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
22		un0 3796	. . . . . . . . . . . . . . . . 17 $\$ $\$
23	21, 22	syl6eq 2500	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
24	23	fveq2d 5860	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
25	16, 24	syl5eq 2496	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
26		diffi 7753	. . . . . . . . . . . . . . . . . . 19 $\$
27		dmfi 7805	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
28	26, 27	syl 16	. . . . . . . . . . . . . . . . . 18 $\$
29		hashcl 12410	. . . . . . . . . . . . . . . . . 18 $\$ $\$
30	28, 29	syl 16	. . . . . . . . . . . . . . . . 17 $\$
31	30	nn0red 10860	. . . . . . . . . . . . . . . 16 $\$
32		hashcl 12410	. . . . . . . . . . . . . . . . . 18 $\$ $\$
33	26, 32	syl 16	. . . . . . . . . . . . . . . . 17 $\$
34	33	nn0red 10860	. . . . . . . . . . . . . . . 16 $\$
35		peano2re 9756	. . . . . . . . . . . . . . . . 17 $\$ $\$
36	34, 35	syl 16	. . . . . . . . . . . . . . . 16 $\$
37		fidomdm 7804	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
38	26, 37	syl 16	. . . . . . . . . . . . . . . . 17 $\$ $\$
39		hashdom 12429	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
40	28, 26, 39	syl2anc 661	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$
41	38, 40	mpbird 232	. . . . . . . . . . . . . . . 16 $\$ $\$
42	34	ltp1d 10483	. . . . . . . . . . . . . . . 16 $\$ $\$
43	31, 34, 36, 41, 42	lelttrd 9743	. . . . . . . . . . . . . . 15 $\$ $\$
44	43	3ad2ant1 1018	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
45	25, 44	eqbrtrd 4457	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
46		snfi 7598	. . . . . . . . . . . . . . . . 17
47		incom 3676	. . . . . . . . . . . . . . . . . 18 $\$ $\$
48		disjdif 3886	. . . . . . . . . . . . . . . . . 18 $\$
49	47, 48	eqtri 2472	. . . . . . . . . . . . . . . . 17 $\$
50		hashun 12432	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $\$ $\$ $\$
51	46, 49, 50	mp3an23 1317	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
52	26, 51	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
53		vex 3098	. . . . . . . . . . . . . . . . 17
54		hashsng 12420	. . . . . . . . . . . . . . . . 17
55	53, 54	ax-mp 5	. . . . . . . . . . . . . . . 16
56	55	oveq2i 6292	. . . . . . . . . . . . . . 15 $\$ $\$
57	52, 56	syl6req 2501	. . . . . . . . . . . . . 14 $\$ $\$
58	57	3ad2ant1 1018	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
59	45, 58	breqtrd 4461	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
60		difsnid 4161	. . . . . . . . . . . . . . 15 $\$
61	60	dmeqd 5195	. . . . . . . . . . . . . 14 $\$
62	61	fveq2d 5860	. . . . . . . . . . . . 13 $\$
63	62	3ad2ant2 1019	. . . . . . . . . . . 12 $/\$ $/\$ $\$
64	60	fveq2d 5860	. . . . . . . . . . . . 13 $\$
65	64	3ad2ant2 1019	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66	59, 63, 65	3brtr3d 4466	. . . . . . . . . . 11 $/\$ $/\$
67	66	rexlimdv3a 2937	. . . . . . . . . 10
68	14, 67	syl5bi 217	. . . . . . . . 9
69	68	imp 429	. . . . . . . 8 $/\$
70	8, 69	gtned 9723	. . . . . . 7 $/\$
71	70	ex 434	. . . . . 6
72	71	necon4bd 2665	. . . . 5
73	72	imp 429	. . . 4 $/\$
74		2nalexn 1636	. . . . . . . 8 $/\$ $/\$
75		df-ne 2640	. . . . . . . . . . . . 13
76	75	anbi2i 694	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
77		annim 425	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
78	76, 77	bitri 249	. . . . . . . . . . 11 $/\$ $/\$ $/\$
79	78	exbii 1654	. . . . . . . . . 10 $/\$ $/\$ $/\$
80		exnal 1635	. . . . . . . . . 10 $/\$ $/\$
81	79, 80	bitr2i 250	. . . . . . . . 9 $/\$ $/\$ $/\$
82	81	2exbii 1655	. . . . . . . 8 $/\$ $/\$ $/\$
83	74, 82	bitri 249	. . . . . . 7 $/\$ $/\$ $/\$
84	7	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$
85		2re 10612	. . . . . . . . . . . . 13
86		diffi 7753	. . . . . . . . . . . . . . . . 17 $\$
87		dmfi 7805	. . . . . . . . . . . . . . . . 17 $\$ $\$
88	86, 87	syl 16	. . . . . . . . . . . . . . . 16 $\$
89		hashcl 12410	. . . . . . . . . . . . . . . 16 $\$ $\$
90	88, 89	syl 16	. . . . . . . . . . . . . . 15 $\$
91	90	nn0red 10860	. . . . . . . . . . . . . 14 $\$
92	91	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
93		readdcl 9578	. . . . . . . . . . . . 13 $/\$ $\$ $\$
94	85, 92, 93	sylancr 663	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
95		hashcl 12410	. . . . . . . . . . . . . 14
96	95	nn0red 10860	. . . . . . . . . . . . 13
97	96	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98		1re 9598	. . . . . . . . . . . . . . 15
99		readdcl 9578	. . . . . . . . . . . . . . 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 5199	. . . . . . . . . . . . . . . . . 18 $\$ $\$
105		opex 4701	. . . . . . . . . . . . . . . . . . . . 21
106		opex 4701	. . . . . . . . . . . . . . . . . . . . 21
107	105, 106	prss 4169	. . . . . . . . . . . . . . . . . . . 20 $/\$
108		undif 3894	. . . . . . . . . . . . . . . . . . . 20 $\$
109	107, 108	sylbb 197	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
110	109	dmeqd 5195	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
111	104, 110	syl5reqr 2499	. . . . . . . . . . . . . . . . 17 $/\$ $\$
112		vex 3098	. . . . . . . . . . . . . . . . . . . 20
113		vex 3098	. . . . . . . . . . . . . . . . . . . 20
114	112, 113	dmprop 5473	. . . . . . . . . . . . . . . . . . 19
115		dfsn2 4027	. . . . . . . . . . . . . . . . . . 19
116	114, 115	eqtr4i 2475	. . . . . . . . . . . . . . . . . 18
117	116	uneq1i 3639	. . . . . . . . . . . . . . . . 17 $\$ $\$
118	111, 117	syl6eq 2500	. . . . . . . . . . . . . . . 16 $/\$ $\$
119	118	fveq2d 5860	. . . . . . . . . . . . . . 15 $/\$ $\$
120	119	ad2antrl 727	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
121		hashun2 12433	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$ $\$
122	46, 88, 121	sylancr 663	. . . . . . . . . . . . . . . 16 $\$ $\$
123	55	oveq1i 6291	. . . . . . . . . . . . . . . 16 $\$ $\$
124	122, 123	syl6breq 4476	. . . . . . . . . . . . . . 15 $\$ $\$
125	124	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
126	120, 125	eqbrtrd 4457	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
127		1lt2 10709	. . . . . . . . . . . . . . 15
128		ltadd1 10026	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$ $\$
129	98, 85, 128	mp3an12 1315	. . . . . . . . . . . . . . . 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 9743	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
134		fidomdm 7804	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
135	86, 134	syl 16	. . . . . . . . . . . . . . . 16 $\$ $\$
136		hashdom 12429	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
137	88, 86, 136	syl2anc 661	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
138	135, 137	mpbird 232	. . . . . . . . . . . . . . 15 $\$ $\$
139		hashcl 12410	. . . . . . . . . . . . . . . . . 18 $\$ $\$
140	86, 139	syl 16	. . . . . . . . . . . . . . . . 17 $\$
141	140	nn0red 10860	. . . . . . . . . . . . . . . 16 $\$
142		leadd2 10028	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
143	85, 142	mp3an3 1314	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
144	91, 141, 143	syl2anc 661	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$
145	138, 144	mpbid 210	. . . . . . . . . . . . . 14 $\$ $\$
146	145	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
147		prfi 7797	. . . . . . . . . . . . . . . . 17
148		disjdif 3886	. . . . . . . . . . . . . . . . 17 $\$
149		hashun 12432	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $\$ $\$
150	147, 148, 149	mp3an13 1316	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
151	86, 150	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
152	151	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
153	109	fveq2d 5860	. . . . . . . . . . . . . . 15 $/\$ $\$
154	153	ad2antrl 727	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
155	53, 112	opth 4711	. . . . . . . . . . . . . . . . . . 19 $/\$
156	155	simprbi 464	. . . . . . . . . . . . . . . . . 18
157	156	necon3i 2683	. . . . . . . . . . . . . . . . 17
158		hashprg 12442	. . . . . . . . . . . . . . . . . 18 $/\$
159	105, 106, 158	mp2an 672	. . . . . . . . . . . . . . . . 17
160	157, 159	sylib 196	. . . . . . . . . . . . . . . 16
161	160	oveq1d 6296	. . . . . . . . . . . . . . 15 $\$ $\$
162	161	ad2antll 728	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
163	152, 154, 162	3eqtr3rd 2493	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
164	146, 163	breqtrd 4461	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
165	84, 94, 97, 133, 164	ltletrd 9745	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	84, 165	gtned 9723	. . . . . . . . . 10 $/\$ $/\$ $/\$
167	166	ex 434	. . . . . . . . 9 $/\$ $/\$
168	167	exlimdv 1711	. . . . . . . 8 $/\$ $/\$
169	168	exlimdvv 1712	. . . . . . 7 $/\$ $/\$
170	83, 169	syl5bi 217	. . . . . 6 $/\$
171	170	necon4bd 2665	. . . . 5 $/\$
172	171	imp 429	. . . 4 $/\$ $/\$
173		dffun4 5590	. . . 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 974

wal 1381

wceq 1383

wex 1599

wcel 1804

wne 2638

wral 2793

wrex 2794

cvv 3095 $\$ cdif 3458

cun 3459

cin 3460

wss 3461

c0 3770

csn 4014

cpr 4016

cop 4020 class class class wbr 4437

cxp 4987

cdm 4989

wrel 4994

wfun 5572

wfn 5573

cfv 5578 (class class class)co 6281

cdom 7516

cfn 7518

cr 9494

c1 9496

caddc 9498

clt 9631

cle 9632

c2 10592

cn0 10802

chash 12387

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577 ax-cnex 9551 ax-resscn 9552 ax-1cn 9553 ax-icn 9554 ax-addcl 9555 ax-addrcl 9556 ax-mulcl 9557 ax-mulrcl 9558 ax-mulcom 9559 ax-addass 9560 ax-mulass 9561 ax-distr 9562 ax-i2m1 9563 ax-1ne0 9564 ax-1rid 9565 ax-rnegex 9566 ax-rrecex 9567 ax-cnre 9568 ax-pre-lttri 9569 ax-pre-lttrn 9570 ax-pre-ltadd 9571 ax-pre-mulgt0 9572

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 975 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-nel 2641 df-ral 2798 df-rex 2799 df-reu 2800 df-rmo 2801 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-tp 4019 df-op 4021 df-uni 4235 df-int 4272 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-tr 4531 df-eprel 4781 df-id 4785 df-po 4790 df-so 4791 df-fr 4828 df-we 4830 df-ord 4871 df-on 4872 df-lim 4873 df-suc 4874 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-riota 6242 df-ov 6284 df-oprab 6285 df-mpt2 6286 df-om 6686 df-1st 6785 df-2nd 6786 df-recs 7044 df-rdg 7078 df-1o 7132 df-oadd 7136 df-er 7313 df-en 7519 df-dom 7520 df-sdom 7521 df-fin 7522 df-card 8323 df-cda 8551 df-pnf 9633 df-mnf 9634 df-xr 9635 df-ltxr 9636 df-le 9637 df-sub 9812 df-neg 9813 df-nn 10544 df-2 10601 df-n0 10803 df-z 10872 df-uz 11093 df-fz 11684 df-hash 12388

This theorem is referenced by: hashfzdm 12480 hashfirdm 12482 cusgrasizeinds 24454

W3C validator