This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hashf1dmrn

Description: The size of the domain of a one-to-one set function is equal to the size of its range. (Contributed by BTernaryTau, 1-Oct-2023)

Ref Expression
Assertion hashf1dmrn 
|- ( ( F e. V /\ F : A -1-1-> B ) -> ( # ` A ) = ( # ` ran F ) )

Proof

Step Hyp Ref Expression
1 f1fun 
 |-  ( F : A -1-1-> B -> Fun F )
2 hashfundm 
 |-  ( ( F e. V /\ Fun F ) -> ( # ` F ) = ( # ` dom F ) )
3 1 2 sylan2 
 |-  ( ( F e. V /\ F : A -1-1-> B ) -> ( # ` F ) = ( # ` dom F ) )
4 f1dm 
 |-  ( F : A -1-1-> B -> dom F = A )
5 4 adantl 
 |-  ( ( F e. V /\ F : A -1-1-> B ) -> dom F = A )
6 dmexg 
 |-  ( F e. V -> dom F e. _V )
7 6 adantr 
 |-  ( ( F e. V /\ F : A -1-1-> B ) -> dom F e. _V )
8 5 7 eqeltrrd 
 |-  ( ( F e. V /\ F : A -1-1-> B ) -> A e. _V )
9 hashf1rn 
 |-  ( ( A e. _V /\ F : A -1-1-> B ) -> ( # ` F ) = ( # ` ran F ) )
10 8 9 sylancom 
 |-  ( ( F e. V /\ F : A -1-1-> B ) -> ( # ` F ) = ( # ` ran F ) )
11 5 fveq2d 
 |-  ( ( F e. V /\ F : A -1-1-> B ) -> ( # ` dom F ) = ( # ` A ) )
12 3 10 11 3eqtr3rd 
 |-  ( ( F e. V /\ F : A -1-1-> B ) -> ( # ` A ) = ( # ` ran F ) )