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

Metamath Proof Explorer

Theorem hashfac

Description: A factorial counts the number of bijections on a finite set. (Contributed by Mario Carneiro, 21-Jan-2015) (Proof shortened by Mario Carneiro, 17-Apr-2015)

Ref Expression
Assertion hashfac 
|- ( A e. Fin -> ( # ` { f | f : A -1-1-onto-> A } ) = ( ! ` ( # ` A ) ) )

Proof

Step Hyp Ref Expression
1 hashf1 
 |-  ( ( A e. Fin /\ A e. Fin ) -> ( # ` { f | f : A -1-1-> A } ) = ( ( ! ` ( # ` A ) ) x. ( ( # ` A ) _C ( # ` A ) ) ) )
2 1 anidms 
 |-  ( A e. Fin -> ( # ` { f | f : A -1-1-> A } ) = ( ( ! ` ( # ` A ) ) x. ( ( # ` A ) _C ( # ` A ) ) ) )
3 enrefg 
 |-  ( A e. Fin -> A ~~ A )
4 f1finf1o 
 |-  ( ( A ~~ A /\ A e. Fin ) -> ( f : A -1-1-> A <-> f : A -1-1-onto-> A ) )
5 3 4 mpancom 
 |-  ( A e. Fin -> ( f : A -1-1-> A <-> f : A -1-1-onto-> A ) )
6 5 abbidv 
 |-  ( A e. Fin -> { f | f : A -1-1-> A } = { f | f : A -1-1-onto-> A } )
7 6 fveq2d 
 |-  ( A e. Fin -> ( # ` { f | f : A -1-1-> A } ) = ( # ` { f | f : A -1-1-onto-> A } ) )
8 hashcl 
 |-  ( A e. Fin -> ( # ` A ) e. NN0 )
9 bcnn 
 |-  ( ( # ` A ) e. NN0 -> ( ( # ` A ) _C ( # ` A ) ) = 1 )
10 8 9 syl 
 |-  ( A e. Fin -> ( ( # ` A ) _C ( # ` A ) ) = 1 )
11 10 oveq2d 
 |-  ( A e. Fin -> ( ( ! ` ( # ` A ) ) x. ( ( # ` A ) _C ( # ` A ) ) ) = ( ( ! ` ( # ` A ) ) x. 1 ) )
12 8 faccld 
 |-  ( A e. Fin -> ( ! ` ( # ` A ) ) e. NN )
13 12 nncnd 
 |-  ( A e. Fin -> ( ! ` ( # ` A ) ) e. CC )
14 13 mulridd 
 |-  ( A e. Fin -> ( ( ! ` ( # ` A ) ) x. 1 ) = ( ! ` ( # ` A ) ) )
15 11 14 eqtrd 
 |-  ( A e. Fin -> ( ( ! ` ( # ` A ) ) x. ( ( # ` A ) _C ( # ` A ) ) ) = ( ! ` ( # ` A ) ) )
16 2 7 15 3eqtr3d 
 |-  ( A e. Fin -> ( # ` { f | f : A -1-1-onto-> A } ) = ( ! ` ( # ` A ) ) )