Definition df-symgrp 10400

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.

Assertion

Ref	Expression
df-symgrp	|- SymGrp = {<.x, y>. | y = {<.<.f, g>., h>. | (f:x-1-1-onto->x /\ g:x-1-1-onto->x /\ h = (f o. g))}}

Distinct variable group:   x,y,f,g,h

Detailed syntax breakdown of Definition df-symgrp

Step	Hyp	Ref	Expression
1		csymgrp 10399	. 2 class SymGrp
2		vy	. . . . 5 set y
3	2	cv 955	. . . 4 class y
4		vx	. . . . . . . 8 set x
5	4	cv 955	. . . . . . 7 class x
6		vf	. . . . . . . 8 set f
7	6	cv 955	. . . . . . 7 class f
8	5, 5, 7	wf1o 3181	. . . . . 6 wff f:x-1-1-onto->x
9		vg	. . . . . . . 8 set g
10	9	cv 955	. . . . . . 7 class g
11	5, 5, 10	wf1o 3181	. . . . . 6 wff g:x-1-1-onto->x
12		vh	. . . . . . . 8 set h
13	12	cv 955	. . . . . . 7 class h
14	7, 10	ccom 3174	. . . . . . 7 class (f o. g)
15	13, 14	wceq 956	. . . . . 6 wff h = (f o. g)
16	8, 11, 15	w3a 775	. . . . 5 wff (f:x-1-1-onto->x /\ g:x-1-1-onto->x /\ h = (f o. g))
17	16, 6, 9, 12	copab2 3964	. . . 4 class {<.<.f, g>., h>. | (f:x-1-1-onto->x /\ g:x-1-1-onto->x /\ h = (f o. g))}
18	3, 17	wceq 956	. . 3 wff y = {<.<.f, g>., h>. | (f:x-1-1-onto->x /\ g:x-1-1-onto->x /\ h = (f o. g))}
19	18, 4, 2	copab 2666	. 2 class {<.x, y>. | y = {<.<.f, g>., h>. | (f:x-1-1-onto->x /\ g:x-1-1-onto->x /\ h = (f o. g))}}
20	1, 19	wceq 956	1 wff SymGrp = {<.x, y>. | y = {<.<.f, g>., h>. | (f:x-1-1-onto->x /\ g:x-1-1-onto->x /\ h = (f o. g))}}

This definition is referenced by:  symgval 10403

Copyright terms: Public domain