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