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 = ( 𝑥 ∈ V ↦ ( ( EndoFMnd ‘ 𝑥 ) ↾s { : 𝑥1-1-onto𝑥 } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 csymg SymGrp
1 vx 𝑥
2 cvv V
3 cefmnd EndoFMnd
4 1 cv 𝑥
5 4 3 cfv ( EndoFMnd ‘ 𝑥 )
6 cress s
7 vh
8 7 cv
9 4 4 8 wf1o : 𝑥1-1-onto𝑥
10 9 7 cab { : 𝑥1-1-onto𝑥 }
11 5 10 6 co ( ( EndoFMnd ‘ 𝑥 ) ↾s { : 𝑥1-1-onto𝑥 } )
12 1 2 11 cmpt ( 𝑥 ∈ V ↦ ( ( EndoFMnd ‘ 𝑥 ) ↾s { : 𝑥1-1-onto𝑥 } ) )
13 0 12 wceq SymGrp = ( 𝑥 ∈ V ↦ ( ( EndoFMnd ‘ 𝑥 ) ↾s { : 𝑥1-1-onto𝑥 } ) )