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 ) )