Metamath Proof Explorer


Theorem symgressbas

Description: The symmetric group on A characterized as structure restriction of the monoid of endofunctions on A to its base set. (Contributed by AV, 30-Mar-2024)

Ref Expression
Hypotheses symgbas.1
|- G = ( SymGrp ` A )
symgbas.2
|- B = ( Base ` G )
symgressbas.m
|- M = ( EndoFMnd ` A )
Assertion symgressbas
|- G = ( M |`s B )

Proof

Step Hyp Ref Expression
1 symgbas.1
 |-  G = ( SymGrp ` A )
2 symgbas.2
 |-  B = ( Base ` G )
3 symgressbas.m
 |-  M = ( EndoFMnd ` A )
4 eqid
 |-  { f | f : A -1-1-onto-> A } = { f | f : A -1-1-onto-> A }
5 1 4 symgval
 |-  G = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } )
6 1 2 symgbas
 |-  B = { f | f : A -1-1-onto-> A }
7 3 6 oveq12i
 |-  ( M |`s B ) = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } )
8 5 7 eqtr4i
 |-  G = ( M |`s B )