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 ∈ V ⟼ EndoFMnd ⁡ x ↾ 𝑠 h | h : x ⟶ 1-1 onto x

Detailed syntax breakdown

Step Hyp Ref Expression
0 csymg class SymGrp
1 vx setvar x
2 cvv class V
3 cefmnd class EndoFMnd
4 1 cv setvar x
5 4 3 cfv class EndoFMnd ⁡ x
6 cress class ↾ 𝑠
7 vh setvar h
8 7 cv setvar h
9 4 4 8 wf1o wff h : x ⟶ 1-1 onto x
10 9 7 cab class h | h : x ⟶ 1-1 onto x
11 5 10 6 co class EndoFMnd ⁡ x ↾ 𝑠 h | h : x ⟶ 1-1 onto x
12 1 2 11 cmpt class x ∈ V ⟼ EndoFMnd ⁡ x ↾ 𝑠 h | h : x ⟶ 1-1 onto x
13 0 12 wceq wff SymGrp = x ∈ V ⟼ EndoFMnd ⁡ x ↾ 𝑠 h | h : x ⟶ 1-1 onto x