Definition df-bj-end

Description: The monoid of endomorphisms on an object of a category. (Contributed by BJ, 4-Apr-2024)

	Ref	Expression
Assertion	df-bj-end	$$⊢End=\left(c\in \mathrm{Cat}⟼\left(x\in {\mathrm{Base}}_c⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(c\right)x⟩,⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(c\right)x⟩\right\}\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cend	$$classEnd$$
1		vc	$$setvarc$$
2		ccat	$$class\mathrm{Cat}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarc$$
6	5 4	cfv	$$class{\mathrm{Base}}_c$$
7		cnx	$$class\mathrm{ndx}$$
8	7 4	cfv	$$class{\mathrm{Base}}_{\mathrm{ndx}}$$
9	3	cv	$$setvarx$$
10		chom	$$class\mathrm{Hom}$$
11	5 10	cfv	$$class\mathrm{Hom}\left(c\right)$$
12	9 9 11	co	$$class\left(x\mathrm{Hom}\left(c\right)x\right)$$
13	8 12	cop	$$class⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(c\right)x⟩$$
14		cplusg	$$class{+}_{𝑔}$$
15	7 14	cfv	$$class{+}_{\mathrm{ndx}}$$
16	9 9	cop	$$class⟨x,x⟩$$
17		cco	$$class\mathrm{comp}$$
18	5 17	cfv	$$class\mathrm{comp}\left(c\right)$$
19	16 9 18	co	$$class\left(⟨x,x⟩\mathrm{comp}\left(c\right)x\right)$$
20	15 19	cop	$$class⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(c\right)x⟩$$
21	13 20	cpr	$$class\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(c\right)x⟩,⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(c\right)x⟩\right\}$$
22	3 6 21	cmpt	$$class\left(x\in {\mathrm{Base}}_c⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(c\right)x⟩,⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(c\right)x⟩\right\}\right)$$
23	1 2 22	cmpt	$$class\left(c\in \mathrm{Cat}⟼\left(x\in {\mathrm{Base}}_c⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(c\right)x⟩,⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(c\right)x⟩\right\}\right)\right)$$
24	0 23	wceq	$$wffEnd=\left(c\in \mathrm{Cat}⟼\left(x\in {\mathrm{Base}}_c⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(c\right)x⟩,⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(c\right)x⟩\right\}\right)\right)$$