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 = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) ⟩ } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cend	⊢ End
1		vc	⊢ 𝑐
2		ccat	⊢ Cat
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑐
6	5 4	cfv	⊢ ( Base ‘ 𝑐 )
7		cnx	⊢ ndx
8	7 4	cfv	⊢ ( Base ‘ ndx )
9	3	cv	⊢ 𝑥
10		chom	⊢ Hom
11	5 10	cfv	⊢ ( Hom ‘ 𝑐 )
12	9 9 11	co	⊢ ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 )
13	8 12	cop	⊢ ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) ⟩
14		cplusg	⊢ +g
15	7 14	cfv	⊢ ( +g ‘ ndx )
16	9 9	cop	⊢ ⟨ 𝑥 , 𝑥 ⟩
17		cco	⊢ comp
18	5 17	cfv	⊢ ( comp ‘ 𝑐 )
19	16 9 18	co	⊢ ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑥 )
20	15 19	cop	⊢ ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) ⟩
21	13 20	cpr	⊢ { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) ⟩ }
22	3 6 21	cmpt	⊢ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) ⟩ } )
23	1 2 22	cmpt	⊢ ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) ⟩ } ) )
24	0 23	wceq	⊢ End = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) ⟩ } ) )