Metamath Proof Explorer

Theorem hashfn

Description: A function is equinumerous to its domain. (Contributed by Mario Carneiro, 12-Mar-2015)

Ref Expression
Assertion hashfn 
|- ( F Fn A -> ( # ` F ) = ( # ` A ) )

Proof

Step Hyp Ref Expression
1 fndmeng 
 |-  ( ( F Fn A /\ A e. _V ) -> A ~~ F )
2 ensym 
 |-  ( A ~~ F -> F ~~ A )
3 hasheni 
 |-  ( F ~~ A -> ( # ` F ) = ( # ` A ) )
4 1 2 3 3syl 
 |-  ( ( F Fn A /\ A e. _V ) -> ( # ` F ) = ( # ` A ) )
5 dmexg 
 |-  ( F e. _V -> dom F e. _V )
6 fndm 
 |-  ( F Fn A -> dom F = A )
7 6 eleq1d 
 |-  ( F Fn A -> ( dom F e. _V <-> A e. _V ) )
8 5 7 imbitrid 
 |-  ( F Fn A -> ( F e. _V -> A e. _V ) )
9 8 con3dimp 
 |-  ( ( F Fn A /\ -. A e. _V ) -> -. F e. _V )
10 fvprc 
 |-  ( -. F e. _V -> ( # ` F ) = (/) )
11 9 10 syl 
 |-  ( ( F Fn A /\ -. A e. _V ) -> ( # ` F ) = (/) )
12 fvprc 
 |-  ( -. A e. _V -> ( # ` A ) = (/) )
13 12 adantl 
 |-  ( ( F Fn A /\ -. A e. _V ) -> ( # ` A ) = (/) )
14 11 13 eqtr4d 
 |-  ( ( F Fn A /\ -. A e. _V ) -> ( # ` F ) = ( # ` A ) )
15 4 14 pm2.61dan 
 |-  ( F Fn A -> ( # ` F ) = ( # ` A ) )