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=\mathrm{SymGrp}\left(A\right)$$
	symgbas.2	$$⊢B={\mathrm{Base}}_G$$
Assertion	symghash	$$⊢A\in \mathrm{Fin}\to \left|B\right|=\left|A\right|!$$

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgbas.2	$$⊢B={\mathrm{Base}}_G$$
3	1 2	symgbas	$$⊢B=\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
4	3	fveq2i	$$⊢\left|B\right|=\left|\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\right|$$
5		hashfac	$$⊢A\in \mathrm{Fin}\to \left|\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}\right|=\left|A\right|!$$
6	4 5	syl5eq	$$⊢A\in \mathrm{Fin}\to \left|B\right|=\left|A\right|!$$