Definition df-symg 16198

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 16197	. 2 class SymGrp
2		vx	. . 3 setvar x
3		cvv 3113	. . 3 class _V
4		vb	. . . 4 setvar b
5	2	cv 1378	. . . . . 6 class x
6		vh	. . . . . . 7 setvar h
7	6	cv 1378	. . . . . 6 class h
8	5, 5, 7	wf1o 5585	. . . . 5 wff h : x -1-1-onto-> x
9	8, 6	cab 2452	. . . 4 class { h | h : x -1-1-onto-> x }
10		cnx 14483	. . . . . . 7 class ndx
11		cbs 14486	. . . . . . 7 class Base
12	10, 11	cfv 5586	. . . . . 6 class ( Base ` ndx )
13	4	cv 1378	. . . . . 6 class b
14	12, 13	cop 4033	. . . . 5 class <. ( Base ` ndx ) , b >.
15		cplusg 14551	. . . . . . 7 class +g
16	10, 15	cfv 5586	. . . . . 6 class ( +g ` ndx )
17		vf	. . . . . . 7 setvar f
18		vg	. . . . . . 7 setvar g
19	17	cv 1378	. . . . . . . 8 class f
20	18	cv 1378	. . . . . . . 8 class g
21	19, 20	ccom 5003	. . . . . . 7 class ( f o. g )
22	17, 18, 13, 13, 21	cmpt2 6284	. . . . . 6 class ( f e. b , g e. b |-> ( f o. g ) )
23	16, 22	cop 4033	. . . . 5 class <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >.
24		cts 14557	. . . . . . 7 class TopSet
25	10, 24	cfv 5586	. . . . . 6 class (TopSet ` ndx )
26	5	cpw 4010	. . . . . . . . 9 class ~P x
27	26	csn 4027	. . . . . . . 8 class { ~P x }
28	5, 27	cxp 4997	. . . . . . 7 class ( x X. { ~P x } )
29		cpt 14690	. . . . . . 7 class Xt_
30	28, 29	cfv 5586	. . . . . 6 class ( Xt_ ` ( x X. { ~P x } ) )
31	25, 30	cop 4033	. . . . 5 class <. (TopSet ` ndx ) , ( Xt_ ` ( x X. { ~P x } ) ) >.
32	14, 23, 31	ctp 4031	. . . 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 3435	. . 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 4505	. 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 1379	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  16199