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

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