This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- 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 } ) )