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

Definition df-symg 14770
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 14769 . 2  class  SymGrp
2 vx . . 3  set  x
3 cvv 2788 . . 3  class  _V
4 vb . . . 4  set  b
52cv 1622 . . . . . 6  class  x
6 vh . . . . . . 7  set  h
76cv 1622 . . . . . 6  class  h
85, 5, 7wf1o 5254 . . . . 5  wff  h : x -1-1-onto-> x
98, 6cab 2269 . . . 4  class  { h  |  h : x -1-1-onto-> x }
10 cnx 13145 . . . . . . 7  class  ndx
11 cbs 13148 . . . . . . 7  class  Base
1210, 11cfv 5255 . . . . . 6  class  ( Base `  ndx )
134cv 1622 . . . . . 6  class  b
1412, 13cop 3643 . . . . 5  class  <. ( Base `  ndx ) ,  b >.
15 cplusg 13208 . . . . . . 7  class  +g
1610, 15cfv 5255 . . . . . 6  class  ( +g  ` 
ndx )
17 vf . . . . . . 7  set  f
18 vg . . . . . . 7  set  g
1917cv 1622 . . . . . . . 8  class  f
2018cv 1622 . . . . . . . 8  class  g
2119, 20ccom 4693 . . . . . . 7  class  ( f  o.  g )
2217, 18, 13, 13, 21cmpt2 5860 . . . . . 6  class  ( f  e.  b ,  g  e.  b  |->  ( f  o.  g ) )
2316, 22cop 3643 . . . . 5  class  <. ( +g  `  ndx ) ,  ( f  e.  b ,  g  e.  b 
|->  ( f  o.  g
) ) >.
24 cts 13214 . . . . . . 7  class TopSet
2510, 24cfv 5255 . . . . . 6  class  (TopSet `  ndx )
265cpw 3625 . . . . . . . . 9  class  ~P x
2726csn 3640 . . . . . . . 8  class  { ~P x }
285, 27cxp 4687 . . . . . . 7  class  ( x  X.  { ~P x } )
29 cpt 13343 . . . . . . 7  class  Xt_
3028, 29cfv 5255 . . . . . 6  class  ( Xt_ `  ( x  X.  { ~P x } ) )
3125, 30cop 3643 . . . . 5  class  <. (TopSet ` 
ndx ) ,  (
Xt_ `  ( x  X.  { ~P x }
) ) >.
3214, 23, 31ctp 3642 . . . 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 3081 . . 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 4077 . 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 1623 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  14771
  Copyright terms: Public domain W3C validator