Metamath Proof Explorer

Theorem hashf1dmcdm

Description: The size of the domain of a one-to-one set function is less than or equal to the size of its codomain, if it exists. (Contributed by BTernaryTau, 1-Oct-2023)

Ref Expression
Assertion hashf1dmcdm 
|- ( ( F e. V /\ B e. W /\ F : A -1-1-> B ) -> ( # ` A ) <_ ( # ` B ) )

Proof

Step Hyp Ref Expression
1 hashf1dmrn 
 |-  ( ( F e. V /\ F : A -1-1-> B ) -> ( # ` A ) = ( # ` ran F ) )
2 1 3adant2 
 |-  ( ( F e. V /\ B e. W /\ F : A -1-1-> B ) -> ( # ` A ) = ( # ` ran F ) )
3 f1f 
 |-  ( F : A -1-1-> B -> F : A --> B )
4 frn 
 |-  ( F : A --> B -> ran F C_ B )
5 hashss 
 |-  ( ( B e. W /\ ran F C_ B ) -> ( # ` ran F ) <_ ( # ` B ) )
6 4 5 sylan2 
 |-  ( ( B e. W /\ F : A --> B ) -> ( # ` ran F ) <_ ( # ` B ) )
7 3 6 sylan2 
 |-  ( ( B e. W /\ F : A -1-1-> B ) -> ( # ` ran F ) <_ ( # ` B ) )
8 7 3adant1 
 |-  ( ( F e. V /\ B e. W /\ F : A -1-1-> B ) -> ( # ` ran F ) <_ ( # ` B ) )
9 2 8 eqbrtrd 
 |-  ( ( F e. V /\ B e. W /\ F : A -1-1-> B ) -> ( # ` A ) <_ ( # ` B ) )