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 17564
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. (Contributed by Paul Chapman, 25-Feb-2008.)
Assertion
Ref Expression
df-symg SymGrp = (𝑥 ∈ V ↦ {:𝑥1-1-onto𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
Distinct variable group:   𝑓,𝑏,𝑔,,𝑥

Detailed syntax breakdown of Definition df-symg
StepHypRef Expression
1 csymg 17563 . 2 class SymGrp
2 vx . . 3 setvar 𝑥
3 cvv 3169 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1473 . . . . . 6 class 𝑥
6 vh . . . . . . 7 setvar
76cv 1473 . . . . . 6 class
85, 5, 7wf1o 5786 . . . . 5 wff :𝑥1-1-onto𝑥
98, 6cab 2592 . . . 4 class {:𝑥1-1-onto𝑥}
10 cnx 15635 . . . . . . 7 class ndx
11 cbs 15638 . . . . . . 7 class Base
1210, 11cfv 5787 . . . . . 6 class (Base‘ndx)
134cv 1473 . . . . . 6 class 𝑏
1412, 13cop 4127 . . . . 5 class ⟨(Base‘ndx), 𝑏
15 cplusg 15711 . . . . . . 7 class +g
1610, 15cfv 5787 . . . . . 6 class (+g‘ndx)
17 vf . . . . . . 7 setvar 𝑓
18 vg . . . . . . 7 setvar 𝑔
1917cv 1473 . . . . . . . 8 class 𝑓
2018cv 1473 . . . . . . . 8 class 𝑔
2119, 20ccom 5029 . . . . . . 7 class (𝑓𝑔)
2217, 18, 13, 13, 21cmpt2 6526 . . . . . 6 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))
2316, 22cop 4127 . . . . 5 class ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩
24 cts 15717 . . . . . . 7 class TopSet
2510, 24cfv 5787 . . . . . 6 class (TopSet‘ndx)
265cpw 4104 . . . . . . . . 9 class 𝒫 𝑥
2726csn 4121 . . . . . . . 8 class {𝒫 𝑥}
285, 27cxp 5023 . . . . . . 7 class (𝑥 × {𝒫 𝑥})
29 cpt 15865 . . . . . . 7 class t
3028, 29cfv 5787 . . . . . 6 class (∏t‘(𝑥 × {𝒫 𝑥}))
3125, 30cop 4127 . . . . 5 class ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩
3214, 23, 31ctp 4125 . . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
334, 9, 32csb 3495 . . 3 class {:𝑥1-1-onto𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
342, 3, 33cmpt 4634 . 2 class (𝑥 ∈ V ↦ {:𝑥1-1-onto𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
351, 34wceq 1474 1 wff SymGrp = (𝑥 ∈ V ↦ {:𝑥1-1-onto𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
Colors of variables: wff setvar class
This definition is referenced by:  symgval  17565
  Copyright terms: Public domain W3C validator