Metamath Proof Explorer

Theorem hashnexinj

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. (Contributed by metakunt, 2-May-2025)

Ref Expression
Hypotheses hashnexinj.1 
|- ( ph -> A e. Fin )
hashnexinj.2 
|- ( ph -> B e. Fin )
hashnexinj.3 
|- ( ph -> ( # ` B ) < ( # ` A ) )
hashnexinj.4 
|- ( ph -> F : A --> B )
Assertion hashnexinj 
|- ( ph -> E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) )

Proof

Step Hyp Ref Expression
1 hashnexinj.1 
 |-  ( ph -> A e. Fin )
2 hashnexinj.2 
 |-  ( ph -> B e. Fin )
3 hashnexinj.3 
 |-  ( ph -> ( # ` B ) < ( # ` A ) )
4 hashnexinj.4 
 |-  ( ph -> F : A --> B )
5 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
6 2 5 syl 
 |-  ( ph -> ( # ` B ) e. NN0 )
7 6 nn0red 
 |-  ( ph -> ( # ` B ) e. RR )
8 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
9 1 8 syl 
 |-  ( ph -> ( # ` A ) e. NN0 )
10 9 nn0red 
 |-  ( ph -> ( # ` A ) e. RR )
11 7 10 ltnled 
 |-  ( ph -> ( ( # ` B ) < ( # ` A ) <-> -. ( # ` A ) <_ ( # ` B ) ) )
12 3 11 mpbid 
 |-  ( ph -> -. ( # ` A ) <_ ( # ` B ) )
13 hashdom 
 |-  ( ( A e. Fin /\ B e. Fin ) -> ( ( # ` A ) <_ ( # ` B ) <-> A ~<_ B ) )
14 1 2 13 syl2anc 
 |-  ( ph -> ( ( # ` A ) <_ ( # ` B ) <-> A ~<_ B ) )
15 14 notbid 
 |-  ( ph -> ( -. ( # ` A ) <_ ( # ` B ) <-> -. A ~<_ B ) )
16 15 biimpd 
 |-  ( ph -> ( -. ( # ` A ) <_ ( # ` B ) -> -. A ~<_ B ) )
17 12 16 mpd 
 |-  ( ph -> -. A ~<_ B )
18 brdomg 
 |-  ( B e. Fin -> ( A ~<_ B <-> E. f f : A -1-1-> B ) )
19 18 notbid 
 |-  ( B e. Fin -> ( -. A ~<_ B <-> -. E. f f : A -1-1-> B ) )
20 19 biimpd 
 |-  ( B e. Fin -> ( -. A ~<_ B -> -. E. f f : A -1-1-> B ) )
21 2 20 syl 
 |-  ( ph -> ( -. A ~<_ B -> -. E. f f : A -1-1-> B ) )
22 17 21 mpd 
 |-  ( ph -> -. E. f f : A -1-1-> B )
23 alnex 
 |-  ( A. f -. f : A -1-1-> B <-> -. E. f f : A -1-1-> B )
24 22 23 sylibr 
 |-  ( ph -> A. f -. f : A -1-1-> B )
25 2 1 4 elmapdd 
 |-  ( ph -> F e. ( B ^m A ) )
26 f1eq1 
 |-  ( f = F -> ( f : A -1-1-> B <-> F : A -1-1-> B ) )
27 26 notbid 
 |-  ( f = F -> ( -. f : A -1-1-> B <-> -. F : A -1-1-> B ) )
28 27 spcgv 
 |-  ( F e. ( B ^m A ) -> ( A. f -. f : A -1-1-> B -> -. F : A -1-1-> B ) )
29 25 28 syl 
 |-  ( ph -> ( A. f -. f : A -1-1-> B -> -. F : A -1-1-> B ) )
30 24 29 mpd 
 |-  ( ph -> -. F : A -1-1-> B )
31 dff13 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
32 iman 
 |-  ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> -. ( ( F ` x ) = ( F ` y ) /\ -. x = y ) )
33 df-ne 
 |-  ( x =/= y <-> -. x = y )
34 33 anbi2i 
 |-  ( ( ( F ` x ) = ( F ` y ) /\ x =/= y ) <-> ( ( F ` x ) = ( F ` y ) /\ -. x = y ) )
35 32 34 xchbinxr 
 |-  ( ( ( F ` x ) = ( F ` y ) -> x = y ) <-> -. ( ( F ` x ) = ( F ` y ) /\ x =/= y ) )
36 35 2ralbii 
 |-  ( A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> A. x e. A A. y e. A -. ( ( F ` x ) = ( F ` y ) /\ x =/= y ) )
37 ralnex2 
 |-  ( A. x e. A A. y e. A -. ( ( F ` x ) = ( F ` y ) /\ x =/= y ) <-> -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) )
38 36 37 bitri 
 |-  ( A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) <-> -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) )
39 38 anbi2i 
 |-  ( ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) <-> ( F : A --> B /\ -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) )
40 31 39 bitri 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) )
41 40 a1i 
 |-  ( ph -> ( F : A -1-1-> B <-> ( F : A --> B /\ -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) )
42 41 notbid 
 |-  ( ph -> ( -. F : A -1-1-> B <-> -. ( F : A --> B /\ -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) )
43 42 biimpd 
 |-  ( ph -> ( -. F : A -1-1-> B -> -. ( F : A --> B /\ -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) ) )
44 30 43 mpd 
 |-  ( ph -> -. ( F : A --> B /\ -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) ) )
45 4 44 mpnanrd 
 |-  ( ph -> -. -. E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) )
46 45 notnotrd 
 |-  ( ph -> E. x e. A E. y e. A ( ( F ` x ) = ( F ` y ) /\ x =/= y ) )