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 𝑠 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 𝑠 f | f : A 1-1 onto A
6 1 2 symgbas B = f | f : A 1-1 onto A
7 3 6 oveq12i M 𝑠 B = EndoFMnd A 𝑠 f | f : A 1-1 onto A
8 5 7 eqtr4i G = M 𝑠 B