Theorem symghash

Description: The symmetric group on n objects has cardinality n ! . (Contributed by Mario Carneiro, 22-Jan-2015)

	Ref	Expression
Hypotheses	symgbas.1	|- G = ( SymGrp ` A )
	symgbas.2	|- B = ( Base ` G )
Assertion	symghash	|- ( A e. Fin -> ( # ` B ) = ( ! ` ( # ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	|- G = ( SymGrp ` A )
2		symgbas.2	|- B = ( Base ` G )
3	1 2	symgbas	|- B = { f | f : A -1-1-onto-> A }
4	3	fveq2i	|- ( # ` B ) = ( # ` { f | f : A -1-1-onto-> A } )
5		hashfac	|- ( A e. Fin -> ( # ` { f | f : A -1-1-onto-> A } ) = ( ! ` ( # ` A ) ) )
6	4 5	eqtrid	|- ( A e. Fin -> ( # ` B ) = ( ! ` ( # ` A ) ) )