hashfun - Metamath Proof Explorer

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

Theorem hashfun 12399

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 5525	. . 3
2		hashfn 12346	. . 3
3	1, 2	sylbi 195	. 2
4		dmfi 7718	. . . . . . . . . . 11
5		hashcl 12330	. . . . . . . . . . 11
6	4, 5	syl 16	. . . . . . . . . 10
7	6	nn0red 10770	. . . . . . . . 9
8	7	adantr 463	. . . . . . . 8 $/\$
9		df-rel 4920	. . . . . . . . . . . . 13
10		dfss3 3407	. . . . . . . . . . . . 13
11	9, 10	bitri 249	. . . . . . . . . . . 12
12	11	notbii 294	. . . . . . . . . . 11
13		rexnal 2830	. . . . . . . . . . 11
14	12, 13	bitr4i 252	. . . . . . . . . 10
15		dmun 5122	. . . . . . . . . . . . . . . 16 $\$ $\$
16	15	fveq2i 5777	. . . . . . . . . . . . . . 15 $\$ $\$
17		dmsnn0 5381	. . . . . . . . . . . . . . . . . . . . 21
18	17	biimpri 206	. . . . . . . . . . . . . . . . . . . 20
19	18	necon1bi 2615	. . . . . . . . . . . . . . . . . . 19
20	19	3ad2ant3 1017	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
21	20	uneq2d 3572	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
22		un0 3737	. . . . . . . . . . . . . . . . 17 $\$ $\$
23	21, 22	syl6eq 2439	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
24	23	fveq2d 5778	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
25	16, 24	syl5eq 2435	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
26		diffi 7667	. . . . . . . . . . . . . . . . . . 19 $\$
27		dmfi 7718	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
28	26, 27	syl 16	. . . . . . . . . . . . . . . . . 18 $\$
29		hashcl 12330	. . . . . . . . . . . . . . . . . 18 $\$ $\$
30	28, 29	syl 16	. . . . . . . . . . . . . . . . 17 $\$
31	30	nn0red 10770	. . . . . . . . . . . . . . . 16 $\$
32		hashcl 12330	. . . . . . . . . . . . . . . . . 18 $\$ $\$
33	26, 32	syl 16	. . . . . . . . . . . . . . . . 17 $\$
34	33	nn0red 10770	. . . . . . . . . . . . . . . 16 $\$
35		peano2re 9664	. . . . . . . . . . . . . . . . 17 $\$ $\$
36	34, 35	syl 16	. . . . . . . . . . . . . . . 16 $\$
37		fidomdm 7717	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
38	26, 37	syl 16	. . . . . . . . . . . . . . . . 17 $\$ $\$
39		hashdom 12350	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
40	28, 26, 39	syl2anc 659	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$
41	38, 40	mpbird 232	. . . . . . . . . . . . . . . 16 $\$ $\$
42	34	ltp1d 10392	. . . . . . . . . . . . . . . 16 $\$ $\$
43	31, 34, 36, 41, 42	lelttrd 9651	. . . . . . . . . . . . . . 15 $\$ $\$
44	43	3ad2ant1 1015	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
45	25, 44	eqbrtrd 4387	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
46		snfi 7515	. . . . . . . . . . . . . . . . 17
47		incom 3605	. . . . . . . . . . . . . . . . . 18 $\$ $\$
48		disjdif 3816	. . . . . . . . . . . . . . . . . 18 $\$
49	47, 48	eqtri 2411	. . . . . . . . . . . . . . . . 17 $\$
50		hashun 12353	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $\$ $\$ $\$
51	46, 49, 50	mp3an23 1314	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
52	26, 51	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
53		vex 3037	. . . . . . . . . . . . . . . . 17
54		hashsng 12341	. . . . . . . . . . . . . . . . 17
55	53, 54	ax-mp 5	. . . . . . . . . . . . . . . 16
56	55	oveq2i 6207	. . . . . . . . . . . . . . 15 $\$ $\$
57	52, 56	syl6req 2440	. . . . . . . . . . . . . 14 $\$ $\$
58	57	3ad2ant1 1015	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
59	45, 58	breqtrd 4391	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
60		difsnid 4090	. . . . . . . . . . . . . . 15 $\$
61	60	dmeqd 5118	. . . . . . . . . . . . . 14 $\$
62	61	fveq2d 5778	. . . . . . . . . . . . 13 $\$
63	62	3ad2ant2 1016	. . . . . . . . . . . 12 $/\$ $/\$ $\$
64	60	fveq2d 5778	. . . . . . . . . . . . 13 $\$
65	64	3ad2ant2 1016	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66	59, 63, 65	3brtr3d 4396	. . . . . . . . . . 11 $/\$ $/\$
67	66	rexlimdv3a 2876	. . . . . . . . . 10
68	14, 67	syl5bi 217	. . . . . . . . 9
69	68	imp 427	. . . . . . . 8 $/\$
70	8, 69	gtned 9631	. . . . . . 7 $/\$
71	70	ex 432	. . . . . 6
72	71	necon4bd 2604	. . . . 5
73	72	imp 427	. . . 4 $/\$
74		2nalexn 1657	. . . . . . . 8 $/\$ $/\$
75		df-ne 2579	. . . . . . . . . . . . 13
76	75	anbi2i 692	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
77		annim 423	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
78	76, 77	bitri 249	. . . . . . . . . . 11 $/\$ $/\$ $/\$
79	78	exbii 1675	. . . . . . . . . 10 $/\$ $/\$ $/\$
80		exnal 1656	. . . . . . . . . 10 $/\$ $/\$
81	79, 80	bitr2i 250	. . . . . . . . 9 $/\$ $/\$ $/\$
82	81	2exbii 1676	. . . . . . . 8 $/\$ $/\$ $/\$
83	74, 82	bitri 249	. . . . . . 7 $/\$ $/\$ $/\$
84	7	adantr 463	. . . . . . . . . . 11 $/\$ $/\$ $/\$
85		2re 10522	. . . . . . . . . . . . 13
86		diffi 7667	. . . . . . . . . . . . . . . . 17 $\$
87		dmfi 7718	. . . . . . . . . . . . . . . . 17 $\$ $\$
88	86, 87	syl 16	. . . . . . . . . . . . . . . 16 $\$
89		hashcl 12330	. . . . . . . . . . . . . . . 16 $\$ $\$
90	88, 89	syl 16	. . . . . . . . . . . . . . 15 $\$
91	90	nn0red 10770	. . . . . . . . . . . . . 14 $\$
92	91	adantr 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
93		readdcl 9486	. . . . . . . . . . . . 13 $/\$ $\$ $\$
94	85, 92, 93	sylancr 661	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
95		hashcl 12330	. . . . . . . . . . . . . 14
96	95	nn0red 10770	. . . . . . . . . . . . 13
97	96	adantr 463	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98		1re 9506	. . . . . . . . . . . . . . 15
99		readdcl 9486	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
100	98, 91, 99	sylancr 661	. . . . . . . . . . . . . 14 $\$
101	100	adantr 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
102	85, 91, 93	sylancr 661	. . . . . . . . . . . . . 14 $\$
103	102	adantr 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
104		dmun 5122	. . . . . . . . . . . . . . . . . 18 $\$ $\$
105		opex 4626	. . . . . . . . . . . . . . . . . . . . 21
106		opex 4626	. . . . . . . . . . . . . . . . . . . . 21
107	105, 106	prss 4098	. . . . . . . . . . . . . . . . . . . 20 $/\$
108		undif 3824	. . . . . . . . . . . . . . . . . . . 20 $\$
109	107, 108	sylbb 197	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
110	109	dmeqd 5118	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
111	104, 110	syl5reqr 2438	. . . . . . . . . . . . . . . . 17 $/\$ $\$
112		vex 3037	. . . . . . . . . . . . . . . . . . . 20
113		vex 3037	. . . . . . . . . . . . . . . . . . . 20
114	112, 113	dmprop 5391	. . . . . . . . . . . . . . . . . . 19
115		dfsn2 3957	. . . . . . . . . . . . . . . . . . 19
116	114, 115	eqtr4i 2414	. . . . . . . . . . . . . . . . . 18
117	116	uneq1i 3568	. . . . . . . . . . . . . . . . 17 $\$ $\$
118	111, 117	syl6eq 2439	. . . . . . . . . . . . . . . 16 $/\$ $\$
119	118	fveq2d 5778	. . . . . . . . . . . . . . 15 $/\$ $\$
120	119	ad2antrl 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
121		hashun2 12354	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$ $\$
122	46, 88, 121	sylancr 661	. . . . . . . . . . . . . . . 16 $\$ $\$
123	55	oveq1i 6206	. . . . . . . . . . . . . . . 16 $\$ $\$
124	122, 123	syl6breq 4406	. . . . . . . . . . . . . . 15 $\$ $\$
125	124	adantr 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
126	120, 125	eqbrtrd 4387	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
127		1lt2 10619	. . . . . . . . . . . . . . 15
128		ltadd1 9937	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$ $\$
129	98, 85, 128	mp3an12 1312	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
130	91, 129	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
131	127, 130	mpbii 211	. . . . . . . . . . . . . 14 $\$ $\$
132	131	adantr 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
133	84, 101, 103, 126, 132	lelttrd 9651	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
134		fidomdm 7717	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
135	86, 134	syl 16	. . . . . . . . . . . . . . . 16 $\$ $\$
136		hashdom 12350	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
137	88, 86, 136	syl2anc 659	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
138	135, 137	mpbird 232	. . . . . . . . . . . . . . 15 $\$ $\$
139		hashcl 12330	. . . . . . . . . . . . . . . . . 18 $\$ $\$
140	86, 139	syl 16	. . . . . . . . . . . . . . . . 17 $\$
141	140	nn0red 10770	. . . . . . . . . . . . . . . 16 $\$
142		leadd2 9939	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
143	85, 142	mp3an3 1311	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
144	91, 141, 143	syl2anc 659	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$
145	138, 144	mpbid 210	. . . . . . . . . . . . . 14 $\$ $\$
146	145	adantr 463	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
147		prfi 7710	. . . . . . . . . . . . . . . . 17
148		disjdif 3816	. . . . . . . . . . . . . . . . 17 $\$
149		hashun 12353	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $\$ $\$
150	147, 148, 149	mp3an13 1313	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
151	86, 150	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
152	151	adantr 463	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
153	109	fveq2d 5778	. . . . . . . . . . . . . . 15 $/\$ $\$
154	153	ad2antrl 725	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
155	53, 112	opth 4636	. . . . . . . . . . . . . . . . . . 19 $/\$
156	155	simprbi 462	. . . . . . . . . . . . . . . . . 18
157	156	necon3i 2622	. . . . . . . . . . . . . . . . 17
158		hashprg 12364	. . . . . . . . . . . . . . . . . 18 $/\$
159	105, 106, 158	mp2an 670	. . . . . . . . . . . . . . . . 17
160	157, 159	sylib 196	. . . . . . . . . . . . . . . 16
161	160	oveq1d 6211	. . . . . . . . . . . . . . 15 $\$ $\$
162	161	ad2antll 726	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
163	152, 154, 162	3eqtr3rd 2432	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
164	146, 163	breqtrd 4391	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
165	84, 94, 97, 133, 164	ltletrd 9653	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	84, 165	gtned 9631	. . . . . . . . . 10 $/\$ $/\$ $/\$
167	166	ex 432	. . . . . . . . 9 $/\$ $/\$
168	167	exlimdv 1732	. . . . . . . 8 $/\$ $/\$
169	168	exlimdvv 1733	. . . . . . 7 $/\$ $/\$
170	83, 169	syl5bi 217	. . . . . 6 $/\$
171	170	necon4bd 2604	. . . . 5 $/\$
172	171	imp 427	. . . 4 $/\$ $/\$
173		dffun4 5508	. . . 4 $/\$ $/\$
174	73, 172, 173	sylanbrc 662	. . 3 $/\$
175	174	ex 432	. 2
176	3, 175	impbid2 204	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367 $/\$ w3a 971

wal 1397

wceq 1399

wex 1620

wcel 1826

wne 2577

wral 2732

wrex 2733

cvv 3034 $\$ cdif 3386

cun 3387

cin 3388

wss 3389

c0 3711

csn 3944

cpr 3946

cop 3950 class class class wbr 4367

cxp 4911

cdm 4913

wrel 4918

wfun 5490

wfn 5491

cfv 5496 (class class class)co 6196

cdom 7433

cfn 7435

cr 9402

c1 9404

caddc 9406

clt 9539

cle 9540

c2 10502

cn0 10712

chash 12307

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1626 ax-4 1639 ax-5 1712 ax-6 1755 ax-7 1798 ax-8 1828 ax-9 1830 ax-10 1845 ax-11 1850 ax-12 1862 ax-13 2006 ax-ext 2360 ax-rep 4478 ax-sep 4488 ax-nul 4496 ax-pow 4543 ax-pr 4601 ax-un 6491 ax-cnex 9459 ax-resscn 9460 ax-1cn 9461 ax-icn 9462 ax-addcl 9463 ax-addrcl 9464 ax-mulcl 9465 ax-mulrcl 9466 ax-mulcom 9467 ax-addass 9468 ax-mulass 9469 ax-distr 9470 ax-i2m1 9471 ax-1ne0 9472 ax-1rid 9473 ax-rnegex 9474 ax-rrecex 9475 ax-cnre 9476 ax-pre-lttri 9477 ax-pre-lttrn 9478 ax-pre-ltadd 9479 ax-pre-mulgt0 9480

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1402 df-ex 1621 df-nf 1625 df-sb 1748 df-eu 2222 df-mo 2223 df-clab 2368 df-cleq 2374 df-clel 2377 df-nfc 2532 df-ne 2579 df-nel 2580 df-ral 2737 df-rex 2738 df-reu 2739 df-rmo 2740 df-rab 2741 df-v 3036 df-sbc 3253 df-csb 3349 df-dif 3392 df-un 3394 df-in 3396 df-ss 3403 df-pss 3405 df-nul 3712 df-if 3858 df-pw 3929 df-sn 3945 df-pr 3947 df-tp 3949 df-op 3951 df-uni 4164 df-int 4200 df-iun 4245 df-br 4368 df-opab 4426 df-mpt 4427 df-tr 4461 df-eprel 4705 df-id 4709 df-po 4714 df-so 4715 df-fr 4752 df-we 4754 df-ord 4795 df-on 4796 df-lim 4797 df-suc 4798 df-xp 4919 df-rel 4920 df-cnv 4921 df-co 4922 df-dm 4923 df-rn 4924 df-res 4925 df-ima 4926 df-iota 5460 df-fun 5498 df-fn 5499 df-f 5500 df-f1 5501 df-fo 5502 df-f1o 5503 df-fv 5504 df-riota 6158 df-ov 6199 df-oprab 6200 df-mpt2 6201 df-om 6600 df-1st 6699 df-2nd 6700 df-recs 6960 df-rdg 6994 df-1o 7048 df-oadd 7052 df-er 7229 df-en 7436 df-dom 7437 df-sdom 7438 df-fin 7439 df-card 8233 df-cda 8461 df-pnf 9541 df-mnf 9542 df-xr 9543 df-ltxr 9544 df-le 9545 df-sub 9720 df-neg 9721 df-nn 10453 df-2 10511 df-n0 10713 df-z 10782 df-uz 11002 df-fz 11594 df-hash 12308

This theorem is referenced by: hashfzdm 12402 hashfirdm 12404 cusgrasizeinds 24597

W3C validator