MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-symg Structured version   Visualization version   GIF version

Definition df-symg 18488
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
StepHypRef Expression
1 csymg 18487 . 2 class SymGrp
2 vx . . 3 setvar 𝑥
3 cvv 3441 . . 3 class V
42cv 1537 . . . . 5 class 𝑥
5 cefmnd 18025 . . . . 5 class EndoFMnd
64, 5cfv 6324 . . . 4 class (EndoFMnd‘𝑥)
7 vh . . . . . . 7 setvar
87cv 1537 . . . . . 6 class
94, 4, 8wf1o 6323 . . . . 5 wff :𝑥1-1-onto𝑥
109, 7cab 2776 . . . 4 class {:𝑥1-1-onto𝑥}
11 cress 16476 . . . 4 class s
126, 10, 11co 7135 . . 3 class ((EndoFMnd‘𝑥) ↾s {:𝑥1-1-onto𝑥})
132, 3, 12cmpt 5110 . 2 class (𝑥 ∈ V ↦ ((EndoFMnd‘𝑥) ↾s {:𝑥1-1-onto𝑥}))
141, 13wceq 1538 1 wff SymGrp = (𝑥 ∈ V ↦ ((EndoFMnd‘𝑥) ↾s {:𝑥1-1-onto𝑥}))
Colors of variables: wff setvar class
This definition is referenced by:  symgval  18489
  Copyright terms: Public domain W3C validator