Metamath Proof Explorer


Theorem bj-endbase

Description: Base set of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-endval.c φ C Cat
bj-endval.x φ X Base C
Assertion bj-endbase φ Base End C X = X Hom C X

Proof

Step Hyp Ref Expression
1 bj-endval.c φ C Cat
2 bj-endval.x φ X Base C
3 baseid Base = Slot Base ndx
4 fvexd φ End C X V
5 3 4 strfvnd φ Base End C X = End C X Base ndx
6 1 2 bj-endval φ End C X = Base ndx X Hom C X + ndx X X comp C X
7 6 fveq1d φ End C X Base ndx = Base ndx X Hom C X + ndx X X comp C X Base ndx
8 basendxnplusgndx Base ndx + ndx
9 fvex Base ndx V
10 ovex X Hom C X V
11 9 10 fvpr1 Base ndx + ndx Base ndx X Hom C X + ndx X X comp C X Base ndx = X Hom C X
12 8 11 mp1i φ Base ndx X Hom C X + ndx X X comp C X Base ndx = X Hom C X
13 5 7 12 3eqtrd φ Base End C X = X Hom C X