hashfun - Metamath Proof Explorer

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

Theorem hashfun 12557

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 5573	. . 3
2		hashfn 12504	. . 3
3	1, 2	sylbi 198	. 2
4		dmfi 7807	. . . . . . . . . . 11
5		hashcl 12488	. . . . . . . . . . 11
6	4, 5	syl 17	. . . . . . . . . 10
7	6	nn0red 10877	. . . . . . . . 9
8	7	adantr 466	. . . . . . . 8 $/\$
9		df-rel 4803	. . . . . . . . . . . . 13
10		dfss3 3397	. . . . . . . . . . . . 13
11	9, 10	bitri 252	. . . . . . . . . . . 12
12	11	notbii 297	. . . . . . . . . . 11
13		rexnal 2813	. . . . . . . . . . 11
14	12, 13	bitr4i 255	. . . . . . . . . 10
15		dmun 5003	. . . . . . . . . . . . . . . 16 $\$ $\$
16	15	fveq2i 5828	. . . . . . . . . . . . . . 15 $\$ $\$
17		dmsnn0 5263	. . . . . . . . . . . . . . . . . . . . 21
18	17	biimpri 209	. . . . . . . . . . . . . . . . . . . 20
19	18	necon1bi 2629	. . . . . . . . . . . . . . . . . . 19
20	19	3ad2ant3 1028	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
21	20	uneq2d 3563	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$
22		un0 3732	. . . . . . . . . . . . . . . . 17 $\$ $\$
23	21, 22	syl6eq 2478	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $\$ $\$
24	23	fveq2d 5829	. . . . . . . . . . . . . . 15 $/\$ $/\$ $\$ $\$
25	16, 24	syl5eq 2474	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
26		diffi 7756	. . . . . . . . . . . . . . . . . . 19 $\$
27		dmfi 7807	. . . . . . . . . . . . . . . . . . 19 $\$ $\$
28	26, 27	syl 17	. . . . . . . . . . . . . . . . . 18 $\$
29		hashcl 12488	. . . . . . . . . . . . . . . . . 18 $\$ $\$
30	28, 29	syl 17	. . . . . . . . . . . . . . . . 17 $\$
31	30	nn0red 10877	. . . . . . . . . . . . . . . 16 $\$
32		hashcl 12488	. . . . . . . . . . . . . . . . . 18 $\$ $\$
33	26, 32	syl 17	. . . . . . . . . . . . . . . . 17 $\$
34	33	nn0red 10877	. . . . . . . . . . . . . . . 16 $\$
35		peano2re 9757	. . . . . . . . . . . . . . . . 17 $\$ $\$
36	34, 35	syl 17	. . . . . . . . . . . . . . . 16 $\$
37		fidomdm 7806	. . . . . . . . . . . . . . . . . 18 $\$ $\$ $\$
38	26, 37	syl 17	. . . . . . . . . . . . . . . . 17 $\$ $\$
39		hashdom 12508	. . . . . . . . . . . . . . . . . 18 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
40	28, 26, 39	syl2anc 665	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$ $\$
41	38, 40	mpbird 235	. . . . . . . . . . . . . . . 16 $\$ $\$
42	34	ltp1d 10488	. . . . . . . . . . . . . . . 16 $\$ $\$
43	31, 34, 36, 41, 42	lelttrd 9744	. . . . . . . . . . . . . . 15 $\$ $\$
44	43	3ad2ant1 1026	. . . . . . . . . . . . . 14 $/\$ $/\$ $\$ $\$
45	25, 44	eqbrtrd 4387	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
46		snfi 7604	. . . . . . . . . . . . . . . . 17
47		incom 3598	. . . . . . . . . . . . . . . . . 18 $\$ $\$
48		disjdif 3812	. . . . . . . . . . . . . . . . . 18 $\$
49	47, 48	eqtri 2450	. . . . . . . . . . . . . . . . 17 $\$
50		hashun 12511	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $/\$ $\$ $\$ $\$
51	46, 49, 50	mp3an23 1352	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
52	26, 51	syl 17	. . . . . . . . . . . . . . 15 $\$ $\$
53		vex 3025	. . . . . . . . . . . . . . . . 17
54		hashsng 12499	. . . . . . . . . . . . . . . . 17
55	53, 54	ax-mp 5	. . . . . . . . . . . . . . . 16
56	55	oveq2i 6260	. . . . . . . . . . . . . . 15 $\$ $\$
57	52, 56	syl6req 2479	. . . . . . . . . . . . . 14 $\$ $\$
58	57	3ad2ant1 1026	. . . . . . . . . . . . 13 $/\$ $/\$ $\$ $\$
59	45, 58	breqtrd 4391	. . . . . . . . . . . 12 $/\$ $/\$ $\$ $\$
60		difsnid 4089	. . . . . . . . . . . . . . 15 $\$
61	60	dmeqd 4999	. . . . . . . . . . . . . 14 $\$
62	61	fveq2d 5829	. . . . . . . . . . . . 13 $\$
63	62	3ad2ant2 1027	. . . . . . . . . . . 12 $/\$ $/\$ $\$
64	60	fveq2d 5829	. . . . . . . . . . . . 13 $\$
65	64	3ad2ant2 1027	. . . . . . . . . . . 12 $/\$ $/\$ $\$
66	59, 63, 65	3brtr3d 4396	. . . . . . . . . . 11 $/\$ $/\$
67	66	rexlimdv3a 2858	. . . . . . . . . 10
68	14, 67	syl5bi 220	. . . . . . . . 9
69	68	imp 430	. . . . . . . 8 $/\$
70	8, 69	gtned 9721	. . . . . . 7 $/\$
71	70	ex 435	. . . . . 6
72	71	necon4bd 2621	. . . . 5
73	72	imp 430	. . . 4 $/\$
74		2nalexn 1694	. . . . . . . 8 $/\$ $/\$
75		df-ne 2601	. . . . . . . . . . . . 13
76	75	anbi2i 698	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
77		annim 426	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
78	76, 77	bitri 252	. . . . . . . . . . 11 $/\$ $/\$ $/\$
79	78	exbii 1712	. . . . . . . . . 10 $/\$ $/\$ $/\$
80		exnal 1693	. . . . . . . . . 10 $/\$ $/\$
81	79, 80	bitr2i 253	. . . . . . . . 9 $/\$ $/\$ $/\$
82	81	2exbii 1713	. . . . . . . 8 $/\$ $/\$ $/\$
83	74, 82	bitri 252	. . . . . . 7 $/\$ $/\$ $/\$
84	7	adantr 466	. . . . . . . . . . 11 $/\$ $/\$ $/\$
85		2re 10630	. . . . . . . . . . . . 13
86		diffi 7756	. . . . . . . . . . . . . . . . 17 $\$
87		dmfi 7807	. . . . . . . . . . . . . . . . 17 $\$ $\$
88	86, 87	syl 17	. . . . . . . . . . . . . . . 16 $\$
89		hashcl 12488	. . . . . . . . . . . . . . . 16 $\$ $\$
90	88, 89	syl 17	. . . . . . . . . . . . . . 15 $\$
91	90	nn0red 10877	. . . . . . . . . . . . . 14 $\$
92	91	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
93		readdcl 9573	. . . . . . . . . . . . 13 $/\$ $\$ $\$
94	85, 92, 93	sylancr 667	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
95		hashcl 12488	. . . . . . . . . . . . . 14
96	95	nn0red 10877	. . . . . . . . . . . . 13
97	96	adantr 466	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
98		1re 9593	. . . . . . . . . . . . . . 15
99		readdcl 9573	. . . . . . . . . . . . . . 15 $/\$ $\$ $\$
100	98, 91, 99	sylancr 667	. . . . . . . . . . . . . 14 $\$
101	100	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
102	85, 91, 93	sylancr 667	. . . . . . . . . . . . . 14 $\$
103	102	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
104		dmun 5003	. . . . . . . . . . . . . . . . . 18 $\$ $\$
105		opex 4628	. . . . . . . . . . . . . . . . . . . . 21
106		opex 4628	. . . . . . . . . . . . . . . . . . . . 21
107	105, 106	prss 4097	. . . . . . . . . . . . . . . . . . . 20 $/\$
108		undif 3821	. . . . . . . . . . . . . . . . . . . 20 $\$
109	107, 108	sylbb 200	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$
110	109	dmeqd 4999	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
111	104, 110	syl5reqr 2477	. . . . . . . . . . . . . . . . 17 $/\$ $\$
112		vex 3025	. . . . . . . . . . . . . . . . . . . 20
113		vex 3025	. . . . . . . . . . . . . . . . . . . 20
114	112, 113	dmprop 5273	. . . . . . . . . . . . . . . . . . 19
115		dfsn2 3954	. . . . . . . . . . . . . . . . . . 19
116	114, 115	eqtr4i 2453	. . . . . . . . . . . . . . . . . 18
117	116	uneq1i 3559	. . . . . . . . . . . . . . . . 17 $\$ $\$
118	111, 117	syl6eq 2478	. . . . . . . . . . . . . . . 16 $/\$ $\$
119	118	fveq2d 5829	. . . . . . . . . . . . . . 15 $/\$ $\$
120	119	ad2antrl 732	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
121		hashun2 12512	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$ $\$
122	46, 88, 121	sylancr 667	. . . . . . . . . . . . . . . 16 $\$ $\$
123	55	oveq1i 6259	. . . . . . . . . . . . . . . 16 $\$ $\$
124	122, 123	syl6breq 4406	. . . . . . . . . . . . . . 15 $\$ $\$
125	124	adantr 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
126	120, 125	eqbrtrd 4387	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
127		1lt2 10727	. . . . . . . . . . . . . . 15
128		ltadd1 10032	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $\$ $\$ $\$
129	98, 85, 128	mp3an12 1350	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
130	91, 129	syl 17	. . . . . . . . . . . . . . 15 $\$ $\$
131	127, 130	mpbii 214	. . . . . . . . . . . . . 14 $\$ $\$
132	131	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
133	84, 101, 103, 126, 132	lelttrd 9744	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
134		fidomdm 7806	. . . . . . . . . . . . . . . . 17 $\$ $\$ $\$
135	86, 134	syl 17	. . . . . . . . . . . . . . . 16 $\$ $\$
136		hashdom 12508	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
137	88, 86, 136	syl2anc 665	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$ $\$
138	135, 137	mpbird 235	. . . . . . . . . . . . . . 15 $\$ $\$
139		hashcl 12488	. . . . . . . . . . . . . . . . . 18 $\$ $\$
140	86, 139	syl 17	. . . . . . . . . . . . . . . . 17 $\$
141	140	nn0red 10877	. . . . . . . . . . . . . . . 16 $\$
142		leadd2 10034	. . . . . . . . . . . . . . . . 17 $\$ $/\$ $\$ $/\$ $\$ $\$ $\$ $\$
143	85, 142	mp3an3 1349	. . . . . . . . . . . . . . . 16 $\$ $/\$ $\$ $\$ $\$ $\$ $\$
144	91, 141, 143	syl2anc 665	. . . . . . . . . . . . . . 15 $\$ $\$ $\$ $\$
145	138, 144	mpbid 213	. . . . . . . . . . . . . 14 $\$ $\$
146	145	adantr 466	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$ $\$
147		prfi 7799	. . . . . . . . . . . . . . . . 17
148		disjdif 3812	. . . . . . . . . . . . . . . . 17 $\$
149		hashun 12511	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $/\$ $\$ $\$ $\$
150	147, 148, 149	mp3an13 1351	. . . . . . . . . . . . . . . 16 $\$ $\$ $\$
151	86, 150	syl 17	. . . . . . . . . . . . . . 15 $\$ $\$
152	151	adantr 466	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
153	109	fveq2d 5829	. . . . . . . . . . . . . . 15 $/\$ $\$
154	153	ad2antrl 732	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$
155	53, 112	opth 4638	. . . . . . . . . . . . . . . . . . 19 $/\$
156	155	simprbi 465	. . . . . . . . . . . . . . . . . 18
157	156	necon3i 2633	. . . . . . . . . . . . . . . . 17
158		hashprg 12522	. . . . . . . . . . . . . . . . . 18 $/\$
159	105, 106, 158	mp2an 676	. . . . . . . . . . . . . . . . 17
160	157, 159	sylib 199	. . . . . . . . . . . . . . . 16
161	160	oveq1d 6264	. . . . . . . . . . . . . . 15 $\$ $\$
162	161	ad2antll 733	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $\$ $\$
163	152, 154, 162	3eqtr3rd 2471	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $\$
164	146, 163	breqtrd 4391	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
165	84, 94, 97, 133, 164	ltletrd 9746	. . . . . . . . . . 11 $/\$ $/\$ $/\$
166	84, 165	gtned 9721	. . . . . . . . . 10 $/\$ $/\$ $/\$
167	166	ex 435	. . . . . . . . 9 $/\$ $/\$
168	167	exlimdv 1772	. . . . . . . 8 $/\$ $/\$
169	168	exlimdvv 1773	. . . . . . 7 $/\$ $/\$
170	83, 169	syl5bi 220	. . . . . 6 $/\$
171	170	necon4bd 2621	. . . . 5 $/\$
172	171	imp 430	. . . 4 $/\$ $/\$
173		dffun4 5556	. . . 4 $/\$ $/\$
174	73, 172, 173	sylanbrc 668	. . 3 $/\$
175	174	ex 435	. 2
176	3, 175	impbid2 207	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wal 1435

wceq 1437

wex 1657

wcel 1872

wne 2599

wral 2714

wrex 2715

cvv 3022 $\$ cdif 3376

cun 3377

cin 3378

wss 3379

c0 3704

csn 3941

cpr 3943

cop 3947 class class class wbr 4366

cxp 4794

cdm 4796

wrel 4801

wfun 5538

wfn 5539

cfv 5544 (class class class)co 6249

cdom 7522

cfn 7524

cr 9489

c1 9491

caddc 9493

clt 9626

cle 9627

c2 10610

cn0 10820

chash 12465

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1663 ax-4 1676 ax-5 1752 ax-6 1798 ax-7 1843 ax-8 1874 ax-9 1876 ax-10 1891 ax-11 1896 ax-12 1909 ax-13 2063 ax-ext 2408 ax-rep 4479 ax-sep 4489 ax-nul 4498 ax-pow 4545 ax-pr 4603 ax-un 6541 ax-cnex 9546 ax-resscn 9547 ax-1cn 9548 ax-icn 9549 ax-addcl 9550 ax-addrcl 9551 ax-mulcl 9552 ax-mulrcl 9553 ax-mulcom 9554 ax-addass 9555 ax-mulass 9556 ax-distr 9557 ax-i2m1 9558 ax-1ne0 9559 ax-1rid 9560 ax-rnegex 9561 ax-rrecex 9562 ax-cnre 9563 ax-pre-lttri 9564 ax-pre-lttrn 9565 ax-pre-ltadd 9566 ax-pre-mulgt0 9567

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3or 983 df-3an 984 df-tru 1440 df-ex 1658 df-nf 1662 df-sb 1791 df-eu 2280 df-mo 2281 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2558 df-ne 2601 df-nel 2602 df-ral 2719 df-rex 2720 df-reu 2721 df-rmo 2722 df-rab 2723 df-v 3024 df-sbc 3243 df-csb 3339 df-dif 3382 df-un 3384 df-in 3386 df-ss 3393 df-pss 3395 df-nul 3705 df-if 3855 df-pw 3926 df-sn 3942 df-pr 3944 df-tp 3946 df-op 3948 df-uni 4163 df-int 4199 df-iun 4244 df-br 4367 df-opab 4426 df-mpt 4427 df-tr 4462 df-eprel 4707 df-id 4711 df-po 4717 df-so 4718 df-fr 4755 df-we 4757 df-xp 4802 df-rel 4803 df-cnv 4804 df-co 4805 df-dm 4806 df-rn 4807 df-res 4808 df-ima 4809 df-pred 5342 df-ord 5388 df-on 5389 df-lim 5390 df-suc 5391 df-iota 5508 df-fun 5546 df-fn 5547 df-f 5548 df-f1 5549 df-fo 5550 df-f1o 5551 df-fv 5552 df-riota 6211 df-ov 6252 df-oprab 6253 df-mpt2 6254 df-om 6651 df-1st 6751 df-2nd 6752 df-wrecs 6983 df-recs 7045 df-rdg 7083 df-1o 7137 df-oadd 7141 df-er 7318 df-en 7525 df-dom 7526 df-sdom 7527 df-fin 7528 df-card 8325 df-cda 8549 df-pnf 9628 df-mnf 9629 df-xr 9630 df-ltxr 9631 df-le 9632 df-sub 9813 df-neg 9814 df-nn 10561 df-2 10619 df-n0 10821 df-z 10889 df-uz 11111 df-fz 11736 df-hash 12466

This theorem is referenced by: hashfzdm 12560 hashfirdm 12562 cusgrasizeinds 25146

W3C validator