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 )