hashnexinjle

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. Also we introduce a one sided inequality to simplify a duplicateable proof. (Contributed by metakunt, 2-May-2025)

	Ref	Expression
Hypotheses	hashnexinjle.1	$⊢ φ \to A \in Fin$
	hashnexinjle.2	$⊢ φ \to B \in Fin$
	hashnexinjle.3	$⊢ φ \to \|B\| < \|A\|$
	hashnexinjle.4	$⊢ φ \to F : A ⟶ B$
	hashnexinjle.5	$⊢ φ \to A \subseteq ℝ$
Assertion	hashnexinjle	$⊢ φ \to \exists x \in A \exists y \in A (F (x) = F (y) \land x < y)$

Proof

Step	Hyp	Ref	Expression
1		hashnexinjle.1	$⊢ φ \to A \in Fin$
2		hashnexinjle.2	$⊢ φ \to B \in Fin$
3		hashnexinjle.3	$⊢ φ \to \|B\| < \|A\|$
4		hashnexinjle.4	$⊢ φ \to F : A ⟶ B$
5		hashnexinjle.5	$⊢ φ \to A \subseteq ℝ$
6		simpr	$⊢ (φ \land \exists x \in A \exists y \in A (F (x) = F (y) \land x < y)) \to \exists x \in A \exists y \in A (F (x) = F (y) \land x < y)$
7		fveq2	$⊢ x = z \to F (x) = F (z)$
8	7	eqeq2d	$⊢ x = z \to (F (y) = F (x) \leftrightarrow F (y) = F (z))$
9		breq2	$⊢ x = z \to (y < x \leftrightarrow y < z)$
10	8 9	anbi12d	$⊢ x = z \to ((F (y) = F (x) \land y < x) \leftrightarrow (F (y) = F (z) \land y < z))$
11		fveqeq2	$⊢ y = w \to (F (y) = F (z) \leftrightarrow F (w) = F (z))$
12		breq1	$⊢ y = w \to (y < z \leftrightarrow w < z)$
13	11 12	anbi12d	$⊢ y = w \to ((F (y) = F (z) \land y < z) \leftrightarrow (F (w) = F (z) \land w < z))$
14	10 13	cbvrex2vw	$⊢ \exists x \in A \exists y \in A (F (y) = F (x) \land y < x) \leftrightarrow \exists z \in A \exists w \in A (F (w) = F (z) \land w < z)$
15	14	bilani	$⊢ (φ \land \exists x \in A \exists y \in A (F (y) = F (x) \land y < x)) \to \exists z \in A \exists w \in A (F (w) = F (z) \land w < z)$
16		fveq2	$⊢ z = y \to F (z) = F (y)$
17	16	eqeq2d	$⊢ z = y \to (F (w) = F (z) \leftrightarrow F (w) = F (y))$
18		breq2	$⊢ z = y \to (w < z \leftrightarrow w < y)$
19	17 18	anbi12d	$⊢ z = y \to ((F (w) = F (z) \land w < z) \leftrightarrow (F (w) = F (y) \land w < y))$
20		fveqeq2	$⊢ w = x \to (F (w) = F (y) \leftrightarrow F (x) = F (y))$
21		breq1	$⊢ w = x \to (w < y \leftrightarrow x < y)$
22	20 21	anbi12d	$⊢ w = x \to ((F (w) = F (y) \land w < y) \leftrightarrow (F (x) = F (y) \land x < y))$
23	19 22	cbvrex2vw	$⊢ \exists z \in A \exists w \in A (F (w) = F (z) \land w < z) \leftrightarrow \exists y \in A \exists x \in A (F (x) = F (y) \land x < y)$
24	15 23	sylib	$⊢ (φ \land \exists x \in A \exists y \in A (F (y) = F (x) \land y < x)) \to \exists y \in A \exists x \in A (F (x) = F (y) \land x < y)$
25		rexcom	$⊢ \exists y \in A \exists x \in A (F (x) = F (y) \land x < y) \leftrightarrow \exists x \in A \exists y \in A (F (x) = F (y) \land x < y)$
26	24 25	sylib	$⊢ (φ \land \exists x \in A \exists y \in A (F (y) = F (x) \land y < x)) \to \exists x \in A \exists y \in A (F (x) = F (y) \land x < y)$
27	1 2 3 4	hashnexinj	$⊢ φ \to \exists x \in A \exists y \in A (F (x) = F (y) \land x \neq y)$
28		simplrl	$⊢ (((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \land x < y) \to F (x) = F (y)$
29		simpr	$⊢ (((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \land x < y) \to x < y$
30	28 29	jca	$⊢ (((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \land x < y) \to (F (x) = F (y) \land x < y)$
31	30	orcd	$⊢ (((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \land x < y) \to ((F (x) = F (y) \land x < y) \lor (F (y) = F (x) \land y < x))$
32		simplrl	$⊢ (((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \land y < x) \to F (x) = F (y)$
33	32	eqcomd	$⊢ (((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \land y < x) \to F (y) = F (x)$
34		simpr	$⊢ (((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \land y < x) \to y < x$
35	33 34	jca	$⊢ (((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \land y < x) \to (F (y) = F (x) \land y < x)$
36	35	olcd	$⊢ (((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \land y < x) \to ((F (x) = F (y) \land x < y) \lor (F (y) = F (x) \land y < x))$
37		simprr	$⊢ ((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \to x \neq y$
38		simpl	$⊢ (φ \land (x \in A \land y \in A)) \to φ$
39		simprl	$⊢ (φ \land (x \in A \land y \in A)) \to x \in A$
40	38 39	jca	$⊢ (φ \land (x \in A \land y \in A)) \to (φ \land x \in A)$
41	5	sselda	$⊢ (φ \land x \in A) \to x \in ℝ$
42	40 41	syl	$⊢ (φ \land (x \in A \land y \in A)) \to x \in ℝ$
43	42	adantr	$⊢ ((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \to x \in ℝ$
44		simprr	$⊢ (φ \land (x \in A \land y \in A)) \to y \in A$
45	38 44	jca	$⊢ (φ \land (x \in A \land y \in A)) \to (φ \land y \in A)$
46	5	sselda	$⊢ (φ \land y \in A) \to y \in ℝ$
47	45 46	syl	$⊢ (φ \land (x \in A \land y \in A)) \to y \in ℝ$
48	47	adantr	$⊢ ((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \to y \in ℝ$
49	43 48	lttri2d	$⊢ ((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \to (x \neq y \leftrightarrow (x < y \lor y < x))$
50	37 49	mpbid	$⊢ ((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \to (x < y \lor y < x)$
51	31 36 50	mpjaodan	$⊢ ((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \to ((F (x) = F (y) \land x < y) \lor (F (y) = F (x) \land y < x))$
52	51	ex	$⊢ (φ \land (x \in A \land y \in A)) \to ((F (x) = F (y) \land x \neq y) \to ((F (x) = F (y) \land x < y) \lor (F (y) = F (x) \land y < x)))$
53	52	reximdvva	$⊢ φ \to (\exists x \in A \exists y \in A (F (x) = F (y) \land x \neq y) \to \exists x \in A \exists y \in A ((F (x) = F (y) \land x < y) \lor (F (y) = F (x) \land y < x)))$
54	53	imp	$⊢ (φ \land \exists x \in A \exists y \in A (F (x) = F (y) \land x \neq y)) \to \exists x \in A \exists y \in A ((F (x) = F (y) \land x < y) \lor (F (y) = F (x) \land y < x))$
55		r19.43	$⊢ \exists y \in A ((F (x) = F (y) \land x < y) \lor (F (y) = F (x) \land y < x)) \leftrightarrow (\exists y \in A (F (x) = F (y) \land x < y) \lor \exists y \in A (F (y) = F (x) \land y < x))$
56	55	rexbii	$⊢ \exists x \in A \exists y \in A ((F (x) = F (y) \land x < y) \lor (F (y) = F (x) \land y < x)) \leftrightarrow \exists x \in A (\exists y \in A (F (x) = F (y) \land x < y) \lor \exists y \in A (F (y) = F (x) \land y < x))$
57	54 56	sylib	$⊢ (φ \land \exists x \in A \exists y \in A (F (x) = F (y) \land x \neq y)) \to \exists x \in A (\exists y \in A (F (x) = F (y) \land x < y) \lor \exists y \in A (F (y) = F (x) \land y < x))$
58		r19.43	$⊢ \exists x \in A (\exists y \in A (F (x) = F (y) \land x < y) \lor \exists y \in A (F (y) = F (x) \land y < x)) \leftrightarrow (\exists x \in A \exists y \in A (F (x) = F (y) \land x < y) \lor \exists x \in A \exists y \in A (F (y) = F (x) \land y < x))$
59	57 58	sylib	$⊢ (φ \land \exists x \in A \exists y \in A (F (x) = F (y) \land x \neq y)) \to (\exists x \in A \exists y \in A (F (x) = F (y) \land x < y) \lor \exists x \in A \exists y \in A (F (y) = F (x) \land y < x))$
60	59	ex	$⊢ φ \to (\exists x \in A \exists y \in A (F (x) = F (y) \land x \neq y) \to (\exists x \in A \exists y \in A (F (x) = F (y) \land x < y) \lor \exists x \in A \exists y \in A (F (y) = F (x) \land y < x)))$
61	27 60	mpd	$⊢ φ \to (\exists x \in A \exists y \in A (F (x) = F (y) \land x < y) \lor \exists x \in A \exists y \in A (F (y) = F (x) \land y < x))$
62	6 26 61	mpjaodan	$⊢ φ \to \exists x \in A \exists y \in A (F (x) = F (y) \land x < y)$

Metamath Proof Explorer

Theorem hashnexinjle

Proof