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

Definition df-symg 15085
 Description: Define the symmetry group on set . We represent the group as the set of 1-1-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 TopSet
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-symg
StepHypRef Expression
1 csymg 15084 . 2
2 vx . . 3
3 cvv 2948 . . 3
4 vb . . . 4
52cv 1651 . . . . . 6
6 vh . . . . . . 7
76cv 1651 . . . . . 6
85, 5, 7wf1o 5445 . . . . 5
98, 6cab 2421 . . . 4
10 cnx 13458 . . . . . . 7
11 cbs 13461 . . . . . . 7
1210, 11cfv 5446 . . . . . 6
134cv 1651 . . . . . 6
1412, 13cop 3809 . . . . 5
15 cplusg 13521 . . . . . . 7
1610, 15cfv 5446 . . . . . 6
17 vf . . . . . . 7
18 vg . . . . . . 7
1917cv 1651 . . . . . . . 8
2018cv 1651 . . . . . . . 8
2119, 20ccom 4874 . . . . . . 7
2217, 18, 13, 13, 21cmpt2 6075 . . . . . 6
2316, 22cop 3809 . . . . 5
24 cts 13527 . . . . . . 7 TopSet
2510, 24cfv 5446 . . . . . 6 TopSet
265cpw 3791 . . . . . . . . 9
2726csn 3806 . . . . . . . 8
285, 27cxp 4868 . . . . . . 7
29 cpt 13658 . . . . . . 7
3028, 29cfv 5446 . . . . . 6
3125, 30cop 3809 . . . . 5 TopSet
3214, 23, 31ctp 3808 . . . 4 TopSet
334, 9, 32csb 3243 . . 3 TopSet
342, 3, 33cmpt 4258 . 2 TopSet
351, 34wceq 1652 1 TopSet
 Colors of variables: wff set class This definition is referenced by:  symgval  15086
 Copyright terms: Public domain W3C validator