Definition df-symg 19387

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 19386	. 2 class SymGrp
2		vx	. . 3 setvar 𝑥
3		cvv 3480	. . 3 class V
4	2	cv 1539	. . . . 5 class 𝑥
5		cefmnd 18881	. . . . 5 class EndoFMnd
6	4, 5	cfv 6561	. . . 4 class (EndoFMnd‘𝑥)
7		vh	. . . . . . 7 setvar ℎ
8	7	cv 1539	. . . . . 6 class ℎ
9	4, 4, 8	wf1o 6560	. . . . 5 wff ℎ:𝑥–1-1-onto→𝑥
10	9, 7	cab 2714	. . . 4 class {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥}
11		cress 17274	. . . 4 class ↾s
12	6, 10, 11	co 7431	. . 3 class ((EndoFMnd‘𝑥) ↾s {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥})
13	2, 3, 12	cmpt 5225	. 2 class (𝑥 ∈ V ↦ ((EndoFMnd‘𝑥) ↾s {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥}))
14	1, 13	wceq 1540	1 wff SymGrp = (𝑥 ∈ V ↦ ((EndoFMnd‘𝑥) ↾s {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥}))

This definition is referenced by:  symgval  19388