Definition df-symg

Description: Define the symmetric group on set x . We represent the group as the set of one-to-one onto functions from x to itself under function composition, and topologize it as a function space assuming the set is discrete. This definition is based on the fact that a symmetric group is a restriction of the monoid of endofunctions. (Contributed by Paul Chapman, 25-Feb-2008) (Revised by AV, 28-Mar-2024)

	Ref	Expression
Assertion	df-symg	$$⊢\mathrm{SymGrp}=\left(x\in \mathrm{V}⟼\mathrm{EndoFMnd}\left(x\right){\upharpoonright }_{𝑠}\left\{h|h:x\underset{1-1\; onto}{⟶}x\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csymg	$$class\mathrm{SymGrp}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		cefmnd	$$class\mathrm{EndoFMnd}$$
4	1	cv	$$setvarx$$
5	4 3	cfv	$$class\mathrm{EndoFMnd}\left(x\right)$$
6		cress	$$class{\upharpoonright }_{𝑠}$$
7		vh	$$setvarh$$
8	7	cv	$$setvarh$$
9	4 4 8	wf1o	$$wffh:x\underset{1-1\; onto}{⟶}x$$
10	9 7	cab	$$class\left\{h|h:x\underset{1-1\; onto}{⟶}x\right\}$$
11	5 10 6	co	$$class\left(\mathrm{EndoFMnd}\left(x\right){\upharpoonright }_{𝑠}\left\{h|h:x\underset{1-1\; onto}{⟶}x\right\}\right)$$
12	1 2 11	cmpt	$$class\left(x\in \mathrm{V}⟼\mathrm{EndoFMnd}\left(x\right){\upharpoonright }_{𝑠}\left\{h|h:x\underset{1-1\; onto}{⟶}x\right\}\right)$$
13	0 12	wceq	$$wff\mathrm{SymGrp}=\left(x\in \mathrm{V}⟼\mathrm{EndoFMnd}\left(x\right){\upharpoonright }_{𝑠}\left\{h|h:x\underset{1-1\; onto}{⟶}x\right\}\right)$$