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

Definition df-symg 14786
Description: Define the symmetry group on set  x. We represent the group as the set of 1-1-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 14785 . 2  class  SymGrp
2 vx . . 3  set  x
3 cvv 2801 . . 3  class  _V
4 vb . . . 4  set  b
52cv 1631 . . . . . 6  class  x
6 vh . . . . . . 7  set  h
76cv 1631 . . . . . 6  class  h
85, 5, 7wf1o 5270 . . . . 5  wff  h : x -1-1-onto-> x
98, 6cab 2282 . . . 4  class  { h  |  h : x -1-1-onto-> x }
10 cnx 13161 . . . . . . 7  class  ndx
11 cbs 13164 . . . . . . 7  class  Base
1210, 11cfv 5271 . . . . . 6  class  ( Base `  ndx )
134cv 1631 . . . . . 6  class  b
1412, 13cop 3656 . . . . 5  class  <. ( Base `  ndx ) ,  b >.
15 cplusg 13224 . . . . . . 7  class  +g
1610, 15cfv 5271 . . . . . 6  class  ( +g  ` 
ndx )
17 vf . . . . . . 7  set  f
18 vg . . . . . . 7  set  g
1917cv 1631 . . . . . . . 8  class  f
2018cv 1631 . . . . . . . 8  class  g
2119, 20ccom 4709 . . . . . . 7  class  ( f  o.  g )
2217, 18, 13, 13, 21cmpt2 5876 . . . . . 6  class  ( f  e.  b ,  g  e.  b  |->  ( f  o.  g ) )
2316, 22cop 3656 . . . . 5  class  <. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b 
|->  ( f  o.  g
) ) >.
24 cts 13230 . . . . . . 7  class TopSet
2510, 24cfv 5271 . . . . . 6  class  (TopSet `  ndx )
265cpw 3638 . . . . . . . . 9  class  ~P x
2726csn 3653 . . . . . . . 8  class  { ~P x }
285, 27cxp 4703 . . . . . . 7  class  ( x  X.  { ~P x } )
29 cpt 13359 . . . . . . 7  class  Xt_
3028, 29cfv 5271 . . . . . 6  class  ( Xt_ `  ( x  X.  { ~P x } ) )
3125, 30cop 3656 . . . . 5  class  <. (TopSet ` 
ndx ) ,  (
Xt_ `  ( x  X.  { ~P x }
) ) >.
3214, 23, 31ctp 3655 . . . 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 3094 . . 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 4093 . 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 1632 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 set class
This definition is referenced by:  symgval  14787
  Copyright terms: Public domain W3C validator