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 e. 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 } e. Fin
5 3 4 eqeltri 
 |-  A e. Fin
6 1 2 symghash 
 |-  ( A e. Fin -> ( # ` B ) = ( ! ` ( # ` A ) ) )
7 5 6 ax-mp 
 |-  ( # ` B ) = ( ! ` ( # ` A ) )
8 3 fveq2i 
 |-  ( # ` A ) = ( # ` { I } )
9 hashsng 
 |-  ( I e. V -> ( # ` { I } ) = 1 )
10 8 9 eqtrid 
 |-  ( I e. V -> ( # ` A ) = 1 )
11 10 fveq2d 
 |-  ( I e. V -> ( ! ` ( # ` A ) ) = ( ! ` 1 ) )
12 fac1 
 |-  ( ! ` 1 ) = 1
13 11 12 eqtrdi 
 |-  ( I e. V -> ( ! ` ( # ` A ) ) = 1 )
14 7 13 eqtrid 
 |-  ( I e. V -> ( # ` B ) = 1 )