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	|- SymGrp = ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csymg	|- SymGrp
1		vx	|- x
2		cvv	|- _V
3		cefmnd	|- EndoFMnd
4	1	cv	|- x
5	4 3	cfv	|- ( EndoFMnd ` x )
6		cress	|- |`s
7		vh	|- h
8	7	cv	|- h
9	4 4 8	wf1o	|- h : x -1-1-onto-> x
10	9 7	cab	|- { h | h : x -1-1-onto-> x }
11	5 10 6	co	|- ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } )
12	1 2 11	cmpt	|- ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) )
13	0 12	wceq	|- SymGrp = ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) )