hashfun - Metamath Proof Explorer

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

Theorem hashfun 12457

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 5615	. . 3
2		hashfn 12407	. . 3
3	1, 2	sylbi 195	. 2
4		dmfi 7799	. . . . . . . . . . 11
5		hashcl 12392	. . . . . . . . . . 11
6	4, 5	syl 16	. . . . . . . . . 10
7	6	nn0red 10849	. . . . . . . . 9
8	7	adantr 465	. . . . . . . 8 $/\$
9		df-rel 5006	. . . . . . . . . . . . 13
10		dfss3 3494	. . . . . . . . . . . . 13
11	9, 10	bitri 249	. . . . . . . . . . . 12
12	11	notbii 296	. . . . . . . . . . 11
13		rexnal 2912	. . . . . . . . . . 11
14	12, 13	bitr4i 252	. . . . . . . . . 10
15		dmun 5207	. . . . . . . . . . . . . . . 16 $\$ $\$
16	15	fveq2i 5867	. . . . . . . . . . . . . . 15 $\$ $\$
17		dmsnn0 5471	. . . . . . . . . . . . . . . . . . . . 21
18	17	biimpri 206	. . . . . . . . . . . . . . . . . . . 20
19	18	necon1bi 2700	. . . . . . . . . . . . . . . . . . 19
20	19	3ad2ant3 1019	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
21	20	uneq2d 3658	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
22		un0 3810	. . . . . . . . . . . . . . . . 17 $\$ $\$
23	21, 22	syl6eq 2524	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
24	23	fveq2d 5868	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
25	16, 24	syl5eq 2520	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
26		diffi 7747	. . . . . . . . . . . . . . . . . . 19 $\$
27		dmfi 7799	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
28	26, 27	syl 16	. . . . . . . . . . . . . . . . . 18 $\$
29		hashcl 12392	. . . . . . . . . . . . . . . . . 18 $\$ $\$
30	28, 29	syl 16	. . . . . . . . . . . . . . . . 17 $\$
31	30	nn0red 10849	. . . . . . . . . . . . . . . 16 $\$
32		hashcl 12392	. . . . . . . . . . . . . . . . . 18 $\$ $\$
33	26, 32	syl 16	. . . . . . . . . . . . . . . . 17 $\$
34	33	nn0red 10849	. . . . . . . . . . . . . . . 16 $\$
35		peano2re 9748	. . . . . . . . . . . . . . . . 17 $\$ $\$
36	34, 35	syl 16	. . . . . . . . . . . . . . . 16 $\$
37		fidomdm 7798	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
38	26, 37	syl 16	. . . . . . . . . . . . . . . . 17 $\$ $\$
39		hashdom 12411	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
40	28, 26, 39	syl2anc 661	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$
41	38, 40	mpbird 232	. . . . . . . . . . . . . . . 16 $\$ $\$
42	34	ltp1d 10472	. . . . . . . . . . . . . . . 16 $\$ $\$
43	31, 34, 36, 41, 42	lelttrd 9735	. . . . . . . . . . . . . . 15 $\$ $\$
44	43	3ad2ant1 1017	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
45	25, 44	eqbrtrd 4467	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
46		snfi 7593	. . . . . . . . . . . . . . . . 17
47		incom 3691	. . . . . . . . . . . . . . . . . 18 $\$ $\$
48		disjdif 3899	. . . . . . . . . . . . . . . . . 18 $\$
49	47, 48	eqtri 2496	. . . . . . . . . . . . . . . . 17 $\$
50		hashun 12414	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $\$ $\$ $\$
51	46, 49, 50	mp3an23 1316	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
52	26, 51	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
53		vex 3116	. . . . . . . . . . . . . . . . 17
54		hashsng 12402	. . . . . . . . . . . . . . . . 17
55	53, 54	ax-mp 5	. . . . . . . . . . . . . . . 16
56	55	oveq2i 6293	. . . . . . . . . . . . . . 15 $\$ $\$
57	52, 56	syl6req 2525	. . . . . . . . . . . . . 14 $\$ $\$
58	57	3ad2ant1 1017	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
59	45, 58	breqtrd 4471	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
60		difsnid 4173	. . . . . . . . . . . . . . 15 $\$
61	60	dmeqd 5203	. . . . . . . . . . . . . 14 $\$
62	61	fveq2d 5868	. . . . . . . . . . . . 13 $\$
63	62	3ad2ant2 1018	. . . . . . . . . . . 12 $/\$ $/\$ $\$
64	60	fveq2d 5868	. . . . . . . . . . . . 13 $\$
65	64	3ad2ant2 1018	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66	59, 63, 65	3brtr3d 4476	. . . . . . . . . . 11 $/\$ $/\$
67	66	rexlimdv3a 2957	. . . . . . . . . 10
68	14, 67	syl5bi 217	. . . . . . . . 9
69	68	imp 429	. . . . . . . 8 $/\$
70	8, 69	gtned 9715	. . . . . . 7 $/\$
71	70	ex 434	. . . . . 6
72	71	necon4bd 2689	. . . . 5
73	72	imp 429	. . . 4 $/\$
74		2nalexn 1629	. . . . . . . 8 $/\$ $/\$
75		df-ne 2664	. . . . . . . . . . . . 13
76	75	anbi2i 694	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
77		annim 425	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
78	76, 77	bitri 249	. . . . . . . . . . 11 $/\$ $/\$ $/\$
79	78	exbii 1644	. . . . . . . . . 10 $/\$ $/\$ $/\$
80		exnal 1628	. . . . . . . . . 10 $/\$ $/\$
81	79, 80	bitr2i 250	. . . . . . . . 9 $/\$ $/\$ $/\$
82	81	2exbii 1645	. . . . . . . 8 $/\$ $/\$ $/\$
83	74, 82	bitri 249	. . . . . . 7 $/\$ $/\$ $/\$
84	7	adantr 465	. . . . . . . . . . 11 $/\$ $/\$ $/\$
85		2re 10601	. . . . . . . . . . . . 13
86		diffi 7747	. . . . . . . . . . . . . . . . 17 $\$
87		dmfi 7799	. . . . . . . . . . . . . . . . 17 $\$ $\$
88	86, 87	syl 16	. . . . . . . . . . . . . . . 16 $\$
89		hashcl 12392	. . . . . . . . . . . . . . . 16 $\$ $\$
90	88, 89	syl 16	. . . . . . . . . . . . . . 15 $\$
91	90	nn0red 10849	. . . . . . . . . . . . . 14 $\$
92	91	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
93		readdcl 9571	. . . . . . . . . . . . 13 $/\$ $\$ $\$
94	85, 92, 93	sylancr 663	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
95		hashcl 12392	. . . . . . . . . . . . . 14
96	95	nn0red 10849	. . . . . . . . . . . . 13
97	96	adantr 465	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98		1re 9591	. . . . . . . . . . . . . . 15
99		readdcl 9571	. . . . . . . . . . . . . . 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 5207	. . . . . . . . . . . . . . . . . 18 $\$ $\$
105		opex 4711	. . . . . . . . . . . . . . . . . . . . 21
106		opex 4711	. . . . . . . . . . . . . . . . . . . . 21
107	105, 106	prss 4181	. . . . . . . . . . . . . . . . . . . 20 $/\$
108		undif 3907	. . . . . . . . . . . . . . . . . . . 20 $\$
109	107, 108	sylbb 197	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
110	109	dmeqd 5203	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
111	104, 110	syl5reqr 2523	. . . . . . . . . . . . . . . . 17 $/\$ $\$
112		vex 3116	. . . . . . . . . . . . . . . . . . . 20
113		vex 3116	. . . . . . . . . . . . . . . . . . . 20
114	112, 113	dmprop 5481	. . . . . . . . . . . . . . . . . . 19
115		dfsn2 4040	. . . . . . . . . . . . . . . . . . 19
116	114, 115	eqtr4i 2499	. . . . . . . . . . . . . . . . . 18
117	116	uneq1i 3654	. . . . . . . . . . . . . . . . 17 $\$ $\$
118	111, 117	syl6eq 2524	. . . . . . . . . . . . . . . 16 $/\$ $\$
119	118	fveq2d 5868	. . . . . . . . . . . . . . 15 $/\$ $\$
120	119	ad2antrl 727	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
121		hashun2 12415	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$ $\$
122	46, 88, 121	sylancr 663	. . . . . . . . . . . . . . . 16 $\$ $\$
123	55	oveq1i 6292	. . . . . . . . . . . . . . . 16 $\$ $\$
124	122, 123	syl6breq 4486	. . . . . . . . . . . . . . 15 $\$ $\$
125	124	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
126	120, 125	eqbrtrd 4467	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
127		1lt2 10698	. . . . . . . . . . . . . . 15
128		ltadd1 10015	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$ $\$
129	98, 85, 128	mp3an12 1314	. . . . . . . . . . . . . . . 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 9735	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
134		fidomdm 7798	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
135	86, 134	syl 16	. . . . . . . . . . . . . . . 16 $\$ $\$
136		hashdom 12411	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
137	88, 86, 136	syl2anc 661	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
138	135, 137	mpbird 232	. . . . . . . . . . . . . . 15 $\$ $\$
139		hashcl 12392	. . . . . . . . . . . . . . . . . 18 $\$ $\$
140	86, 139	syl 16	. . . . . . . . . . . . . . . . 17 $\$
141	140	nn0red 10849	. . . . . . . . . . . . . . . 16 $\$
142		leadd2 10017	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
143	85, 142	mp3an3 1313	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
144	91, 141, 143	syl2anc 661	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$
145	138, 144	mpbid 210	. . . . . . . . . . . . . 14 $\$ $\$
146	145	adantr 465	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
147		prfi 7791	. . . . . . . . . . . . . . . . 17
148		disjdif 3899	. . . . . . . . . . . . . . . . 17 $\$
149		hashun 12414	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $\$ $\$
150	147, 148, 149	mp3an13 1315	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
151	86, 150	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
152	151	adantr 465	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
153	109	fveq2d 5868	. . . . . . . . . . . . . . 15 $/\$ $\$
154	153	ad2antrl 727	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
155	53, 112	opth 4721	. . . . . . . . . . . . . . . . . . 19 $/\$
156	155	simprbi 464	. . . . . . . . . . . . . . . . . 18
157	156	necon3i 2707	. . . . . . . . . . . . . . . . 17
158		hashprg 12424	. . . . . . . . . . . . . . . . . 18 $/\$
159	105, 106, 158	mp2an 672	. . . . . . . . . . . . . . . . 17
160	157, 159	sylib 196	. . . . . . . . . . . . . . . 16
161	160	oveq1d 6297	. . . . . . . . . . . . . . 15 $\$ $\$
162	161	ad2antll 728	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
163	152, 154, 162	3eqtr3rd 2517	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
164	146, 163	breqtrd 4471	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
165	84, 94, 97, 133, 164	ltletrd 9737	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	84, 165	gtned 9715	. . . . . . . . . 10 $/\$ $/\$ $/\$
167	166	ex 434	. . . . . . . . 9 $/\$ $/\$
168	167	exlimdv 1700	. . . . . . . 8 $/\$ $/\$
169	168	exlimdvv 1701	. . . . . . 7 $/\$ $/\$
170	83, 169	syl5bi 217	. . . . . 6 $/\$
171	170	necon4bd 2689	. . . . 5 $/\$
172	171	imp 429	. . . 4 $/\$ $/\$
173		dffun4 5598	. . . 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 973

wal 1377

wceq 1379

wex 1596

wcel 1767

wne 2662

wral 2814

wrex 2815

cvv 3113 $\$ cdif 3473

cun 3474

cin 3475

wss 3476

c0 3785

csn 4027

cpr 4029

cop 4033 class class class wbr 4447

cxp 4997

cdm 4999

wrel 5004

wfun 5580

wfn 5581

cfv 5586 (class class class)co 6282

cdom 7511

cfn 7513

cr 9487

c1 9489

caddc 9491

clt 9624

cle 9625

c2 10581

cn0 10791

chash 12369

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4558 ax-sep 4568 ax-nul 4576 ax-pow 4625 ax-pr 4686 ax-un 6574 ax-cnex 9544 ax-resscn 9545 ax-1cn 9546 ax-icn 9547 ax-addcl 9548 ax-addrcl 9549 ax-mulcl 9550 ax-mulrcl 9551 ax-mulcom 9552 ax-addass 9553 ax-mulass 9554 ax-distr 9555 ax-i2m1 9556 ax-1ne0 9557 ax-1rid 9558 ax-rnegex 9559 ax-rrecex 9560 ax-cnre 9561 ax-pre-lttri 9562 ax-pre-lttrn 9563 ax-pre-ltadd 9564 ax-pre-mulgt0 9565

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2819 df-rex 2820 df-reu 2821 df-rmo 2822 df-rab 2823 df-v 3115 df-sbc 3332 df-csb 3436 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-pss 3492 df-nul 3786 df-if 3940 df-pw 4012 df-sn 4028 df-pr 4030 df-tp 4032 df-op 4034 df-uni 4246 df-int 4283 df-iun 4327 df-br 4448 df-opab 4506 df-mpt 4507 df-tr 4541 df-eprel 4791 df-id 4795 df-po 4800 df-so 4801 df-fr 4838 df-we 4840 df-ord 4881 df-on 4882 df-lim 4883 df-suc 4884 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-rn 5010 df-res 5011 df-ima 5012 df-iota 5549 df-fun 5588 df-fn 5589 df-f 5590 df-f1 5591 df-fo 5592 df-f1o 5593 df-fv 5594 df-riota 6243 df-ov 6285 df-oprab 6286 df-mpt2 6287 df-om 6679 df-1st 6781 df-2nd 6782 df-recs 7039 df-rdg 7073 df-1o 7127 df-oadd 7131 df-er 7308 df-en 7514 df-dom 7515 df-sdom 7516 df-fin 7517 df-card 8316 df-cda 8544 df-pnf 9626 df-mnf 9627 df-xr 9628 df-ltxr 9629 df-le 9630 df-sub 9803 df-neg 9804 df-nn 10533 df-2 10590 df-n0 10792 df-z 10861 df-uz 11079 df-fz 11669 df-hash 12370

This theorem is referenced by: hashfzdm 12460 hashfirdm 12462 cusgrasizeinds 24152

W3C validator