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	⊢ ( 𝜑 → 𝐴 ∈ Fin )
	hashnexinj.2	⊢ ( 𝜑 → 𝐵 ∈ Fin )
	hashnexinj.3	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐴 ) )
	hashnexinj.4	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion	hashnexinj	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		hashnexinj.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		hashnexinj.2	⊢ ( 𝜑 → 𝐵 ∈ Fin )
3		hashnexinj.3	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐴 ) )
4		hashnexinj.4	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
5		hashcl	⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ₀ )
6	2 5	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℕ₀ )
7	6	nn0red	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) ∈ ℝ )
8		hashcl	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ₀ )
9	1 8	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℕ₀ )
10	9	nn0red	⊢ ( 𝜑 → ( ♯ ‘ 𝐴 ) ∈ ℝ )
11	7 10	ltnled	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐴 ) ↔ ¬ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ) )
12	3 11	mpbid	⊢ ( 𝜑 → ¬ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) )
13		hashdom	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ∈ Fin ) → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) )
14	1 2 13	syl2anc	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ 𝐴 ≼ 𝐵 ) )
15	14	notbid	⊢ ( 𝜑 → ( ¬ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) ↔ ¬ 𝐴 ≼ 𝐵 ) )
16	15	biimpd	⊢ ( 𝜑 → ( ¬ ( ♯ ‘ 𝐴 ) ≤ ( ♯ ‘ 𝐵 ) → ¬ 𝐴 ≼ 𝐵 ) )
17	12 16	mpd	⊢ ( 𝜑 → ¬ 𝐴 ≼ 𝐵 )
18		brdomg	⊢ ( 𝐵 ∈ Fin → ( 𝐴 ≼ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )
19	18	notbid	⊢ ( 𝐵 ∈ Fin → ( ¬ 𝐴 ≼ 𝐵 ↔ ¬ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )
20	19	biimpd	⊢ ( 𝐵 ∈ Fin → ( ¬ 𝐴 ≼ 𝐵 → ¬ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )
21	2 20	syl	⊢ ( 𝜑 → ( ¬ 𝐴 ≼ 𝐵 → ¬ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 ) )
22	17 21	mpd	⊢ ( 𝜑 → ¬ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 )
23		alnex	⊢ ( ∀ 𝑓 ¬ 𝑓 : 𝐴 –1-1→ 𝐵 ↔ ¬ ∃ 𝑓 𝑓 : 𝐴 –1-1→ 𝐵 )
24	22 23	sylibr	⊢ ( 𝜑 → ∀ 𝑓 ¬ 𝑓 : 𝐴 –1-1→ 𝐵 )
25	2 1 4	elmapdd	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐵 ↑_m 𝐴 ) )
26		f1eq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 : 𝐴 –1-1→ 𝐵 ↔ 𝐹 : 𝐴 –1-1→ 𝐵 ) )
27	26	notbid	⊢ ( 𝑓 = 𝐹 → ( ¬ 𝑓 : 𝐴 –1-1→ 𝐵 ↔ ¬ 𝐹 : 𝐴 –1-1→ 𝐵 ) )
28	27	spcgv	⊢ ( 𝐹 ∈ ( 𝐵 ↑_m 𝐴 ) → ( ∀ 𝑓 ¬ 𝑓 : 𝐴 –1-1→ 𝐵 → ¬ 𝐹 : 𝐴 –1-1→ 𝐵 ) )
29	25 28	syl	⊢ ( 𝜑 → ( ∀ 𝑓 ¬ 𝑓 : 𝐴 –1-1→ 𝐵 → ¬ 𝐹 : 𝐴 –1-1→ 𝐵 ) )
30	24 29	mpd	⊢ ( 𝜑 → ¬ 𝐹 : 𝐴 –1-1→ 𝐵 )
31		dff13	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
32		iman	⊢ ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ¬ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
33		df-ne	⊢ ( 𝑥 ≠ 𝑦 ↔ ¬ 𝑥 = 𝑦 )
34	33	anbi2i	⊢ ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ ¬ 𝑥 = 𝑦 ) )
35	32 34	xchbinxr	⊢ ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ¬ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
36	35	2ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
37		ralnex2	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ¬ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
38	36 37	bitri	⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ↔ ¬ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
39	38	anbi2i	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ¬ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) )
40	31 39	bitri	⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ¬ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) )
41	40	a1i	⊢ ( 𝜑 → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ¬ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) )
42	41	notbid	⊢ ( 𝜑 → ( ¬ 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ¬ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ¬ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) )
43	42	biimpd	⊢ ( 𝜑 → ( ¬ 𝐹 : 𝐴 –1-1→ 𝐵 → ¬ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ¬ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ) )
44	30 43	mpd	⊢ ( 𝜑 → ¬ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ¬ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) )
45	4 44	mpnanrd	⊢ ( 𝜑 → ¬ ¬ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
46	45	notnotrd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )

Metamath Proof Explorer

Theorem hashnexinj

Proof