Metamath Proof Explorer


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 ‘ 𝑐 ) 𝑥 ) ⟩ } ) )