Metamath Proof Explorer


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 classSymGrp
1 vx setvarx
2 cvv classV
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𝑠
7 vh setvarh
8 7 cv setvarh
9 4 4 8 wf1o wffh:x1-1 ontox
10 9 7 cab classh|h:x1-1 ontox
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