Definition df-efmnd

Description: Define the monoid of endofunctions on set x . We represent the monoid as the set of functions from x to itself ( ( x ^m x ) ) 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 and symgvalstruct . (Contributed by AV, 25-Jan-2024)

	Ref	Expression
Assertion	df-efmnd	$$⊢\mathrm{EndoFMnd}=\left(x\in \mathrm{V}⟼⦋\left(x^x\right)/b⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(x\times \left\{𝒫x\right\}\right)⟩\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cefmnd	$$class\mathrm{EndoFMnd}$$
1		vx	$$setvarx$$
2		cvv	$$class\mathrm{V}$$
3	1	cv	$$setvarx$$
4		cmap	$$class{\uparrow }_{𝑚}$$
5	3 3 4	co	$$class\left(x^x\right)$$
6		vb	$$setvarb$$
7		cbs	$$class\mathrm{Base}$$
8		cnx	$$class\mathrm{ndx}$$
9	8 7	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
10	6	cv	$$setvarb$$
11	9 10	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩$$
12		cplusg	$$class{+}_{𝑔}$$
13	8 12	cfv	$$class{+}_{\mathrm{ndx}}$$
14		vf	$$setvarf$$
15		vg	$$setvarg$$
16	14	cv	$$setvarf$$
17	15	cv	$$setvarg$$
18	16 17	ccom	$$class\left(f\circ g\right)$$
19	14 15 10 10 18	cmpo	$$class\left(f\in b,g\in b⟼f\circ g\right)$$
20	13 19	cop	$$class⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼f\circ g\right)⟩$$
21		cts	$$class\mathrm{TopSet}$$
22	8 21	cfv	$$class\mathrm{TopSet}\left(\mathrm{ndx}\right)$$
23		cpt	$$class{\prod }_{𝑡}$$
24	3	cpw	$$class𝒫x$$
25	24	csn	$$class\left\{𝒫x\right\}$$
26	3 25	cxp	$$class\left(x\times \left\{𝒫x\right\}\right)$$
27	26 23	cfv	$$class{\prod }_{𝑡}\left(x\times \left\{𝒫x\right\}\right)$$
28	22 27	cop	$$class⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(x\times \left\{𝒫x\right\}\right)⟩$$
29	11 20 28	ctp	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(x\times \left\{𝒫x\right\}\right)⟩\right\}$$
30	6 5 29	csb	$$class⦋\left(x^x\right)/b⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(x\times \left\{𝒫x\right\}\right)⟩\right\}$$
31	1 2 30	cmpt	$$class\left(x\in \mathrm{V}⟼⦋\left(x^x\right)/b⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(x\times \left\{𝒫x\right\}\right)⟩\right\}\right)$$
32	0 31	wceq	$$wff\mathrm{EndoFMnd}=\left(x\in \mathrm{V}⟼⦋\left(x^x\right)/b⦌\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},b⟩,⟨{+}_{\mathrm{ndx}},\left(f\in b,g\in b⟼f\circ g\right)⟩,⟨\mathrm{TopSet}\left(\mathrm{ndx}\right),{\prod }_{𝑡}\left(x\times \left\{𝒫x\right\}\right)⟩\right\}\right)$$