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=\mathrm{SymGrp}\left(A\right)$$
	symgbas.2	$$⊢B={\mathrm{Base}}_G$$
	symgressbas.m	$$⊢M=\mathrm{EndoFMnd}\left(A\right)$$
Assertion	symgressbas	$$⊢G=M{\upharpoonright }_{𝑠}B$$

Proof

Step	Hyp	Ref	Expression
1		symgbas.1	$$⊢G=\mathrm{SymGrp}\left(A\right)$$
2		symgbas.2	$$⊢B={\mathrm{Base}}_G$$
3		symgressbas.m	$$⊢M=\mathrm{EndoFMnd}\left(A\right)$$
4		eqid	$$⊢\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}=\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
5	1 4	symgval	$$⊢G=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
6	1 2	symgbas	$$⊢B=\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
7	3 6	oveq12i	$$⊢M{\upharpoonright }_{𝑠}B=\mathrm{EndoFMnd}\left(A\right){\upharpoonright }_{𝑠}\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
8	5 7	eqtr4i	$$⊢G=M{\upharpoonright }_{𝑠}B$$