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 = ( c e. Cat |-> ( x e. ( Base ` c ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. } ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cend 
 |-  End
1 vc 
 |-  c
2 ccat 
 |-  Cat
3 vx 
 |-  x
4 cbs 
 |-  Base
5 1 cv 
 |-  c
6 5 4 cfv 
 |-  ( Base ` c )
7 cnx 
 |-  ndx
8 7 4 cfv 
 |-  ( Base ` ndx )
9 3 cv 
 |-  x
10 chom 
 |-  Hom
11 5 10 cfv 
 |-  ( Hom ` c )
12 9 9 11 co 
 |-  ( x ( Hom ` c ) x )
13 8 12 cop 
 |-  <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >.
14 cplusg 
 |-  +g
15 7 14 cfv 
 |-  ( +g ` ndx )
16 9 9 cop 
 |-  <. x , x >.
17 cco 
 |-  comp
18 5 17 cfv 
 |-  ( comp ` c )
19 16 9 18 co 
 |-  ( <. x , x >. ( comp ` c ) x )
20 15 19 cop 
 |-  <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >.
21 13 20 cpr 
 |-  { <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. }
22 3 6 21 cmpt 
 |-  ( x e. ( Base ` c ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. } )
23 1 2 22 cmpt 
 |-  ( c e. Cat |-> ( x e. ( Base ` c ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. } ) )
24 0 23 wceq 
 |-  End = ( c e. Cat |-> ( x e. ( Base ` c ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. } ) )