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	No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
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	Could not format M = ( EndoFMnd ` A ) : No typesetting found for |- M = ( EndoFMnd ` A ) with typecode |-
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	Could not format G = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) : No typesetting found for |- G = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) with typecode |-
6	1 2	symgbas	$$⊢B=\left\{f|f:A\underset{1-1\; onto}{⟶}A\right\}$$
7	3 6	oveq12i	Could not format ( M |`s B ) = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) : No typesetting found for |- ( M |`s B ) = ( ( EndoFMnd ` A ) |`s { f | f : A -1-1-onto-> A } ) with typecode |-
8	5 7	eqtr4i	$$⊢G=M{\upharpoonright }_{𝑠}B$$