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	a1i	$⊢ φ \to (\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))$
16	15	biimpd	$⊢ φ \to (\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))$
17	16	imp	$⊢ (φ \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)$
18		fveq2	$⊢ z = y \to F (z) = F (y)$
19	18	eqeq2d	$⊢ z = y \to (F (w) = F (z) \leftrightarrow F (w) = F (y))$
20		breq2	$⊢ z = y \to (w < z \leftrightarrow w < y)$
21	19 20	anbi12d	$⊢ z = y \to ((F (w) = F (z) \land w < z) \leftrightarrow (F (w) = F (y) \land w < y))$
22		fveqeq2	$⊢ w = x \to (F (w) = F (y) \leftrightarrow F (x) = F (y))$
23		breq1	$⊢ w = x \to (w < y \leftrightarrow x < y)$
24	22 23	anbi12d	$⊢ w = x \to ((F (w) = F (y) \land w < y) \leftrightarrow (F (x) = F (y) \land x < y))$
25	21 24	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)$
26	17 25	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)$
27		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)$
28	26 27	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)$
29	1 2 3 4	hashnexinj	$⊢ φ \to \exists x \in A \exists y \in A (F (x) = F (y) \land x \neq y)$
30		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)$
31		simpr	$⊢ (((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \land x < y) \to x < y$
32	30 31	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)$
33	32	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))$
34		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)$
35	34	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)$
36		simpr	$⊢ (((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \land y < x) \to y < x$
37	35 36	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)$
38	37	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))$
39		simprr	$⊢ ((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \to x \neq y$
40		simpl	$⊢ (φ \land (x \in A \land y \in A)) \to φ$
41		simprl	$⊢ (φ \land (x \in A \land y \in A)) \to x \in A$
42	40 41	jca	$⊢ (φ \land (x \in A \land y \in A)) \to (φ \land x \in A)$
43	5	sselda	$⊢ (φ \land x \in A) \to x \in ℝ$
44	42 43	syl	$⊢ (φ \land (x \in A \land y \in A)) \to x \in ℝ$
45	44	adantr	$⊢ ((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \to x \in ℝ$
46		simprr	$⊢ (φ \land (x \in A \land y \in A)) \to y \in A$
47	40 46	jca	$⊢ (φ \land (x \in A \land y \in A)) \to (φ \land y \in A)$
48	5	sselda	$⊢ (φ \land y \in A) \to y \in ℝ$
49	47 48	syl	$⊢ (φ \land (x \in A \land y \in A)) \to y \in ℝ$
50	49	adantr	$⊢ ((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \to y \in ℝ$
51	45 50	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))$
52	39 51	mpbid	$⊢ ((φ \land (x \in A \land y \in A)) \land (F (x) = F (y) \land x \neq y)) \to (x < y \lor y < x)$
53	33 38 52	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))$
54	53	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)))$
55	54	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)))$
56	55	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))$
57		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))$
58	57	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))$
59	56 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 y \in A (F (y) = F (x) \land y < x))$
60		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))$
61	59 60	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))$
62	61	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)))$
63	29 62	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))$
64	6 28 63	mpjaodan	$⊢ φ \to \exists x \in A \exists y \in A (F (x) = F (y) \land x < y)$

Metamath Proof Explorer

Theorem hashnexinjle

Proof