hashfun - Metamath Proof Explorer

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

Theorem hashfun 11655

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 5441	. . 3
2		hashfn 11604	. . 3
3	1, 2	sylbi 188	. 2
4		dmfi 7348	. . . . . . . . . . 11
5		hashcl 11594	. . . . . . . . . . 11
6	4, 5	syl 16	. . . . . . . . . 10
7	6	nn0red 10231	. . . . . . . . 9
8	7	adantr 452	. . . . . . . 8 $/\$
9		df-rel 4844	. . . . . . . . . . . . 13
10		dfss3 3298	. . . . . . . . . . . . 13
11	9, 10	bitri 241	. . . . . . . . . . . 12
12	11	notbii 288	. . . . . . . . . . 11
13		rexnal 2677	. . . . . . . . . . 11
14	12, 13	bitr4i 244	. . . . . . . . . 10
15		dmun 5035	. . . . . . . . . . . . . . . 16 $\$ $\$
16	15	fveq2i 5690	. . . . . . . . . . . . . . 15 $\$ $\$
17		dmsnn0 5294	. . . . . . . . . . . . . . . . . . . . 21
18	17	biimpri 198	. . . . . . . . . . . . . . . . . . . 20
19	18	necon1bi 2610	. . . . . . . . . . . . . . . . . . 19
20	19	3ad2ant3 980	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
21	20	uneq2d 3461	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
22		un0 3612	. . . . . . . . . . . . . . . . 17 $\$ $\$
23	21, 22	syl6eq 2452	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
24	23	fveq2d 5691	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
25	16, 24	syl5eq 2448	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
26		diffi 7298	. . . . . . . . . . . . . . . . . . 19 $\$
27		dmfi 7348	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
28	26, 27	syl 16	. . . . . . . . . . . . . . . . . 18 $\$
29		hashcl 11594	. . . . . . . . . . . . . . . . . 18 $\$ $\$
30	28, 29	syl 16	. . . . . . . . . . . . . . . . 17 $\$
31	30	nn0red 10231	. . . . . . . . . . . . . . . 16 $\$
32		hashcl 11594	. . . . . . . . . . . . . . . . . 18 $\$ $\$
33	26, 32	syl 16	. . . . . . . . . . . . . . . . 17 $\$
34	33	nn0red 10231	. . . . . . . . . . . . . . . 16 $\$
35		peano2re 9195	. . . . . . . . . . . . . . . . 17 $\$ $\$
36	34, 35	syl 16	. . . . . . . . . . . . . . . 16 $\$
37		fidomdm 7347	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
38	26, 37	syl 16	. . . . . . . . . . . . . . . . 17 $\$ $\$
39		hashdom 11608	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
40	28, 26, 39	syl2anc 643	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$
41	38, 40	mpbird 224	. . . . . . . . . . . . . . . 16 $\$ $\$
42	34	ltp1d 9897	. . . . . . . . . . . . . . . 16 $\$ $\$
43	31, 34, 36, 41, 42	lelttrd 9184	. . . . . . . . . . . . . . 15 $\$ $\$
44	43	3ad2ant1 978	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
45	25, 44	eqbrtrd 4192	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
46		snfi 7146	. . . . . . . . . . . . . . . . 17
47		incom 3493	. . . . . . . . . . . . . . . . . 18 $\$ $\$
48		disjdif 3660	. . . . . . . . . . . . . . . . . 18 $\$
49	47, 48	eqtri 2424	. . . . . . . . . . . . . . . . 17 $\$
50		hashun 11611	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $\$ $\$ $\$
51	46, 49, 50	mp3an23 1271	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
52	26, 51	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
53		vex 2919	. . . . . . . . . . . . . . . . 17
54		hashsng 11602	. . . . . . . . . . . . . . . . 17
55	53, 54	ax-mp 8	. . . . . . . . . . . . . . . 16
56	55	oveq2i 6051	. . . . . . . . . . . . . . 15 $\$ $\$
57	52, 56	syl6req 2453	. . . . . . . . . . . . . 14 $\$ $\$
58	57	3ad2ant1 978	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
59	45, 58	breqtrd 4196	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
60		difsnid 3904	. . . . . . . . . . . . . . 15 $\$
61	60	dmeqd 5031	. . . . . . . . . . . . . 14 $\$
62	61	fveq2d 5691	. . . . . . . . . . . . 13 $\$
63	62	3ad2ant2 979	. . . . . . . . . . . 12 $/\$ $/\$ $\$
64	60	fveq2d 5691	. . . . . . . . . . . . 13 $\$
65	64	3ad2ant2 979	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66	59, 63, 65	3brtr3d 4201	. . . . . . . . . . 11 $/\$ $/\$
67	66	rexlimdv3a 2792	. . . . . . . . . 10
68	14, 67	syl5bi 209	. . . . . . . . 9
69	68	imp 419	. . . . . . . 8 $/\$
70	8, 69	gtned 9164	. . . . . . 7 $/\$
71	70	ex 424	. . . . . 6
72	71	necon4bd 2629	. . . . 5
73	72	imp 419	. . . 4 $/\$
74		2nalexn 1579	. . . . . . . 8 $/\$ $/\$
75		df-ne 2569	. . . . . . . . . . . . 13
76	75	anbi2i 676	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
77		annim 415	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
78	76, 77	bitri 241	. . . . . . . . . . 11 $/\$ $/\$ $/\$
79	78	exbii 1589	. . . . . . . . . 10 $/\$ $/\$ $/\$
80		exnal 1580	. . . . . . . . . 10 $/\$ $/\$
81	79, 80	bitr2i 242	. . . . . . . . 9 $/\$ $/\$ $/\$
82	81	2exbii 1590	. . . . . . . 8 $/\$ $/\$ $/\$
83	74, 82	bitri 241	. . . . . . 7 $/\$ $/\$ $/\$
84	7	adantr 452	. . . . . . . . . . 11 $/\$ $/\$ $/\$
85		2re 10025	. . . . . . . . . . . . 13
86		diffi 7298	. . . . . . . . . . . . . . . . 17 $\$
87		dmfi 7348	. . . . . . . . . . . . . . . . 17 $\$ $\$
88	86, 87	syl 16	. . . . . . . . . . . . . . . 16 $\$
89		hashcl 11594	. . . . . . . . . . . . . . . 16 $\$ $\$
90	88, 89	syl 16	. . . . . . . . . . . . . . 15 $\$
91	90	nn0red 10231	. . . . . . . . . . . . . 14 $\$
92	91	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
93		readdcl 9029	. . . . . . . . . . . . 13 $/\$ $\$ $\$
94	85, 92, 93	sylancr 645	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
95		hashcl 11594	. . . . . . . . . . . . . 14
96	95	nn0red 10231	. . . . . . . . . . . . 13
97	96	adantr 452	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98		1re 9046	. . . . . . . . . . . . . . 15
99		readdcl 9029	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
100	98, 91, 99	sylancr 645	. . . . . . . . . . . . . 14 $\$
101	100	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
102	85, 91, 93	sylancr 645	. . . . . . . . . . . . . 14 $\$
103	102	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
104		dmun 5035	. . . . . . . . . . . . . . . . . 18 $\$ $\$
105		opex 4387	. . . . . . . . . . . . . . . . . . . . . 22
106		opex 4387	. . . . . . . . . . . . . . . . . . . . . 22
107	105, 106	prss 3912	. . . . . . . . . . . . . . . . . . . . 21 $/\$
108		undif 3668	. . . . . . . . . . . . . . . . . . . . 21 $\$
109	107, 108	bitri 241	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$
110	109	biimpi 187	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
111	110	dmeqd 5031	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
112	104, 111	syl5reqr 2451	. . . . . . . . . . . . . . . . 17 $/\$ $\$
113		vex 2919	. . . . . . . . . . . . . . . . . . . 20
114		vex 2919	. . . . . . . . . . . . . . . . . . . 20
115	113, 114	dmprop 5304	. . . . . . . . . . . . . . . . . . 19
116		dfsn2 3788	. . . . . . . . . . . . . . . . . . 19
117	115, 116	eqtr4i 2427	. . . . . . . . . . . . . . . . . 18
118	117	uneq1i 3457	. . . . . . . . . . . . . . . . 17 $\$ $\$
119	112, 118	syl6eq 2452	. . . . . . . . . . . . . . . 16 $/\$ $\$
120	119	fveq2d 5691	. . . . . . . . . . . . . . 15 $/\$ $\$
121	120	ad2antrl 709	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
122		hashun2 11612	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$ $\$
123	46, 88, 122	sylancr 645	. . . . . . . . . . . . . . . 16 $\$ $\$
124	55	oveq1i 6050	. . . . . . . . . . . . . . . 16 $\$ $\$
125	123, 124	syl6breq 4211	. . . . . . . . . . . . . . 15 $\$ $\$
126	125	adantr 452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
127	121, 126	eqbrtrd 4192	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
128		1lt2 10098	. . . . . . . . . . . . . . 15
129		ltadd1 9451	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$ $\$
130	98, 85, 129	mp3an12 1269	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
131	91, 130	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
132	128, 131	mpbii 203	. . . . . . . . . . . . . 14 $\$ $\$
133	132	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
134	84, 101, 103, 127, 133	lelttrd 9184	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
135		fidomdm 7347	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
136	86, 135	syl 16	. . . . . . . . . . . . . . . 16 $\$ $\$
137		hashdom 11608	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
138	88, 86, 137	syl2anc 643	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
139	136, 138	mpbird 224	. . . . . . . . . . . . . . 15 $\$ $\$
140		hashcl 11594	. . . . . . . . . . . . . . . . . 18 $\$ $\$
141	86, 140	syl 16	. . . . . . . . . . . . . . . . 17 $\$
142	141	nn0red 10231	. . . . . . . . . . . . . . . 16 $\$
143		leadd2 9453	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
144	85, 143	mp3an3 1268	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
145	91, 142, 144	syl2anc 643	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$
146	139, 145	mpbid 202	. . . . . . . . . . . . . 14 $\$ $\$
147	146	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
148		prfi 7340	. . . . . . . . . . . . . . . . 17
149		disjdif 3660	. . . . . . . . . . . . . . . . 17 $\$
150		hashun 11611	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $\$ $\$
151	148, 149, 150	mp3an13 1270	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
152	86, 151	syl 16	. . . . . . . . . . . . . . 15 $\$ $\$
153	152	adantr 452	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
154	110	fveq2d 5691	. . . . . . . . . . . . . . 15 $/\$ $\$
155	154	ad2antrl 709	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
156	53, 113	opth 4395	. . . . . . . . . . . . . . . . . . 19 $/\$
157	156	simprbi 451	. . . . . . . . . . . . . . . . . 18
158	157	necon3i 2606	. . . . . . . . . . . . . . . . 17
159		hashprg 11621	. . . . . . . . . . . . . . . . . 18 $/\$
160	105, 106, 159	mp2an 654	. . . . . . . . . . . . . . . . 17
161	158, 160	sylib 189	. . . . . . . . . . . . . . . 16
162	161	oveq1d 6055	. . . . . . . . . . . . . . 15 $\$ $\$
163	162	ad2antll 710	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
164	153, 155, 163	3eqtr3rd 2445	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
165	147, 164	breqtrd 4196	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
166	84, 94, 97, 134, 165	ltletrd 9186	. . . . . . . . . . 11 $/\$ $/\$ $/\$
167	84, 166	gtned 9164	. . . . . . . . . 10 $/\$ $/\$ $/\$
168	167	ex 424	. . . . . . . . 9 $/\$ $/\$
169	168	exlimdv 1643	. . . . . . . 8 $/\$ $/\$
170	169	exlimdvv 1644	. . . . . . 7 $/\$ $/\$
171	83, 170	syl5bi 209	. . . . . 6 $/\$
172	171	necon4bd 2629	. . . . 5 $/\$
173	172	imp 419	. . . 4 $/\$ $/\$
174		dffun4 5425	. . . 4 $/\$ $/\$
175	73, 173, 174	sylanbrc 646	. . 3 $/\$
176	175	ex 424	. 2
177	3, 176	impbid2 196	1

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wal 1546

wex 1547

wceq 1649

wcel 1721

wne 2567

wral 2666

wrex 2667

cvv 2916 $\$ cdif 3277

cun 3278

cin 3279

wss 3280

c0 3588

csn 3774

cpr 3775

cop 3777 class class class wbr 4172

cxp 4835

cdm 4837

wrel 4842

wfun 5407

wfn 5408

cfv 5413 (class class class)co 6040

cdom 7066

cfn 7068

cr 8945

c1 8947

caddc 8949

clt 9076

cle 9077

c2 10005

cn0 10177

chash 11573

This theorem is referenced by: cusgrasizeinds 21438 hashfirdm 27996 hashfzdm 27997

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2385 ax-rep 4280 ax-sep 4290 ax-nul 4298 ax-pow 4337 ax-pr 4363 ax-un 4660 ax-cnex 9002 ax-resscn 9003 ax-1cn 9004 ax-icn 9005 ax-addcl 9006 ax-addrcl 9007 ax-mulcl 9008 ax-mulrcl 9009 ax-mulcom 9010 ax-addass 9011 ax-mulass 9012 ax-distr 9013 ax-i2m1 9014 ax-1ne0 9015 ax-1rid 9016 ax-rnegex 9017 ax-rrecex 9018 ax-cnre 9019 ax-pre-lttri 9020 ax-pre-lttrn 9021 ax-pre-ltadd 9022 ax-pre-mulgt0 9023

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3or 937 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2258 df-mo 2259 df-clab 2391 df-cleq 2397 df-clel 2400 df-nfc 2529 df-ne 2569 df-nel 2570 df-ral 2671 df-rex 2672 df-reu 2673 df-rmo 2674 df-rab 2675 df-v 2918 df-sbc 3122 df-csb 3212 df-dif 3283 df-un 3285 df-in 3287 df-ss 3294 df-pss 3296 df-nul 3589 df-if 3700 df-pw 3761 df-sn 3780 df-pr 3781 df-tp 3782 df-op 3783 df-uni 3976 df-int 4011 df-iun 4055 df-br 4173 df-opab 4227 df-mpt 4228 df-tr 4263 df-eprel 4454 df-id 4458 df-po 4463 df-so 4464 df-fr 4501 df-we 4503 df-ord 4544 df-on 4545 df-lim 4546 df-suc 4547 df-om 4805 df-xp 4843 df-rel 4844 df-cnv 4845 df-co 4846 df-dm 4847 df-rn 4848 df-res 4849 df-ima 4850 df-iota 5377 df-fun 5415 df-fn 5416 df-f 5417 df-f1 5418 df-fo 5419 df-f1o 5420 df-fv 5421 df-ov 6043 df-oprab 6044 df-mpt2 6045 df-1st 6308 df-2nd 6309 df-riota 6508 df-recs 6592 df-rdg 6627 df-1o 6683 df-oadd 6687 df-er 6864 df-en 7069 df-dom 7070 df-sdom 7071 df-fin 7072 df-card 7782 df-cda 8004 df-pnf 9078 df-mnf 9079 df-xr 9080 df-ltxr 9081 df-le 9082 df-sub 9249 df-neg 9250 df-nn 9957 df-2 10014 df-n0 10178 df-z 10239 df-uz 10445 df-fz 11000 df-hash 11574

W3C validator