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

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