Metamath Proof Explorer

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 bilani ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 < 𝑧 ) )
16 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑦 ) )
17 16 eqeq2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ↔ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) ) )
18 breq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑤 < 𝑧 ↔ 𝑤 < 𝑦 ) )
19 17 18 anbi12d ⊢ ( 𝑧 = 𝑦 → ( ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 < 𝑧 ) ↔ ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑤 < 𝑦 ) ) )
20 fveqeq2 ⊢ ( 𝑤 = 𝑥 → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) )
21 breq1 ⊢ ( 𝑤 = 𝑥 → ( 𝑤 < 𝑦 ↔ 𝑥 < 𝑦 ) )
22 20 21 anbi12d ⊢ ( 𝑤 = 𝑥 → ( ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑤 < 𝑦 ) ↔ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) )
23 19 22 cbvrex2vw ⊢ ( ∃ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐴 ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∧ 𝑤 < 𝑧 ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) )
24 15 23 sylib ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) )
25 rexcom ⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑥 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ↔ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) )
26 24 25 sylib ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) )
27 1 2 3 4 hashnexinj ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) )
28 simplrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
29 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 < 𝑦 )
30 28 29 jca ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) )
31 30 orcd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑥 < 𝑦 ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
32 simplrl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑦 < 𝑥 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
33 32 eqcomd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑦 < 𝑥 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) )
34 simpr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑦 < 𝑥 ) → 𝑦 < 𝑥 )
35 33 34 jca ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑦 < 𝑥 ) → ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) )
36 35 olcd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) ∧ 𝑦 < 𝑥 ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
37 simprr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ≠ 𝑦 )
38 simpl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝜑 )
39 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ 𝐴 )
40 38 39 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) )
41 5 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ )
42 40 41 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑥 ∈ ℝ )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑥 ∈ ℝ )
44 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ 𝐴 )
45 38 44 jca ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) )
46 5 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
47 45 46 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → 𝑦 ∈ ℝ )
48 47 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → 𝑦 ∈ ℝ )
49 43 48 lttri2d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑥 ≠ 𝑦 ↔ ( 𝑥 < 𝑦 ∨ 𝑦 < 𝑥 ) ) )
50 37 49 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( 𝑥 < 𝑦 ∨ 𝑦 < 𝑥 ) )
51 31 36 50 mpjaodan ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
52 51 ex ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) → ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ) )
53 52 reximdvva ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ) )
54 53 imp ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
55 r19.43 ⊢ ( ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ↔ ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
56 55 rexbii ⊢ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ↔ ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
57 54 56 sylib ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
58 r19.43 ⊢ ( ∃ 𝑥 ∈ 𝐴 ( ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ↔ ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
59 57 58 sylib ⊢ ( ( 𝜑 ∧ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
60 59 ex ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 ≠ 𝑦 ) → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ) )
61 27 60 mpd ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) ∨ ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) )
62 6 26 61 mpjaodan ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ∃ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ∧ 𝑥 < 𝑦 ) )