Definition df-efmnd 18882

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 19387 and symgvalstruct 19414. (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 18881	. 2 class EndoFMnd
2		vx	. . 3 setvar 𝑥
3		cvv 3480	. . 3 class V
4		vb	. . . 4 setvar 𝑏
5	2	cv 1539	. . . . 5 class 𝑥
6		cmap 8866	. . . . 5 class ↑m
7	5, 5, 6	co 7431	. . . 4 class (𝑥 ↑m 𝑥)
8		cnx 17230	. . . . . . 7 class ndx
9		cbs 17247	. . . . . . 7 class Base
10	8, 9	cfv 6561	. . . . . 6 class (Base‘ndx)
11	4	cv 1539	. . . . . 6 class 𝑏
12	10, 11	cop 4632	. . . . 5 class ⟨(Base‘ndx), 𝑏⟩
13		cplusg 17297	. . . . . . 7 class +g
14	8, 13	cfv 6561	. . . . . 6 class (+g‘ndx)
15		vf	. . . . . . 7 setvar 𝑓
16		vg	. . . . . . 7 setvar 𝑔
17	15	cv 1539	. . . . . . . 8 class 𝑓
18	16	cv 1539	. . . . . . . 8 class 𝑔
19	17, 18	ccom 5689	. . . . . . 7 class (𝑓 ∘ 𝑔)
20	15, 16, 11, 11, 19	cmpo 7433	. . . . . 6 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))
21	14, 20	cop 4632	. . . . 5 class ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩
22		cts 17303	. . . . . . 7 class TopSet
23	8, 22	cfv 6561	. . . . . 6 class (TopSet‘ndx)
24	5	cpw 4600	. . . . . . . . 9 class 𝒫 𝑥
25	24	csn 4626	. . . . . . . 8 class {𝒫 𝑥}
26	5, 25	cxp 5683	. . . . . . 7 class (𝑥 × {𝒫 𝑥})
27		cpt 17483	. . . . . . 7 class ∏t
28	26, 27	cfv 6561	. . . . . 6 class (∏t‘(𝑥 × {𝒫 𝑥}))
29	23, 28	cop 4632	. . . . 5 class ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩
30	12, 21, 29	ctp 4630	. . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
31	4, 7, 30	csb 3899	. . 3 class ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
32	2, 3, 31	cmpt 5225	. 2 class (𝑥 ∈ V ↦ ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
33	1, 32	wceq 1540	1 wff EndoFMnd = (𝑥 ∈ V ↦ ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})

This definition is referenced by:  efmnd  18883