Definition df-symg 17067

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 17066	. 2 class SymGrp
2		vx	. . 3 setvar x
3		cvv 3056	. . 3 class _V
4		vb	. . . 4 setvar b
5	2	cv 1453	. . . . . 6 class x
6		vh	. . . . . . 7 setvar h
7	6	cv 1453	. . . . . 6 class h
8	5, 5, 7	wf1o 5599	. . . . 5 wff h : x -1-1-onto-> x
9	8, 6	cab 2447	. . . 4 class { h | h : x -1-1-onto-> x }
10		cnx 15166	. . . . . . 7 class ndx
11		cbs 15169	. . . . . . 7 class Base
12	10, 11	cfv 5600	. . . . . 6 class ( Base ` ndx )
13	4	cv 1453	. . . . . 6 class b
14	12, 13	cop 3985	. . . . 5 class <. ( Base ` ndx ) , b >.
15		cplusg 15238	. . . . . . 7 class +g
16	10, 15	cfv 5600	. . . . . 6 class ( +g ` ndx )
17		vf	. . . . . . 7 setvar f
18		vg	. . . . . . 7 setvar g
19	17	cv 1453	. . . . . . . 8 class f
20	18	cv 1453	. . . . . . . 8 class g
21	19, 20	ccom 4856	. . . . . . 7 class ( f o. g )
22	17, 18, 13, 13, 21	cmpt2 6316	. . . . . 6 class ( f e. b , g e. b |-> ( f o. g ) )
23	16, 22	cop 3985	. . . . 5 class <. ( +g ` ndx ) , ( f e. b , g e. b |-> ( f o. g ) ) >.
24		cts 15244	. . . . . . 7 class TopSet
25	10, 24	cfv 5600	. . . . . 6 class (TopSet ` ndx )
26	5	cpw 3962	. . . . . . . . 9 class ~P x
27	26	csn 3979	. . . . . . . 8 class { ~P x }
28	5, 27	cxp 4850	. . . . . . 7 class ( x X. { ~P x } )
29		cpt 15385	. . . . . . 7 class Xt_
30	28, 29	cfv 5600	. . . . . 6 class ( Xt_ ` ( x X. { ~P x } ) )
31	25, 30	cop 3985	. . . . 5 class <. (TopSet ` ndx ) , ( Xt_ ` ( x X. { ~P x } ) ) >.
32	14, 23, 31	ctp 3983	. . . 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 3374	. . 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 4474	. 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 1454	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  17068