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 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 V Fun F F = dom F
3 1 2 sylan2 F V F : A 1-1 B F = dom F
4 f1dm F : A 1-1 B dom F = A
5 4 adantl F V F : A 1-1 B dom F = A
6 dmexg F V dom F V
7 6 adantr F V F : A 1-1 B dom F V
8 5 7 eqeltrrd F V F : A 1-1 B A V
9 hashf1rn A V F : A 1-1 B F = ran F
10 8 9 sylancom F V F : A 1-1 B F = ran F
11 5 fveq2d F V F : A 1-1 B dom F = A
12 3 10 11 3eqtr3rd F V F : A 1-1 B A = ran F