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

Proof

Step	Hyp	Ref	Expression
1		hashnexinjle.1	⊢ ( 𝜑 → 𝐴 ∈ Fin )
2		hashnexinjle.2	⊢ ( 𝜑 → 𝐵 ∈ Fin )
3		hashnexinjle.3	⊢ ( 𝜑 → ( ♯ ‘ 𝐵 ) < ( ♯ ‘ 𝐴 ) )
4		hashnexinjle.4	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
5		hashnexinjle.5	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
6		simpr	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) )
7		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
8	7	eqeq2d	⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ) )
9		breq2	⊢ ( 𝑥 = 𝑧 → ( 𝑦 < 𝑥 ↔ 𝑦 < 𝑧 ) )
10	8 9	anbi12d	⊢ ( 𝑥 = 𝑧 → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ↔ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 < 𝑧 ) ) )
11		fveqeq2	⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ) )
12		breq1	⊢ ( 𝑦 = 𝑤 → ( 𝑦 < 𝑧 ↔ 𝑤 < 𝑧 ) )
13	11 12	anbi12d	⊢ ( 𝑦 = 𝑤 → ( ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑦 < 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 < 𝑧 ) ) )
14	10 13	cbvrex2vw	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 < 𝑧 ) )
15	14	a1i	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ↔ ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 < 𝑧 ) ) )
16	15	biimpd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) → ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 < 𝑧 ) ) )
17	16	imp	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 < 𝑧 ) )
18		fveq2	⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
19	18	eqeq2d	⊢ ( 𝑧 = 𝑦 → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) ) )
20		breq2	⊢ ( 𝑧 = 𝑦 → ( 𝑤 < 𝑧 ↔ 𝑤 < 𝑦 ) )
21	19 20	anbi12d	⊢ ( 𝑧 = 𝑦 → ( ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 < 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑤 < 𝑦 ) ) )
22		fveqeq2	⊢ ( 𝑤 = 𝑥 → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
23		breq1	⊢ ( 𝑤 = 𝑥 → ( 𝑤 < 𝑦 ↔ 𝑥 < 𝑦 ) )
24	22 23	anbi12d	⊢ ( 𝑤 = 𝑥 → ( ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑤 < 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) )
25	21 24	cbvrex2vw	⊢ ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 < 𝑧 ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) )
26	17 25	sylib	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) )
27		rexcom	⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) )
28	26 27	sylib	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) )
29	1 2 3 4	hashnexinj	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
30		simplrl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
31		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 < 𝑦 )
32	30 31	jca	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) )
33	32	orcd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑥 < 𝑦 ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
34		simplrl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑦 < 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
35	34	eqcomd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑦 < 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
36		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑦 < 𝑥 ) → 𝑦 < 𝑥 )
37	35 36	jca	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑦 < 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) )
38	37	olcd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑦 < 𝑥 ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
39		simprr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ≠ 𝑦 )
40		simpl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝜑 )
41		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
42	40 41	jca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) )
43	5	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
44	42 43	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ ℝ )
45	44	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ ℝ )
46		simprr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
47	40 46	jca	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) )
48	5	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
49	47 48	syl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ ℝ )
50	49	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑦 ∈ ℝ )
51	45 50	lttri2d	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑥 ≠ 𝑦 ↔ ( 𝑥 < 𝑦 ∨ 𝑦 < 𝑥 ) ) )
52	39 51	mpbid	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑥 < 𝑦 ∨ 𝑦 < 𝑥 ) )
53	33 38 52	mpjaodan	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
54	53	ex	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ) )
55	54	reximdvva	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ) )
56	55	imp	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
57		r19.43	⊢ ( ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ↔ ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
58	57	rexbii	⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
59	56 58	sylib	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
60		r19.43	⊢ ( ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
61	59 60	sylib	⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
62	61	ex	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ) )
63	29 62	mpd	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
64	6 28 63	mpjaodan	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) )