hashfun - Metamath Proof Explorer

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

Theorem hashfun 12642

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 5630	. . 3
2		hashfn 12586	. . 3
3	1, 2	sylbi 200	. 2
4		dmfi 7880	. . . . . . . . . . 11
5		hashcl 12570	. . . . . . . . . . 11
6	4, 5	syl 17	. . . . . . . . . 10
7	6	nn0red 10955	. . . . . . . . 9
8	7	adantr 471	. . . . . . . 8 $/\$
9		df-rel 4860	. . . . . . . . . . . . 13
10		dfss3 3434	. . . . . . . . . . . . 13
11	9, 10	bitri 257	. . . . . . . . . . . 12
12	11	notbii 302	. . . . . . . . . . 11
13		rexnal 2848	. . . . . . . . . . 11
14	12, 13	bitr4i 260	. . . . . . . . . 10
15		dmun 5060	. . . . . . . . . . . . . . . 16 $\$ $\$
16	15	fveq2i 5891	. . . . . . . . . . . . . . 15 $\$ $\$
17		dmsnn0 5320	. . . . . . . . . . . . . . . . . . . . 21
18	17	biimpri 211	. . . . . . . . . . . . . . . . . . . 20
19	18	necon1bi 2664	. . . . . . . . . . . . . . . . . . 19
20	19	3ad2ant3 1037	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
21	20	uneq2d 3600	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
22		un0 3771	. . . . . . . . . . . . . . . . 17 $\$ $\$
23	21, 22	syl6eq 2512	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
24	23	fveq2d 5892	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
25	16, 24	syl5eq 2508	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
26		diffi 7829	. . . . . . . . . . . . . . . . . . 19 $\$
27		dmfi 7880	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
28	26, 27	syl 17	. . . . . . . . . . . . . . . . . 18 $\$
29		hashcl 12570	. . . . . . . . . . . . . . . . . 18 $\$ $\$
30	28, 29	syl 17	. . . . . . . . . . . . . . . . 17 $\$
31	30	nn0red 10955	. . . . . . . . . . . . . . . 16 $\$
32		hashcl 12570	. . . . . . . . . . . . . . . . . 18 $\$ $\$
33	26, 32	syl 17	. . . . . . . . . . . . . . . . 17 $\$
34	33	nn0red 10955	. . . . . . . . . . . . . . . 16 $\$
35		peano2re 9832	. . . . . . . . . . . . . . . . 17 $\$ $\$
36	34, 35	syl 17	. . . . . . . . . . . . . . . 16 $\$
37		fidomdm 7879	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
38	26, 37	syl 17	. . . . . . . . . . . . . . . . 17 $\$ $\$
39		hashdom 12590	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
40	28, 26, 39	syl2anc 671	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$
41	38, 40	mpbird 240	. . . . . . . . . . . . . . . 16 $\$ $\$
42	34	ltp1d 10565	. . . . . . . . . . . . . . . 16 $\$ $\$
43	31, 34, 36, 41, 42	lelttrd 9819	. . . . . . . . . . . . . . 15 $\$ $\$
44	43	3ad2ant1 1035	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
45	25, 44	eqbrtrd 4437	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
46		snfi 7676	. . . . . . . . . . . . . . . . 17
47		incom 3637	. . . . . . . . . . . . . . . . . 18 $\$ $\$
48		disjdif 3851	. . . . . . . . . . . . . . . . . 18 $\$
49	47, 48	eqtri 2484	. . . . . . . . . . . . . . . . 17 $\$
50		hashun 12593	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $\$ $\$ $\$
51	46, 49, 50	mp3an23 1365	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
52	26, 51	syl 17	. . . . . . . . . . . . . . 15 $\$ $\$
53		vex 3060	. . . . . . . . . . . . . . . . 17
54		hashsng 12581	. . . . . . . . . . . . . . . . 17
55	53, 54	ax-mp 5	. . . . . . . . . . . . . . . 16
56	55	oveq2i 6326	. . . . . . . . . . . . . . 15 $\$ $\$
57	52, 56	syl6req 2513	. . . . . . . . . . . . . 14 $\$ $\$
58	57	3ad2ant1 1035	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
59	45, 58	breqtrd 4441	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
60		difsnid 4131	. . . . . . . . . . . . . . 15 $\$
61	60	dmeqd 5056	. . . . . . . . . . . . . 14 $\$
62	61	fveq2d 5892	. . . . . . . . . . . . 13 $\$
63	62	3ad2ant2 1036	. . . . . . . . . . . 12 $/\$ $/\$ $\$
64	60	fveq2d 5892	. . . . . . . . . . . . 13 $\$
65	64	3ad2ant2 1036	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66	59, 63, 65	3brtr3d 4446	. . . . . . . . . . 11 $/\$ $/\$
67	66	rexlimdv3a 2893	. . . . . . . . . 10
68	14, 67	syl5bi 225	. . . . . . . . 9
69	68	imp 435	. . . . . . . 8 $/\$
70	8, 69	gtned 9796	. . . . . . 7 $/\$
71	70	ex 440	. . . . . 6
72	71	necon4bd 2656	. . . . 5
73	72	imp 435	. . . 4 $/\$
74		2nalexn 1711	. . . . . . . 8 $/\$ $/\$
75		df-ne 2635	. . . . . . . . . . . . 13
76	75	anbi2i 705	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
77		annim 431	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
78	76, 77	bitri 257	. . . . . . . . . . 11 $/\$ $/\$ $/\$
79	78	exbii 1729	. . . . . . . . . 10 $/\$ $/\$ $/\$
80		exnal 1710	. . . . . . . . . 10 $/\$ $/\$
81	79, 80	bitr2i 258	. . . . . . . . 9 $/\$ $/\$ $/\$
82	81	2exbii 1730	. . . . . . . 8 $/\$ $/\$ $/\$
83	74, 82	bitri 257	. . . . . . 7 $/\$ $/\$ $/\$
84	7	adantr 471	. . . . . . . . . . 11 $/\$ $/\$ $/\$
85		2re 10707	. . . . . . . . . . . . 13
86		diffi 7829	. . . . . . . . . . . . . . . . 17 $\$
87		dmfi 7880	. . . . . . . . . . . . . . . . 17 $\$ $\$
88	86, 87	syl 17	. . . . . . . . . . . . . . . 16 $\$
89		hashcl 12570	. . . . . . . . . . . . . . . 16 $\$ $\$
90	88, 89	syl 17	. . . . . . . . . . . . . . 15 $\$
91	90	nn0red 10955	. . . . . . . . . . . . . 14 $\$
92	91	adantr 471	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
93		readdcl 9648	. . . . . . . . . . . . 13 $/\$ $\$ $\$
94	85, 92, 93	sylancr 674	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
95		hashcl 12570	. . . . . . . . . . . . . 14
96	95	nn0red 10955	. . . . . . . . . . . . 13
97	96	adantr 471	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98		1re 9668	. . . . . . . . . . . . . . 15
99		readdcl 9648	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
100	98, 91, 99	sylancr 674	. . . . . . . . . . . . . 14 $\$
101	100	adantr 471	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
102	85, 91, 93	sylancr 674	. . . . . . . . . . . . . 14 $\$
103	102	adantr 471	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
104		dmun 5060	. . . . . . . . . . . . . . . . . 18 $\$ $\$
105		opex 4678	. . . . . . . . . . . . . . . . . . . . 21
106		opex 4678	. . . . . . . . . . . . . . . . . . . . 21
107	105, 106	prss 4139	. . . . . . . . . . . . . . . . . . . 20 $/\$
108		undif 3860	. . . . . . . . . . . . . . . . . . . 20 $\$
109	107, 108	sylbb 202	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
110	109	dmeqd 5056	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
111	104, 110	syl5reqr 2511	. . . . . . . . . . . . . . . . 17 $/\$ $\$
112		vex 3060	. . . . . . . . . . . . . . . . . . . 20
113		vex 3060	. . . . . . . . . . . . . . . . . . . 20
114	112, 113	dmprop 5330	. . . . . . . . . . . . . . . . . . 19
115		dfsn2 3993	. . . . . . . . . . . . . . . . . . 19
116	114, 115	eqtr4i 2487	. . . . . . . . . . . . . . . . . 18
117	116	uneq1i 3596	. . . . . . . . . . . . . . . . 17 $\$ $\$
118	111, 117	syl6eq 2512	. . . . . . . . . . . . . . . 16 $/\$ $\$
119	118	fveq2d 5892	. . . . . . . . . . . . . . 15 $/\$ $\$
120	119	ad2antrl 739	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
121		hashun2 12594	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$ $\$
122	46, 88, 121	sylancr 674	. . . . . . . . . . . . . . . 16 $\$ $\$
123	55	oveq1i 6325	. . . . . . . . . . . . . . . 16 $\$ $\$
124	122, 123	syl6breq 4456	. . . . . . . . . . . . . . 15 $\$ $\$
125	124	adantr 471	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
126	120, 125	eqbrtrd 4437	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
127		1lt2 10805	. . . . . . . . . . . . . . 15
128		ltadd1 10109	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$ $\$
129	98, 85, 128	mp3an12 1363	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
130	91, 129	syl 17	. . . . . . . . . . . . . . 15 $\$ $\$
131	127, 130	mpbii 216	. . . . . . . . . . . . . 14 $\$ $\$
132	131	adantr 471	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
133	84, 101, 103, 126, 132	lelttrd 9819	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
134		fidomdm 7879	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
135	86, 134	syl 17	. . . . . . . . . . . . . . . 16 $\$ $\$
136		hashdom 12590	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
137	88, 86, 136	syl2anc 671	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
138	135, 137	mpbird 240	. . . . . . . . . . . . . . 15 $\$ $\$
139		hashcl 12570	. . . . . . . . . . . . . . . . . 18 $\$ $\$
140	86, 139	syl 17	. . . . . . . . . . . . . . . . 17 $\$
141	140	nn0red 10955	. . . . . . . . . . . . . . . 16 $\$
142		leadd2 10111	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
143	85, 142	mp3an3 1362	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
144	91, 141, 143	syl2anc 671	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$
145	138, 144	mpbid 215	. . . . . . . . . . . . . 14 $\$ $\$
146	145	adantr 471	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
147		prfi 7872	. . . . . . . . . . . . . . . . 17
148		disjdif 3851	. . . . . . . . . . . . . . . . 17 $\$
149		hashun 12593	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $\$ $\$
150	147, 148, 149	mp3an13 1364	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
151	86, 150	syl 17	. . . . . . . . . . . . . . 15 $\$ $\$
152	151	adantr 471	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
153	109	fveq2d 5892	. . . . . . . . . . . . . . 15 $/\$ $\$
154	153	ad2antrl 739	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
155	53, 112	opth 4690	. . . . . . . . . . . . . . . . . . 19 $/\$
156	155	simprbi 470	. . . . . . . . . . . . . . . . . 18
157	156	necon3i 2668	. . . . . . . . . . . . . . . . 17
158		hashprg 12604	. . . . . . . . . . . . . . . . . 18 $/\$
159	105, 106, 158	mp2an 683	. . . . . . . . . . . . . . . . 17
160	157, 159	sylib 201	. . . . . . . . . . . . . . . 16
161	160	oveq1d 6330	. . . . . . . . . . . . . . 15 $\$ $\$
162	161	ad2antll 740	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
163	152, 154, 162	3eqtr3rd 2505	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
164	146, 163	breqtrd 4441	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
165	84, 94, 97, 133, 164	ltletrd 9821	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	84, 165	gtned 9796	. . . . . . . . . 10 $/\$ $/\$ $/\$
167	166	ex 440	. . . . . . . . 9 $/\$ $/\$
168	167	exlimdv 1790	. . . . . . . 8 $/\$ $/\$
169	168	exlimdvv 1791	. . . . . . 7 $/\$ $/\$
170	83, 169	syl5bi 225	. . . . . 6 $/\$
171	170	necon4bd 2656	. . . . 5 $/\$
172	171	imp 435	. . . 4 $/\$ $/\$
173		dffun4 5613	. . . 4 $/\$ $/\$
174	73, 172, 173	sylanbrc 675	. . 3 $/\$
175	174	ex 440	. 2
176	3, 175	impbid2 209	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 189 $/\$ wa 375 $/\$ w3a 991

wal 1453

wceq 1455

wex 1674

wcel 1898

wne 2633

wral 2749

wrex 2750

cvv 3057 $\$ cdif 3413

cun 3414

cin 3415

wss 3416

c0 3743

csn 3980

cpr 3982

cop 3986 class class class wbr 4416

cxp 4851

cdm 4853

wrel 4858

wfun 5595

wfn 5596

cfv 5601 (class class class)co 6315

cdom 7593

cfn 7595

cr 9564

c1 9566

caddc 9568

clt 9701

cle 9702

c2 10687

cn0 10898

chash 12547

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-8 1900 ax-9 1907 ax-10 1926 ax-11 1931 ax-12 1944 ax-13 2102 ax-ext 2442 ax-rep 4529 ax-sep 4539 ax-nul 4548 ax-pow 4595 ax-pr 4653 ax-un 6610 ax-cnex 9621 ax-resscn 9622 ax-1cn 9623 ax-icn 9624 ax-addcl 9625 ax-addrcl 9626 ax-mulcl 9627 ax-mulrcl 9628 ax-mulcom 9629 ax-addass 9630 ax-mulass 9631 ax-distr 9632 ax-i2m1 9633 ax-1ne0 9634 ax-1rid 9635 ax-rnegex 9636 ax-rrecex 9637 ax-cnre 9638 ax-pre-lttri 9639 ax-pre-lttrn 9640 ax-pre-ltadd 9641 ax-pre-mulgt0 9642

This theorem depends on definitions: df-bi 190 df-or 376 df-an 377 df-3or 992 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-eu 2314 df-mo 2315 df-clab 2449 df-cleq 2455 df-clel 2458 df-nfc 2592 df-ne 2635 df-nel 2636 df-ral 2754 df-rex 2755 df-reu 2756 df-rmo 2757 df-rab 2758 df-v 3059 df-sbc 3280 df-csb 3376 df-dif 3419 df-un 3421 df-in 3423 df-ss 3430 df-pss 3432 df-nul 3744 df-if 3894 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4213 df-int 4249 df-iun 4294 df-br 4417 df-opab 4476 df-mpt 4477 df-tr 4512 df-eprel 4764 df-id 4768 df-po 4774 df-so 4775 df-fr 4812 df-we 4814 df-xp 4859 df-rel 4860 df-cnv 4861 df-co 4862 df-dm 4863 df-rn 4864 df-res 4865 df-ima 4866 df-pred 5399 df-ord 5445 df-on 5446 df-lim 5447 df-suc 5448 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6277 df-ov 6318 df-oprab 6319 df-mpt2 6320 df-om 6720 df-1st 6820 df-2nd 6821 df-wrecs 7054 df-recs 7116 df-rdg 7154 df-1o 7208 df-oadd 7212 df-er 7389 df-en 7596 df-dom 7597 df-sdom 7598 df-fin 7599 df-card 8399 df-cda 8624 df-pnf 9703 df-mnf 9704 df-xr 9705 df-ltxr 9706 df-le 9707 df-sub 9888 df-neg 9889 df-nn 10638 df-2 10696 df-n0 10899 df-z 10967 df-uz 11189 df-fz 11814 df-hash 12548

This theorem is referenced by: hashfzdm 12645 hashfirdm 12647 cusgrasizeinds 25253

W3C validator