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 
|- ( ph -> A e. Fin )
hashnexinjle.2 
|- ( ph -> B e. Fin )
hashnexinjle.3 
|- ( ph -> ( # ` B ) < ( # ` A ) )
hashnexinjle.4 
|- ( ph -> F : A --> B )
hashnexinjle.5 
|- ( ph -> A C_ RR )
Assertion hashnexinjle 
|- ( ph -> E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x < y ) )

Proof

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