Metamath Proof Explorer


Theorem symg1hash

Description: The symmetric group on a singleton has cardinality 1 . (Contributed by AV, 9-Dec-2018)

Ref Expression
Hypotheses symg1bas.1 G = SymGrp A
symg1bas.2 B = Base G
symg1bas.0 A = I
Assertion symg1hash I V B = 1

Proof

Step Hyp Ref Expression
1 symg1bas.1 G = SymGrp A
2 symg1bas.2 B = Base G
3 symg1bas.0 A = I
4 snfi I Fin
5 3 4 eqeltri A Fin
6 1 2 symghash A Fin B = A !
7 5 6 ax-mp B = A !
8 3 fveq2i A = I
9 hashsng I V I = 1
10 8 9 eqtrid I V A = 1
11 10 fveq2d I V A ! = 1 !
12 fac1 1 ! = 1
13 11 12 eqtrdi I V A ! = 1
14 7 13 eqtrid I V B = 1