Definition df-symg 16602

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

Step	Hyp	Ref	Expression
1		csymg 16601	. 2 class SymGrp
2		vx	. . 3 setvar x
3		cvv 3106	. . 3 class _V
4		vb	. . . 4 setvar b
5	2	cv 1397	. . . . . 6 class x
6		vh	. . . . . . 7 setvar h
7	6	cv 1397	. . . . . 6 class h
8	5, 5, 7	wf1o 5569	. . . . 5 wff h : x -1-1-onto-> x
9	8, 6	cab 2439	. . . 4 class { h | h : x -1-1-onto-> x }
10		cnx 14713	. . . . . . 7 class ndx
11		cbs 14716	. . . . . . 7 class Base
12	10, 11	cfv 5570	. . . . . 6 class ( Base ` ndx )
13	4	cv 1397	. . . . . 6 class b
14	12, 13	cop 4022	. . . . 5 class <. ( Base ` ndx ) , b >.
15		cplusg 14784	. . . . . . 7 class +g
16	10, 15	cfv 5570	. . . . . 6 class ( +g ` ndx )
17		vf	. . . . . . 7 setvar f
18		vg	. . . . . . 7 setvar g
19	17	cv 1397	. . . . . . . 8 class f
20	18	cv 1397	. . . . . . . 8 class g
21	19, 20	ccom 4992	. . . . . . 7 class ( f o. g )
22	17, 18, 13, 13, 21	cmpt2 6272	. . . . . 6 class ( f e. b , g e. b |-> ( f o. g ) )
23	16, 22	cop 4022	. . . . 5 class <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >.
24		cts 14790	. . . . . . 7 class TopSet
25	10, 24	cfv 5570	. . . . . 6 class (TopSet ` ndx )
26	5	cpw 3999	. . . . . . . . 9 class ~P x
27	26	csn 4016	. . . . . . . 8 class { ~P x }
28	5, 27	cxp 4986	. . . . . . 7 class ( x X. { ~P x } )
29		cpt 14928	. . . . . . 7 class Xt_
30	28, 29	cfv 5570	. . . . . 6 class ( Xt_ ` ( x X. { ~P x } ) )
31	25, 30	cop 4022	. . . . 5 class <. (TopSet ` ndx ) , ( Xt_ ` ( x X. { ~P x } ) ) >.
32	14, 23, 31	ctp 4020	. . . 4 class { <. ( Base ` ndx ) , b >. , <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >. , <. (TopSet ` ndx ) , ( Xt_ ` ( x X. { ~P x } ) ) >. }
33	4, 9, 32	csb 3420	. . 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 } ) ) >. }
34	2, 3, 33	cmpt 4497	. 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 } ) ) >. } )
35	1, 34	wceq 1398	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 } ) ) >. } )

This definition is referenced by:  symgval  16603