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 17999
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 17998 . 2 class SymGrp
2 vx . . 3 setvar 𝑥
3 cvv 3391 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1636 . . . . . 6 class 𝑥
6 vh . . . . . . 7 setvar
76cv 1636 . . . . . 6 class
85, 5, 7wf1o 6100 . . . . 5 wff :𝑥1-1-onto𝑥
98, 6cab 2792 . . . 4 class {:𝑥1-1-onto𝑥}
10 cnx 16065 . . . . . . 7 class ndx
11 cbs 16068 . . . . . . 7 class Base
1210, 11cfv 6101 . . . . . 6 class (Base‘ndx)
134cv 1636 . . . . . 6 class 𝑏
1412, 13cop 4376 . . . . 5 class ⟨(Base‘ndx), 𝑏
15 cplusg 16153 . . . . . . 7 class +g
1610, 15cfv 6101 . . . . . 6 class (+g‘ndx)
17 vf . . . . . . 7 setvar 𝑓
18 vg . . . . . . 7 setvar 𝑔
1917cv 1636 . . . . . . . 8 class 𝑓
2018cv 1636 . . . . . . . 8 class 𝑔
2119, 20ccom 5315 . . . . . . 7 class (𝑓𝑔)
2217, 18, 13, 13, 21cmpt2 6876 . . . . . 6 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))
2316, 22cop 4376 . . . . 5 class ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩
24 cts 16159 . . . . . . 7 class TopSet
2510, 24cfv 6101 . . . . . 6 class (TopSet‘ndx)
265cpw 4351 . . . . . . . . 9 class 𝒫 𝑥
2726csn 4370 . . . . . . . 8 class {𝒫 𝑥}
285, 27cxp 5309 . . . . . . 7 class (𝑥 × {𝒫 𝑥})
29 cpt 16304 . . . . . . 7 class t
3028, 29cfv 6101 . . . . . 6 class (∏t‘(𝑥 × {𝒫 𝑥}))
3125, 30cop 4376 . . . . 5 class ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩
3214, 23, 31ctp 4374 . . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
334, 9, 32csb 3728 . . 3 class {:𝑥1-1-onto𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
342, 3, 33cmpt 4923 . 2 class (𝑥 ∈ V ↦ {:𝑥1-1-onto𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
351, 34wceq 1637 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  18000
  Copyright terms: Public domain W3C validator