Metamath Proof Explorer

Theorem hashf1rn

Description: The size of a finite set which is a one-to-one function is equal to the size of the function's range. (Contributed by Alexander van der Vekens, 12-Jan-2018) (Revised by AV, 4-May-2021)

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

Proof

Step Hyp Ref Expression
1 f1f 
 |-  ( F : A -1-1-> B -> F : A --> B )
2 1 anim2i 
 |-  ( ( A e. V /\ F : A -1-1-> B ) -> ( A e. V /\ F : A --> B ) )
3 2 ancomd 
 |-  ( ( A e. V /\ F : A -1-1-> B ) -> ( F : A --> B /\ A e. V ) )
4 fex 
 |-  ( ( F : A --> B /\ A e. V ) -> F e. _V )
5 3 4 syl 
 |-  ( ( A e. V /\ F : A -1-1-> B ) -> F e. _V )
6 f1o2ndf1 
 |-  ( F : A -1-1-> B -> ( 2nd |` F ) : F -1-1-onto-> ran F )
7 df-2nd 
 |-  2nd = ( x e. _V |-> U. ran { x } )
8 7 funmpt2 
 |-  Fun 2nd
9 resfunexg 
 |-  ( ( Fun 2nd /\ F e. _V ) -> ( 2nd |` F ) e. _V )
10 8 5 9 sylancr 
 |-  ( ( A e. V /\ F : A -1-1-> B ) -> ( 2nd |` F ) e. _V )
11 f1oeq1 
 |-  ( ( 2nd |` F ) = f -> ( ( 2nd |` F ) : F -1-1-onto-> ran F <-> f : F -1-1-onto-> ran F ) )
12 11 biimpd 
 |-  ( ( 2nd |` F ) = f -> ( ( 2nd |` F ) : F -1-1-onto-> ran F -> f : F -1-1-onto-> ran F ) )
13 12 eqcoms 
 |-  ( f = ( 2nd |` F ) -> ( ( 2nd |` F ) : F -1-1-onto-> ran F -> f : F -1-1-onto-> ran F ) )
14 13 adantl 
 |-  ( ( ( A e. V /\ F : A -1-1-> B ) /\ f = ( 2nd |` F ) ) -> ( ( 2nd |` F ) : F -1-1-onto-> ran F -> f : F -1-1-onto-> ran F ) )
15 10 14 spcimedv 
 |-  ( ( A e. V /\ F : A -1-1-> B ) -> ( ( 2nd |` F ) : F -1-1-onto-> ran F -> E. f f : F -1-1-onto-> ran F ) )
16 15 ex 
 |-  ( A e. V -> ( F : A -1-1-> B -> ( ( 2nd |` F ) : F -1-1-onto-> ran F -> E. f f : F -1-1-onto-> ran F ) ) )
17 16 com13 
 |-  ( ( 2nd |` F ) : F -1-1-onto-> ran F -> ( F : A -1-1-> B -> ( A e. V -> E. f f : F -1-1-onto-> ran F ) ) )
18 6 17 mpcom 
 |-  ( F : A -1-1-> B -> ( A e. V -> E. f f : F -1-1-onto-> ran F ) )
19 18 impcom 
 |-  ( ( A e. V /\ F : A -1-1-> B ) -> E. f f : F -1-1-onto-> ran F )
20 hasheqf1oi 
 |-  ( F e. _V -> ( E. f f : F -1-1-onto-> ran F -> ( # ` F ) = ( # ` ran F ) ) )
21 5 19 20 sylc 
 |-  ( ( A e. V /\ F : A -1-1-> B ) -> ( # ` F ) = ( # ` ran F ) )