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 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
symg1bas.2 ⊢ 𝐵 = ( Base ‘ 𝐺 )
symg1bas.0 ⊢ 𝐴 = { 𝐼 }
Assertion symg1hash ( 𝐼 ∈ 𝑉 → ( ♯ ‘ 𝐵 ) = 1 )

Proof

Step Hyp Ref Expression
1 symg1bas.1 ⊢ 𝐺 = ( SymGrp ‘ 𝐴 )
2 symg1bas.2 ⊢ 𝐵 = ( Base ‘ 𝐺 )
3 symg1bas.0 ⊢ 𝐴 = { 𝐼 }
4 snfi ⊢ { 𝐼 } ∈ Fin
5 3 4 eqeltri ⊢ 𝐴 ∈ Fin
6 1 2 symghash ⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐵 ) = ( ! ‘ ( ♯ ‘ 𝐴 ) ) )
7 5 6 ax-mp ⊢ ( ♯ ‘ 𝐵 ) = ( ! ‘ ( ♯ ‘ 𝐴 ) )
8 3 fveq2i ⊢ ( ♯ ‘ 𝐴 ) = ( ♯ ‘ { 𝐼 } )
9 hashsng ⊢ ( 𝐼 ∈ 𝑉 → ( ♯ ‘ { 𝐼 } ) = 1 )
10 8 9 eqtrid ⊢ ( 𝐼 ∈ 𝑉 → ( ♯ ‘ 𝐴 ) = 1 )
11 10 fveq2d ⊢ ( 𝐼 ∈ 𝑉 → ( ! ‘ ( ♯ ‘ 𝐴 ) ) = ( ! ‘ 1 ) )
12 fac1 ⊢ ( ! ‘ 1 ) = 1
13 11 12 eqtrdi ⊢ ( 𝐼 ∈ 𝑉 → ( ! ‘ ( ♯ ‘ 𝐴 ) ) = 1 )
14 7 13 eqtrid ⊢ ( 𝐼 ∈ 𝑉 → ( ♯ ‘ 𝐵 ) = 1 )