Definition df-bj-end 36281

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

Assertion

Ref	Expression
df-bj-end	⊢ End = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ {⟨(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)⟩, ⟨(+g‘ndx), (⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)⟩}))

Distinct variable group:   𝑥,𝑐

Detailed syntax breakdown of Definition df-bj-end

Step	Hyp	Ref	Expression
1		cend 36280	. 2 class End
2		vc	. . 3 setvar 𝑐
3		ccat 17610	. . 3 class Cat
4		vx	. . . 4 setvar 𝑥
5	2	cv 1540	. . . . 5 class 𝑐
6		cbs 17146	. . . . 5 class Base
7	5, 6	cfv 6543	. . . 4 class (Base‘𝑐)
8		cnx 17128	. . . . . . 7 class ndx
9	8, 6	cfv 6543	. . . . . 6 class (Base‘ndx)
10	4	cv 1540	. . . . . . 7 class 𝑥
11		chom 17210	. . . . . . . 8 class Hom
12	5, 11	cfv 6543	. . . . . . 7 class (Hom ‘𝑐)
13	10, 10, 12	co 7411	. . . . . 6 class (𝑥(Hom ‘𝑐)𝑥)
14	9, 13	cop 4634	. . . . 5 class ⟨(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)⟩
15		cplusg 17199	. . . . . . 7 class +g
16	8, 15	cfv 6543	. . . . . 6 class (+g‘ndx)
17	10, 10	cop 4634	. . . . . . 7 class ⟨𝑥, 𝑥⟩
18		cco 17211	. . . . . . . 8 class comp
19	5, 18	cfv 6543	. . . . . . 7 class (comp‘𝑐)
20	17, 10, 19	co 7411	. . . . . 6 class (⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)
21	16, 20	cop 4634	. . . . 5 class ⟨(+g‘ndx), (⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)⟩
22	14, 21	cpr 4630	. . . 4 class {⟨(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)⟩, ⟨(+g‘ndx), (⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)⟩}
23	4, 7, 22	cmpt 5231	. . 3 class (𝑥 ∈ (Base‘𝑐) ↦ {⟨(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)⟩, ⟨(+g‘ndx), (⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)⟩})
24	2, 3, 23	cmpt 5231	. 2 class (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ {⟨(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)⟩, ⟨(+g‘ndx), (⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)⟩}))
25	1, 24	wceq 1541	1 wff End = (𝑐 ∈ Cat ↦ (𝑥 ∈ (Base‘𝑐) ↦ {⟨(Base‘ndx), (𝑥(Hom ‘𝑐)𝑥)⟩, ⟨(+g‘ndx), (⟨𝑥, 𝑥⟩(comp‘𝑐)𝑥)⟩}))

This definition is referenced by:  bj-endval  36282