hashfun - Metamath Proof Explorer

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

Theorem hashfun 12195

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 5444	. . 3
2		hashfn 12134	. . 3
3	1, 2	sylbi 195	. 2
4		dmfi 7590	. . . . . . . . . . 11
5		hashcl 12122	. . . . . . . . . . 11
6	4, 5	syl 16	. . . . . . . . . 10
7	6	nn0red 10633	. . . . . . . . 9
8	7	adantr 462	. . . . . . . 8 $/\$
9		df-rel 4843	. . . . . . . . . . . . 13
10		dfss3 3343	. . . . . . . . . . . . 13
11	9, 10	bitri 249	. . . . . . . . . . . 12
12	11	notbii 296	. . . . . . . . . . 11
13		rexnal 2724	. . . . . . . . . . 11
14	12, 13	bitr4i 252	. . . . . . . . . 10
15		dmun 5042	. . . . . . . . . . . . . . . 16 $\$ $\$
16	15	fveq2i 5691	. . . . . . . . . . . . . . 15 $\$ $\$
17		dmsnn0 5301	. . . . . . . . . . . . . . . . . . . . 21
18	17	biimpri 206	. . . . . . . . . . . . . . . . . . . 20
19	18	necon1bi 2652	. . . . . . . . . . . . . . . . . . 19
20	19	3ad2ant3 1006	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
21	20	uneq2d 3507	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
22		un0 3659	. . . . . . . . . . . . . . . . 17 $\$ $\$
23	21, 22	syl6eq 2489	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
24	23	fveq2d 5692	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
25	16, 24	syl5eq 2485	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
26		diffi 7539	. . . . . . . . . . . . . . . . . . 19 $\$
27		dmfi 7590	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
28	26, 27	syl 16	. . . . . . . . . . . . . . . . . 18 $\$
29		hashcl 12122	. . . . . . . . . . . . . . . . . 18 $\$ $\$
30	28, 29	syl 16	. . . . . . . . . . . . . . . . 17 $\$
31	30	nn0red 10633	. . . . . . . . . . . . . . . 16 $\$
32		hashcl 12122	. . . . . . . . . . . . . . . . . 18 $\$ $\$
33	26, 32	syl 16	. . . . . . . . . . . . . . . . 17 $\$
34	33	nn0red 10633	. . . . . . . . . . . . . . . 16 $\$
35		peano2re 9538	. . . . . . . . . . . . . . . . 17 $\$ $\$
36	34, 35	syl 16	. . . . . . . . . . . . . . . 16 $\$
37		fidomdm 7589	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
38	26, 37	syl 16	. . . . . . . . . . . . . . . . 17 $\$ $\$
39		hashdom 12138	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
40	28, 26, 39	syl2anc 656	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$
41	38, 40	mpbird 232	. . . . . . . . . . . . . . . 16 $\$ $\$
42	34	ltp1d 10259	. . . . . . . . . . . . . . . 16 $\$ $\$
43	31, 34, 36, 41, 42	lelttrd 9525	. . . . . . . . . . . . . . 15 $\$ $\$
44	43	3ad2ant1 1004	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
45	25, 44	eqbrtrd 4309	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
46		snfi 7386	. . . . . . . . . . . . . . . . 17
47		incom 3540	. . . . . . . . . . . . . . . . . 18 $\$ $\$
48		disjdif 3748	. . . . . . . . . . . . . . . . . 18 $\$
49	47, 48	eqtri 2461	. . . . . . . . . . . . . . . . 17 $\$
50		hashun 12141	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $\$ $\$ $\$
51	46, 49, 50	mp3an23 1301	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
52	26, 51	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
53		vex 2973	. . . . . . . . . . . . . . . . 17
54		hashsng 12132	. . . . . . . . . . . . . . . . 17
55	53, 54	ax-mp 5	. . . . . . . . . . . . . . . 16
56	55	oveq2i 6101	. . . . . . . . . . . . . . 15 $\$ $\$
57	52, 56	syl6req 2490	. . . . . . . . . . . . . 14 $\$ $\$
58	57	3ad2ant1 1004	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
59	45, 58	breqtrd 4313	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
60		difsnid 4016	. . . . . . . . . . . . . . 15 $\$
61	60	dmeqd 5038	. . . . . . . . . . . . . 14 $\$
62	61	fveq2d 5692	. . . . . . . . . . . . 13 $\$
63	62	3ad2ant2 1005	. . . . . . . . . . . 12 $/\$ $/\$ $\$
64	60	fveq2d 5692	. . . . . . . . . . . . 13 $\$
65	64	3ad2ant2 1005	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66	59, 63, 65	3brtr3d 4318	. . . . . . . . . . 11 $/\$ $/\$
67	66	rexlimdv3a 2841	. . . . . . . . . 10
68	14, 67	syl5bi 217	. . . . . . . . 9
69	68	imp 429	. . . . . . . 8 $/\$
70	8, 69	gtned 9505	. . . . . . 7 $/\$
71	70	ex 434	. . . . . 6
72	71	necon4bd 2671	. . . . 5
73	72	imp 429	. . . 4 $/\$
74		2nalexn 1624	. . . . . . . 8 $/\$ $/\$
75		df-ne 2606	. . . . . . . . . . . . 13
76	75	anbi2i 689	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
77		annim 425	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
78	76, 77	bitri 249	. . . . . . . . . . 11 $/\$ $/\$ $/\$
79	78	exbii 1639	. . . . . . . . . 10 $/\$ $/\$ $/\$
80		exnal 1623	. . . . . . . . . 10 $/\$ $/\$
81	79, 80	bitr2i 250	. . . . . . . . 9 $/\$ $/\$ $/\$
82	81	2exbii 1640	. . . . . . . 8 $/\$ $/\$ $/\$
83	74, 82	bitri 249	. . . . . . 7 $/\$ $/\$ $/\$
84	7	adantr 462	. . . . . . . . . . 11 $/\$ $/\$ $/\$
85		2re 10387	. . . . . . . . . . . . 13
86		diffi 7539	. . . . . . . . . . . . . . . . 17 $\$
87		dmfi 7590	. . . . . . . . . . . . . . . . 17 $\$ $\$
88	86, 87	syl 16	. . . . . . . . . . . . . . . 16 $\$
89		hashcl 12122	. . . . . . . . . . . . . . . 16 $\$ $\$
90	88, 89	syl 16	. . . . . . . . . . . . . . 15 $\$
91	90	nn0red 10633	. . . . . . . . . . . . . 14 $\$
92	91	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
93		readdcl 9361	. . . . . . . . . . . . 13 $/\$ $\$ $\$
94	85, 92, 93	sylancr 658	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
95		hashcl 12122	. . . . . . . . . . . . . 14
96	95	nn0red 10633	. . . . . . . . . . . . 13
97	96	adantr 462	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98		1re 9381	. . . . . . . . . . . . . . 15
99		readdcl 9361	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
100	98, 91, 99	sylancr 658	. . . . . . . . . . . . . 14 $\$
101	100	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
102	85, 91, 93	sylancr 658	. . . . . . . . . . . . . 14 $\$
103	102	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
104		dmun 5042	. . . . . . . . . . . . . . . . . 18 $\$ $\$
105		opex 4553	. . . . . . . . . . . . . . . . . . . . 21
106		opex 4553	. . . . . . . . . . . . . . . . . . . . 21
107	105, 106	prss 4024	. . . . . . . . . . . . . . . . . . . 20 $/\$
108		undif 3756	. . . . . . . . . . . . . . . . . . . 20 $\$
109	107, 108	sylbb 197	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
110	109	dmeqd 5038	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
111	104, 110	syl5reqr 2488	. . . . . . . . . . . . . . . . 17 $/\$ $\$
112		vex 2973	. . . . . . . . . . . . . . . . . . . 20
113		vex 2973	. . . . . . . . . . . . . . . . . . . 20
114	112, 113	dmprop 5311	. . . . . . . . . . . . . . . . . . 19
115		dfsn2 3887	. . . . . . . . . . . . . . . . . . 19
116	114, 115	eqtr4i 2464	. . . . . . . . . . . . . . . . . 18
117	116	uneq1i 3503	. . . . . . . . . . . . . . . . 17 $\$ $\$
118	111, 117	syl6eq 2489	. . . . . . . . . . . . . . . 16 $/\$ $\$
119	118	fveq2d 5692	. . . . . . . . . . . . . . 15 $/\$ $\$
120	119	ad2antrl 722	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
121		hashun2 12142	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$ $\$
122	46, 88, 121	sylancr 658	. . . . . . . . . . . . . . . 16 $\$ $\$
123	55	oveq1i 6100	. . . . . . . . . . . . . . . 16 $\$ $\$
124	122, 123	syl6breq 4328	. . . . . . . . . . . . . . 15 $\$ $\$
125	124	adantr 462	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
126	120, 125	eqbrtrd 4309	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
127		1lt2 10484	. . . . . . . . . . . . . . 15
128		ltadd1 9802	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$ $\$
129	98, 85, 128	mp3an12 1299	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
130	91, 129	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
131	127, 130	mpbii 211	. . . . . . . . . . . . . 14 $\$ $\$
132	131	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
133	84, 101, 103, 126, 132	lelttrd 9525	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
134		fidomdm 7589	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
135	86, 134	syl 16	. . . . . . . . . . . . . . . 16 $\$ $\$
136		hashdom 12138	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
137	88, 86, 136	syl2anc 656	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
138	135, 137	mpbird 232	. . . . . . . . . . . . . . 15 $\$ $\$
139		hashcl 12122	. . . . . . . . . . . . . . . . . 18 $\$ $\$
140	86, 139	syl 16	. . . . . . . . . . . . . . . . 17 $\$
141	140	nn0red 10633	. . . . . . . . . . . . . . . 16 $\$
142		leadd2 9804	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
143	85, 142	mp3an3 1298	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
144	91, 141, 143	syl2anc 656	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$
145	138, 144	mpbid 210	. . . . . . . . . . . . . 14 $\$ $\$
146	145	adantr 462	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
147		prfi 7582	. . . . . . . . . . . . . . . . 17
148		disjdif 3748	. . . . . . . . . . . . . . . . 17 $\$
149		hashun 12141	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $\$ $\$
150	147, 148, 149	mp3an13 1300	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
151	86, 150	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
152	151	adantr 462	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
153	109	fveq2d 5692	. . . . . . . . . . . . . . 15 $/\$ $\$
154	153	ad2antrl 722	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
155	53, 112	opth 4563	. . . . . . . . . . . . . . . . . . 19 $/\$
156	155	simprbi 461	. . . . . . . . . . . . . . . . . 18
157	156	necon3i 2648	. . . . . . . . . . . . . . . . 17
158		hashprg 12151	. . . . . . . . . . . . . . . . . 18 $/\$
159	105, 106, 158	mp2an 667	. . . . . . . . . . . . . . . . 17
160	157, 159	sylib 196	. . . . . . . . . . . . . . . 16
161	160	oveq1d 6105	. . . . . . . . . . . . . . 15 $\$ $\$
162	161	ad2antll 723	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
163	152, 154, 162	3eqtr3rd 2482	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
164	146, 163	breqtrd 4313	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
165	84, 94, 97, 133, 164	ltletrd 9527	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	84, 165	gtned 9505	. . . . . . . . . 10 $/\$ $/\$ $/\$
167	166	ex 434	. . . . . . . . 9 $/\$ $/\$
168	167	exlimdv 1695	. . . . . . . 8 $/\$ $/\$
169	168	exlimdvv 1696	. . . . . . 7 $/\$ $/\$
170	83, 169	syl5bi 217	. . . . . 6 $/\$
171	170	necon4bd 2671	. . . . 5 $/\$
172	171	imp 429	. . . 4 $/\$ $/\$
173		dffun4 5427	. . . 4 $/\$ $/\$
174	73, 172, 173	sylanbrc 659	. . 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 960

wal 1362

wceq 1364

wex 1591

wcel 1761

wne 2604

wral 2713

wrex 2714

cvv 2970 $\$ cdif 3322

cun 3323

cin 3324

wss 3325

c0 3634

csn 3874

cpr 3876

cop 3880 class class class wbr 4289

cxp 4834

cdm 4836

wrel 4841

wfun 5409

wfn 5410

cfv 5415 (class class class)co 6090

cdom 7304

cfn 7306

cr 9277

c1 9279

caddc 9281

clt 9414

cle 9415

c2 10367

cn0 10575

chash 12099

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6828 df-rdg 6862 df-1o 6916 df-oadd 6920 df-er 7097 df-en 7307 df-dom 7308 df-sdom 7309 df-fin 7310 df-card 8105 df-cda 8333 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-nn 10319 df-2 10376 df-n0 10576 df-z 10643 df-uz 10858 df-fz 11434 df-hash 12100

This theorem is referenced by: hashfzdm 12198 hashfirdm 12200 cusgrasizeinds 23319

W3C validator