Definition df-symg 18890

Description: Define the symmetric group on set 𝑥. We represent the group as the set of one-to-one onto functions from 𝑥 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.)

Assertion

Ref	Expression
df-symg	⊢ SymGrp = (𝑥 ∈ V ↦ ((EndoFMnd‘𝑥) ↾s {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥}))

Distinct variable group:   𝑥,ℎ

Detailed syntax breakdown of Definition df-symg

Step	Hyp	Ref	Expression
1		csymg 18889	. 2 class SymGrp
2		vx	. . 3 setvar 𝑥
3		cvv 3422	. . 3 class V
4	2	cv 1538	. . . . 5 class 𝑥
5		cefmnd 18422	. . . . 5 class EndoFMnd
6	4, 5	cfv 6418	. . . 4 class (EndoFMnd‘𝑥)
7		vh	. . . . . . 7 setvar ℎ
8	7	cv 1538	. . . . . 6 class ℎ
9	4, 4, 8	wf1o 6417	. . . . 5 wff ℎ:𝑥–1-1-onto→𝑥
10	9, 7	cab 2715	. . . 4 class {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥}
11		cress 16867	. . . 4 class ↾s
12	6, 10, 11	co 7255	. . 3 class ((EndoFMnd‘𝑥) ↾s {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥})
13	2, 3, 12	cmpt 5153	. 2 class (𝑥 ∈ V ↦ ((EndoFMnd‘𝑥) ↾s {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥}))
14	1, 13	wceq 1539	1 wff SymGrp = (𝑥 ∈ V ↦ ((EndoFMnd‘𝑥) ↾s {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥}))

This definition is referenced by:  symgval  18891