Definition df-symg 17798

Description: Define the symmetric group on set 𝑥. We represent the group as the set of one-to-one 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	⊢ SymGrp = (𝑥 ∈ V ↦ ⦋{ℎ ∣ ℎ:𝑥–1-1-onto→𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})

Distinct variable group:   𝑓,𝑏,𝑔,ℎ,𝑥

Detailed syntax breakdown of Definition df-symg

Step	Hyp	Ref	Expression
1		csymg 17797	. 2 class SymGrp
2		vx	. . 3 setvar 𝑥
3		cvv 3200	. . 3 class V
4		vb	. . . 4 setvar 𝑏
5	2	cv 1482	. . . . . 6 class 𝑥
6		vh	. . . . . . 7 setvar ℎ
7	6	cv 1482	. . . . . 6 class ℎ
8	5, 5, 7	wf1o 5887	. . . . 5 wff ℎ:𝑥–1-1-onto→𝑥
9	8, 6	cab 2608	. . . 4 class {ℎ ∣ ℎ:𝑥–1-1-onto→𝑥}
10		cnx 15854	. . . . . . 7 class ndx
11		cbs 15857	. . . . . . 7 class Base
12	10, 11	cfv 5888	. . . . . 6 class (Base‘ndx)
13	4	cv 1482	. . . . . 6 class 𝑏
14	12, 13	cop 4183	. . . . 5 class ⟨(Base‘ndx), 𝑏⟩
15		cplusg 15941	. . . . . . 7 class +g
16	10, 15	cfv 5888	. . . . . 6 class (+g‘ndx)
17		vf	. . . . . . 7 setvar 𝑓
18		vg	. . . . . . 7 setvar 𝑔
19	17	cv 1482	. . . . . . . 8 class 𝑓
20	18	cv 1482	. . . . . . . 8 class 𝑔
21	19, 20	ccom 5118	. . . . . . 7 class (𝑓 ∘ 𝑔)
22	17, 18, 13, 13, 21	cmpt2 6652	. . . . . 6 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))
23	16, 22	cop 4183	. . . . 5 class ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩
24		cts 15947	. . . . . . 7 class TopSet
25	10, 24	cfv 5888	. . . . . 6 class (TopSet‘ndx)
26	5	cpw 4158	. . . . . . . . 9 class 𝒫 𝑥
27	26	csn 4177	. . . . . . . 8 class {𝒫 𝑥}
28	5, 27	cxp 5112	. . . . . . 7 class (𝑥 × {𝒫 𝑥})
29		cpt 16099	. . . . . . 7 class ∏t
30	28, 29	cfv 5888	. . . . . 6 class (∏t‘(𝑥 × {𝒫 𝑥}))
31	25, 30	cop 4183	. . . . 5 class ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩
32	14, 23, 31	ctp 4181	. . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
33	4, 9, 32	csb 3533	. . 3 class ⦋{ℎ ∣ ℎ:𝑥–1-1-onto→𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
34	2, 3, 33	cmpt 4729	. 2 class (𝑥 ∈ V ↦ ⦋{ℎ ∣ ℎ:𝑥–1-1-onto→𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
35	1, 34	wceq 1483	1 wff SymGrp = (𝑥 ∈ V ↦ ⦋{ℎ ∣ ℎ:𝑥–1-1-onto→𝑥} / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})

This definition is referenced by:  symgval  17799