This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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