Definition df-efmnd 18423

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 18890 and symgvalstruct 18919. (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 18422	. 2 class EndoFMnd
2		vx	. . 3 setvar 𝑥
3		cvv 3422	. . 3 class V
4		vb	. . . 4 setvar 𝑏
5	2	cv 1538	. . . . 5 class 𝑥
6		cmap 8573	. . . . 5 class ↑m
7	5, 5, 6	co 7255	. . . 4 class (𝑥 ↑m 𝑥)
8		cnx 16822	. . . . . . 7 class ndx
9		cbs 16840	. . . . . . 7 class Base
10	8, 9	cfv 6418	. . . . . 6 class (Base‘ndx)
11	4	cv 1538	. . . . . 6 class 𝑏
12	10, 11	cop 4564	. . . . 5 class ⟨(Base‘ndx), 𝑏⟩
13		cplusg 16888	. . . . . . 7 class +g
14	8, 13	cfv 6418	. . . . . 6 class (+g‘ndx)
15		vf	. . . . . . 7 setvar 𝑓
16		vg	. . . . . . 7 setvar 𝑔
17	15	cv 1538	. . . . . . . 8 class 𝑓
18	16	cv 1538	. . . . . . . 8 class 𝑔
19	17, 18	ccom 5584	. . . . . . 7 class (𝑓 ∘ 𝑔)
20	15, 16, 11, 11, 19	cmpo 7257	. . . . . 6 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))
21	14, 20	cop 4564	. . . . 5 class ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩
22		cts 16894	. . . . . . 7 class TopSet
23	8, 22	cfv 6418	. . . . . 6 class (TopSet‘ndx)
24	5	cpw 4530	. . . . . . . . 9 class 𝒫 𝑥
25	24	csn 4558	. . . . . . . 8 class {𝒫 𝑥}
26	5, 25	cxp 5578	. . . . . . 7 class (𝑥 × {𝒫 𝑥})
27		cpt 17066	. . . . . . 7 class ∏t
28	26, 27	cfv 6418	. . . . . 6 class (∏t‘(𝑥 × {𝒫 𝑥}))
29	23, 28	cop 4564	. . . . 5 class ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩
30	12, 21, 29	ctp 4562	. . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
31	4, 7, 30	csb 3828	. . 3 class ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
32	2, 3, 31	cmpt 5153	. 2 class (𝑥 ∈ V ↦ ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})
33	1, 32	wceq 1539	1 wff EndoFMnd = (𝑥 ∈ V ↦ ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩})

This definition is referenced by:  efmnd  18424