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

Metamath Proof Explorer

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 ∈ 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 ∈ Fin → f | f : A ⟶ 1-1 onto A = A !
6 4 5 eqtrid ⊢ A ∈ Fin → B = A !