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 18436
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 18435 . 2 class SymGrp
2 vx . . 3 setvar 𝑥
3 cvv 3495 . . 3 class V
4 vb . . . 4 setvar 𝑏
52cv 1527 . . . . . 6 class 𝑥
6 vh . . . . . . 7 setvar
76cv 1527 . . . . . 6 class
85, 5, 7wf1o 6348 . . . . 5 wff :𝑥1-1-onto𝑥
98, 6cab 2799 . . . 4 class {:𝑥1-1-onto𝑥}
10 cnx 16470 . . . . . . 7 class ndx
11 cbs 16473 . . . . . . 7 class Base
1210, 11cfv 6349 . . . . . 6 class (Base‘ndx)
134cv 1527 . . . . . 6 class 𝑏
1412, 13cop 4565 . . . . 5 class ⟨(Base‘ndx), 𝑏
15 cplusg 16555 . . . . . . 7 class +g
1610, 15cfv 6349 . . . . . 6 class (+g‘ndx)
17 vf . . . . . . 7 setvar 𝑓
18 vg . . . . . . 7 setvar 𝑔
1917cv 1527 . . . . . . . 8 class 𝑓
2018cv 1527 . . . . . . . 8 class 𝑔
2119, 20ccom 5553 . . . . . . 7 class (𝑓𝑔)
2217, 18, 13, 13, 21cmpo 7147 . . . . . 6 class (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))
2316, 22cop 4565 . . . . 5 class ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩
24 cts 16561 . . . . . . 7 class TopSet
2510, 24cfv 6349 . . . . . 6 class (TopSet‘ndx)
265cpw 4537 . . . . . . . . 9 class 𝒫 𝑥
2726csn 4559 . . . . . . . 8 class {𝒫 𝑥}
285, 27cxp 5547 . . . . . . 7 class (𝑥 × {𝒫 𝑥})
29 cpt 16702 . . . . . . 7 class t
3028, 29cfv 6349 . . . . . 6 class (∏t‘(𝑥 × {𝒫 𝑥}))
3125, 30cop 4565 . . . . 5 class ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩
3214, 23, 31ctp 4563 . . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
334, 9, 32csb 3882 . . 3 class {:𝑥1-1-onto𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
342, 3, 33cmpt 5138 . 2 class (𝑥 ∈ V ↦ {:𝑥1-1-onto𝑥} / 𝑏{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓𝑏, 𝑔𝑏 ↦ (𝑓𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
351, 34wceq 1528 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  18437
  Copyright terms: Public domain W3C validator