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 ) |
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 ) |