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 bilani 
 |-  ( ( 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 fveq2 
 |-  ( z = y -> ( F ` z ) = ( F ` y ) )
17 16 eqeq2d 
 |-  ( z = y -> ( ( F ` w ) = ( F ` z ) <-> ( F ` w ) = ( F ` y ) ) )
18 breq2 
 |-  ( z = y -> ( w < z <-> w < y ) )
19 17 18 anbi12d 
 |-  ( z = y -> ( ( ( F ` w ) = ( F ` z ) /\ w < z ) <-> ( ( F ` w ) = ( F ` y ) /\ w < y ) ) )
20 fveqeq2 
 |-  ( w = x -> ( ( F ` w ) = ( F ` y ) <-> ( F ` x ) = ( F ` y ) ) )
21 breq1 
 |-  ( w = x -> ( w < y <-> x < y ) )
22 20 21 anbi12d 
 |-  ( w = x -> ( ( ( F ` w ) = ( F ` y ) /\ w < y ) <-> ( ( F ` x ) = ( F ` y ) /\ x < y ) ) )
23 19 22 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 ) )
24 15 23 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 ) )
25 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 ) )
26 24 25 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 ) )
27 1 2 3 4 hashnexinj 
 |-  ( ph -> E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) )
28 simplrl 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) /\ x < y ) -> ( F ` x ) = ( F ` y ) )
29 simpr 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) /\ x < y ) -> x < y )
30 28 29 jca 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) /\ x < y ) -> ( ( F ` x ) = ( F ` y ) /\ x < y ) )
31 30 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 ) ) )
32 simplrl 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) /\ y < x ) -> ( F ` x ) = ( F ` y ) )
33 32 eqcomd 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) /\ y < x ) -> ( F ` y ) = ( F ` x ) )
34 simpr 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) /\ y < x ) -> y < x )
35 33 34 jca 
 |-  ( ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) /\ y < x ) -> ( ( F ` y ) = ( F ` x ) /\ y < x ) )
36 35 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 ) ) )
37 simprr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) -> x =/= y )
38 simpl 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ph )
39 simprl 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> x e. A )
40 38 39 jca 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( ph /\ x e. A ) )
41 5 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. RR )
42 40 41 syl 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> x e. RR )
43 42 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) -> x e. RR )
44 simprr 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> y e. A )
45 38 44 jca 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> ( ph /\ y e. A ) )
46 5 sselda 
 |-  ( ( ph /\ y e. A ) -> y e. RR )
47 45 46 syl 
 |-  ( ( ph /\ ( x e. A /\ y e. A ) ) -> y e. RR )
48 47 adantr 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) -> y e. RR )
49 43 48 lttri2d 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) -> ( x =/= y <-> ( x < y \/ y < x ) ) )
50 37 49 mpbid 
 |-  ( ( ( ph /\ ( x e. A /\ y e. A ) ) /\ ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) -> ( x < y \/ y < x ) )
51 31 36 50 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 ) ) )
52 51 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 ) ) ) )
53 52 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 ) ) ) )
54 53 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 ) ) )
55 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 ) ) )
56 55 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 ) ) )
57 54 56 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 ) ) )
58 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 ) ) )
59 57 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. x e. A E. y e. A ( ( F ` y ) = ( F ` x ) /\ y < x ) ) )
60 59 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 ) ) ) )
61 27 60 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 ) ) )
62 6 26 61 mpjaodan 
 |-  ( ph -> E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x < y ) )