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	Could not format assertion : No typesetting found for |- SymGrp = ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) ) with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csymg	$$class\mathrm{SymGrp}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3		cefmnd	Could not format EndoFMnd : No typesetting found for class EndoFMnd with typecode class
4	1	cv	$$setvarx$$
5	4 3	cfv	Could not format ( EndoFMnd ` x ) : No typesetting found for class ( EndoFMnd ` x ) with typecode class
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	Could not format ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) : No typesetting found for class ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) with typecode class
12	1 2 11	cmpt	Could not format ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) ) : No typesetting found for class ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) ) with typecode class
13	0 12	wceq	Could not format SymGrp = ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) ) : No typesetting found for wff SymGrp = ( x e. _V |-> ( ( EndoFMnd ` x ) |`s { h | h : x -1-1-onto-> x } ) ) with typecode wff