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

Definition df-symg 15994
Description: Define the symmetric group on set  x. We represent the group as the set of one-to-one onto functions from  x 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  =  ( x  e.  _V  |->  [_ { h  |  h : x -1-1-onto-> x }  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( f  o.  g ) ) >. ,  <. (TopSet `  ndx ) ,  ( Xt_ `  ( x  X.  { ~P x } ) )
>. } )
Distinct variable group:    f, b, g, h, x

Detailed syntax breakdown of Definition df-symg
StepHypRef Expression
1 csymg 15993 . 2  class  SymGrp
2 vx . . 3  setvar  x
3 cvv 3071 . . 3  class  _V
4 vb . . . 4  setvar  b
52cv 1369 . . . . . 6  class  x
6 vh . . . . . . 7  setvar  h
76cv 1369 . . . . . 6  class  h
85, 5, 7wf1o 5518 . . . . 5  wff  h : x -1-1-onto-> x
98, 6cab 2436 . . . 4  class  { h  |  h : x -1-1-onto-> x }
10 cnx 14282 . . . . . . 7  class  ndx
11 cbs 14285 . . . . . . 7  class  Base
1210, 11cfv 5519 . . . . . 6  class  ( Base `  ndx )
134cv 1369 . . . . . 6  class  b
1412, 13cop 3984 . . . . 5  class  <. ( Base `  ndx ) ,  b >.
15 cplusg 14349 . . . . . . 7  class  +g
1610, 15cfv 5519 . . . . . 6  class  ( +g  ` 
ndx )
17 vf . . . . . . 7  setvar  f
18 vg . . . . . . 7  setvar  g
1917cv 1369 . . . . . . . 8  class  f
2018cv 1369 . . . . . . . 8  class  g
2119, 20ccom 4945 . . . . . . 7  class  ( f  o.  g )
2217, 18, 13, 13, 21cmpt2 6195 . . . . . 6  class  ( f  e.  b ,  g  e.  b  |->  ( f  o.  g ) )
2316, 22cop 3984 . . . . 5  class  <. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b 
|->  ( f  o.  g
) ) >.
24 cts 14355 . . . . . . 7  class TopSet
2510, 24cfv 5519 . . . . . 6  class  (TopSet `  ndx )
265cpw 3961 . . . . . . . . 9  class  ~P x
2726csn 3978 . . . . . . . 8  class  { ~P x }
285, 27cxp 4939 . . . . . . 7  class  ( x  X.  { ~P x } )
29 cpt 14488 . . . . . . 7  class  Xt_
3028, 29cfv 5519 . . . . . 6  class  ( Xt_ `  ( x  X.  { ~P x } ) )
3125, 30cop 3984 . . . . 5  class  <. (TopSet ` 
ndx ) ,  (
Xt_ `  ( x  X.  { ~P x }
) ) >.
3214, 23, 31ctp 3982 . . . 4  class  { <. (
Base `  ndx ) ,  b >. ,  <. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b 
|->  ( f  o.  g
) ) >. ,  <. (TopSet `  ndx ) ,  (
Xt_ `  ( x  X.  { ~P x }
) ) >. }
334, 9, 32csb 3389 . . 3  class  [_ {
h  |  h : x -1-1-onto-> x }  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( f  o.  g ) ) >. ,  <. (TopSet `  ndx ) ,  ( Xt_ `  ( x  X.  { ~P x } ) )
>. }
342, 3, 33cmpt 4451 . 2  class  ( x  e.  _V  |->  [_ {
h  |  h : x -1-1-onto-> x }  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( f  o.  g ) ) >. ,  <. (TopSet `  ndx ) ,  ( Xt_ `  ( x  X.  { ~P x } ) )
>. } )
351, 34wceq 1370 1  wff  SymGrp  =  ( x  e.  _V  |->  [_ { h  |  h : x -1-1-onto-> x }  /  b ]_ { <. ( Base `  ndx ) ,  b >. , 
<. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b  |->  ( f  o.  g ) ) >. ,  <. (TopSet `  ndx ) ,  ( Xt_ `  ( x  X.  { ~P x } ) )
>. } )
Colors of variables: wff setvar class
This definition is referenced by:  symgval  15995
  Copyright terms: Public domain W3C validator