Definition df-efmnd 18517

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 18984 and symgvalstruct 19013. (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 18516	. 2 class EndoFMnd
2		vx	. . 3 setvar 𝑥
3		cvv 3433	. . 3 class V
4		vb	. . . 4 setvar 𝑏
5	2	cv 1538	. . . . 5 class 𝑥
6		cmap 8624	. . . . 5 class ↑m
7	5, 5, 6	co 7284	. . . 4 class (𝑥 ↑m 𝑥)
8		cnx 16903	. . . . . . 7 class ndx
9		cbs 16921	. . . . . . 7 class Base
10	8, 9	cfv 6437	. . . . . 6 class (Base‘ndx)
11	4	cv 1538	. . . . . 6 class 𝑏
12	10, 11	cop 4568	. . . . 5 class ⟨(Base‘ndx), 𝑏⟩
13		cplusg 16971	. . . . . . 7 class +g
14	8, 13	cfv 6437	. . . . . 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 5594	. . . . . . 7 class (𝑓 ∘ 𝑔)
20	15, 16, 11, 11, 19	cmpo 7286	. . . . . 6 class (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))
21	14, 20	cop 4568	. . . . 5 class ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩
22		cts 16977	. . . . . . 7 class TopSet
23	8, 22	cfv 6437	. . . . . 6 class (TopSet‘ndx)
24	5	cpw 4534	. . . . . . . . 9 class 𝒫 𝑥
25	24	csn 4562	. . . . . . . 8 class {𝒫 𝑥}
26	5, 25	cxp 5588	. . . . . . 7 class (𝑥 × {𝒫 𝑥})
27		cpt 17158	. . . . . . 7 class ∏t
28	26, 27	cfv 6437	. . . . . 6 class (∏t‘(𝑥 × {𝒫 𝑥}))
29	23, 28	cop 4568	. . . . 5 class ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩
30	12, 21, 29	ctp 4566	. . . 4 class {⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
31	4, 7, 30	csb 3833	. . 3 class ⦋(𝑥 ↑m 𝑥) / 𝑏⦌{⟨(Base‘ndx), 𝑏⟩, ⟨(+g‘ndx), (𝑓 ∈ 𝑏, 𝑔 ∈ 𝑏 ↦ (𝑓 ∘ 𝑔))⟩, ⟨(TopSet‘ndx), (∏t‘(𝑥 × {𝒫 𝑥}))⟩}
32	2, 3, 31	cmpt 5158	. 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  18518