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 17738
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 17737 . 2 class SymGrp
2 vx . . 3 setvar 𝑥
3 cvv 3190 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1479 . . . . . 6 class 𝑥
6 vh . . . . . . 7 setvar
76cv 1479 . . . . . 6 class
85, 5, 7wf1o 5856 . . . . 5 wff :𝑥1-1-onto𝑥
98, 6cab 2607 . . . 4 class {:𝑥1-1-onto𝑥}
10 cnx 15797 . . . . . . 7 class ndx
11 cbs 15800 . . . . . . 7 class Base
1210, 11cfv 5857 . . . . . 6 class (Base‘ndx)
134cv 1479 . . . . . 6 class 𝑏
1412, 13cop 4161 . . . . 5 class ⟨(Base‘ndx), 𝑏
15 cplusg 15881 . . . . . . 7 class +g
1610, 15cfv 5857 . . . . . 6 class (+g‘ndx)
17 vf . . . . . . 7 setvar 𝑓
18 vg . . . . . . 7 setvar 𝑔
1917cv 1479 . . . . . . . 8 class 𝑓
2018cv 1479 . . . . . . . 8 class 𝑔
2119, 20ccom 5088 . . . . . . 7 class (𝑓𝑔)
2217, 18, 13, 13, 21cmpt2 6617 . . . . . 6 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))
2316, 22cop 4161 . . . . 5 class ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩
24 cts 15887 . . . . . . 7 class TopSet
2510, 24cfv 5857 . . . . . 6 class (TopSet‘ndx)
265cpw 4136 . . . . . . . . 9 class 𝒫 𝑥
2726csn 4155 . . . . . . . 8 class {𝒫 𝑥}
285, 27cxp 5082 . . . . . . 7 class (𝑥 × {𝒫 𝑥})
29 cpt 16039 . . . . . . 7 class t
3028, 29cfv 5857 . . . . . 6 class (∏t‘(𝑥 × {𝒫 𝑥}))
3125, 30cop 4161 . . . . 5 class ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩
3214, 23, 31ctp 4159 . . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
334, 9, 32csb 3519 . . 3 class {:𝑥1-1-onto𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
342, 3, 33cmpt 4683 . 2 class (𝑥 ∈ V ↦ {:𝑥1-1-onto𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
351, 34wceq 1480 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  17739
  Copyright terms: Public domain W3C validator