Theorem hashnexinj

Description: If the number of elements of the domain are greater than the number of elements in a codomain, then there are two different values that map to the same. (Contributed by metakunt, 2-May-2025)

	Ref	Expression
Hypotheses	hashnexinj.1	$$⊢\phi \to A\in \mathrm{Fin}$$
	hashnexinj.2	$$⊢\phi \to B\in \mathrm{Fin}$$
	hashnexinj.3	$$⊢\phi \to \left|B\right|<\left|A\right|$$
	hashnexinj.4	$$⊢\phi \to F:A⟶B$$
Assertion	hashnexinj	$$⊢\phi \to \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashnexinj.1	$$⊢\phi \to A\in \mathrm{Fin}$$
2		hashnexinj.2	$$⊢\phi \to B\in \mathrm{Fin}$$
3		hashnexinj.3	$$⊢\phi \to \left|B\right|<\left|A\right|$$
4		hashnexinj.4	$$⊢\phi \to F:A⟶B$$
5		hashcl	$$⊢B\in \mathrm{Fin}\to \left|B\right|\in {\mathbb{N}}_0$$
6	2 5	syl	$$⊢\phi \to \left|B\right|\in {\mathbb{N}}_0$$
7	6	nn0red	$$⊢\phi \to \left|B\right|\in ℝ$$
8		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
9	1 8	syl	$$⊢\phi \to \left|A\right|\in {\mathbb{N}}_0$$
10	9	nn0red	$$⊢\phi \to \left|A\right|\in ℝ$$
11	7 10	ltnled	$$⊢\phi \to \left(\left|B\right|<\left|A\right|\leftrightarrow \neg \left|A\right|\le \left|B\right|\right)$$
12	3 11	mpbid	$$⊢\phi \to \neg \left|A\right|\le \left|B\right|$$
13		hashdom	$$⊢\left(A\in \mathrm{Fin}\wedge B\in \mathrm{Fin}\right)\to \left(\left|A\right|\le \left|B\right|\leftrightarrow A\preccurlyeq B\right)$$
14	1 2 13	syl2anc	$$⊢\phi \to \left(\left|A\right|\le \left|B\right|\leftrightarrow A\preccurlyeq B\right)$$
15	14	notbid	$$⊢\phi \to \left(\neg \left|A\right|\le \left|B\right|\leftrightarrow \neg A\preccurlyeq B\right)$$
16	15	biimpd	$$⊢\phi \to \left(\neg \left|A\right|\le \left|B\right|\to \neg A\preccurlyeq B\right)$$
17	12 16	mpd	$$⊢\phi \to \neg A\preccurlyeq B$$
18		brdomg	$$⊢B\in \mathrm{Fin}\to \left(A\preccurlyeq B\leftrightarrow \exists ff:A\underset{1-1}{⟶}B\right)$$
19	18	notbid	$$⊢B\in \mathrm{Fin}\to \left(\neg A\preccurlyeq B\leftrightarrow \neg \exists ff:A\underset{1-1}{⟶}B\right)$$
20	19	biimpd	$$⊢B\in \mathrm{Fin}\to \left(\neg A\preccurlyeq B\to \neg \exists ff:A\underset{1-1}{⟶}B\right)$$
21	2 20	syl	$$⊢\phi \to \left(\neg A\preccurlyeq B\to \neg \exists ff:A\underset{1-1}{⟶}B\right)$$
22	17 21	mpd	$$⊢\phi \to \neg \exists ff:A\underset{1-1}{⟶}B$$
23		alnex	$$⊢\forall f\neg f:A\underset{1-1}{⟶}B\leftrightarrow \neg \exists ff:A\underset{1-1}{⟶}B$$
24	22 23	sylibr	$$⊢\phi \to \forall f\neg f:A\underset{1-1}{⟶}B$$
25	2 1 4	elmapdd	$$⊢\phi \to F\in \left(B^A\right)$$
26		f1eq1	$$⊢f=F\to \left(f:A\underset{1-1}{⟶}B\leftrightarrow F:A\underset{1-1}{⟶}B\right)$$
27	26	notbid	$$⊢f=F\to \left(\neg f:A\underset{1-1}{⟶}B\leftrightarrow \neg F:A\underset{1-1}{⟶}B\right)$$
28	27	spcgv	$$⊢F\in \left(B^A\right)\to \left(\forall f\neg f:A\underset{1-1}{⟶}B\to \neg F:A\underset{1-1}{⟶}B\right)$$
29	25 28	syl	$$⊢\phi \to \left(\forall f\neg f:A\underset{1-1}{⟶}B\to \neg F:A\underset{1-1}{⟶}B\right)$$
30	24 29	mpd	$$⊢\phi \to \neg F:A\underset{1-1}{⟶}B$$
31		dff13	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)$$
32		iman	$$⊢\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \neg \left(F\left(x\right)=F\left(y\right)\wedge \neg x=y\right)$$
33		df-ne	$$⊢x\ne y\leftrightarrow \neg x=y$$
34	33	anbi2i	$$⊢\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)\leftrightarrow \left(F\left(x\right)=F\left(y\right)\wedge \neg x=y\right)$$
35	32 34	xchbinxr	$$⊢\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \neg \left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)$$
36	35	2ralbii	$$⊢\forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \forall x\in A\forall y\in A\neg \left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)$$
37		ralnex2	$$⊢\forall x\in A\forall y\in A\neg \left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)\leftrightarrow \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)$$
38	36 37	bitri	$$⊢\forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\leftrightarrow \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)$$
39	38	anbi2i	$$⊢\left(F:A⟶B\wedge \forall x\in A\forall y\in A\left(F\left(x\right)=F\left(y\right)\to x=y\right)\right)\leftrightarrow \left(F:A⟶B\wedge \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)\right)$$
40	31 39	bitri	$$⊢F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)\right)$$
41	40	a1i	$$⊢\phi \to \left(F:A\underset{1-1}{⟶}B\leftrightarrow \left(F:A⟶B\wedge \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)\right)\right)$$
42	41	notbid	$$⊢\phi \to \left(\neg F:A\underset{1-1}{⟶}B\leftrightarrow \neg \left(F:A⟶B\wedge \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)\right)\right)$$
43	42	biimpd	$$⊢\phi \to \left(\neg F:A\underset{1-1}{⟶}B\to \neg \left(F:A⟶B\wedge \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)\right)\right)$$
44	30 43	mpd	$$⊢\phi \to \neg \left(F:A⟶B\wedge \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)\right)$$
45	4 44	mpnanrd	$$⊢\phi \to \neg \neg \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)$$
46	45	notnotrd	$$⊢\phi \to \exists x\in A\exists y\in A\left(F\left(x\right)=F\left(y\right)\wedge x\ne y\right)$$