Definition df-efmnd 18030

Description: Define the monoid of endofunctions on set 𝑥. We represent the monoid as the set of functions from 𝑥 to itself ((𝑥 ↑_m 𝑥)) under function composition, and topologize it as a function space assuming the set is discrete. Analogous to the former definition of SymGrp, see df-symg 18492 and symgvalstruct 18521. (Contributed by AV, 25-Jan-2024.)

Assertion

Ref	Expression
df-efmnd	⊢ EndoFMnd = (𝑥 ∈ V ↦ ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})

Distinct variable group:   𝑓,𝑏,𝑔,𝑥

Detailed syntax breakdown of Definition df-efmnd

Step	Hyp	Ref	Expression
1		cefmnd 18029	. 2 class EndoFMnd
2		vx	. . 3 setvar 𝑥
3		cvv 3493	. . 3 class V
4		vb	. . . 4 setvar 𝑏
5	2	cv 1535	. . . . 5 class 𝑥
6		cmap 8403	. . . . 5 class ↑m
7	5, 5, 6	co 7153	. . . 4 class (𝑥 ↑m 𝑥)
8		cnx 16476	. . . . . . 7 class ndx
9		cbs 16479	. . . . . . 7 class Base
10	8, 9	cfv 6352	. . . . . 6 class (Base‘ndx)
11	4	cv 1535	. . . . . 6 class 𝑏
12	10, 11	cop 4570	. . . . 5 class ⟨(Base‘ndx), 𝑏⟩
13		cplusg 16561	. . . . . . 7 class +g
14	8, 13	cfv 6352	. . . . . 6 class (+g‘ndx)
15		vf	. . . . . . 7 setvar 𝑓
16		vg	. . . . . . 7 setvar 𝑔
17	15	cv 1535	. . . . . . . 8 class 𝑓
18	16	cv 1535	. . . . . . . 8 class 𝑔
19	17, 18	ccom 5556	. . . . . . 7 class (𝑓 ∘ 𝑔)
20	15, 16, 11, 11, 19	cmpo 7155	. . . . . 6 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))
21	14, 20	cop 4570	. . . . 5 class ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩
22		cts 16567	. . . . . . 7 class TopSet
23	8, 22	cfv 6352	. . . . . 6 class (TopSet‘ndx)
24	5	cpw 4536	. . . . . . . . 9 class 𝒫 𝑥
25	24	csn 4564	. . . . . . . 8 class {𝒫 𝑥}
26	5, 25	cxp 5550	. . . . . . 7 class (𝑥 × {𝒫 𝑥})
27		cpt 16708	. . . . . . 7 class ∏t
28	26, 27	cfv 6352	. . . . . 6 class (∏t‘(𝑥 × {𝒫 𝑥}))
29	23, 28	cop 4570	. . . . 5 class ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩
30	12, 21, 29	ctp 4568	. . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
31	4, 7, 30	csb 3880	. . 3 class ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
32	2, 3, 31	cmpt 5143	. 2 class (𝑥 ∈ V ↦ ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
33	1, 32	wceq 1536	1 wff EndoFMnd = (𝑥 ∈ V ↦ ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})

This definition is referenced by:  efmnd  18031