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	$$⊢\phi \to C\in \mathrm{Cat}$$
	bj-endval.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
Assertion	bj-endbase	$$⊢\phi \to {\mathrm{Base}}_{End\left(C\right)\left(X\right)}=X\mathrm{Hom}\left(C\right)X$$

Proof

Step	Hyp	Ref	Expression
1		bj-endval.c	$$⊢\phi \to C\in \mathrm{Cat}$$
2		bj-endval.x	$$⊢\phi \to X\in {\mathrm{Base}}_C$$
3		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
4		fvexd	$$⊢\phi \to End\left(C\right)\left(X\right)\in \mathrm{V}$$
5	3 4	strfvnd	$$⊢\phi \to {\mathrm{Base}}_{End\left(C\right)\left(X\right)}=End\left(C\right)\left(X\right)\left({\mathrm{Base}}_{\mathrm{ndx}}\right)$$
6	1 2	bj-endval	$$⊢\phi \to End\left(C\right)\left(X\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X\mathrm{Hom}\left(C\right)X⟩,⟨{+}_{\mathrm{ndx}},⟨X,X⟩\mathrm{comp}\left(C\right)X⟩\right\}$$
7	6	fveq1d	$$⊢\phi \to End\left(C\right)\left(X\right)\left({\mathrm{Base}}_{\mathrm{ndx}}\right)=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X\mathrm{Hom}\left(C\right)X⟩,⟨{+}_{\mathrm{ndx}},⟨X,X⟩\mathrm{comp}\left(C\right)X⟩\right\}\left({\mathrm{Base}}_{\mathrm{ndx}}\right)$$
8		basendxnplusgndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}$$
9		fvex	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$$
10		ovex	$$⊢X\mathrm{Hom}\left(C\right)X\in \mathrm{V}$$
11	9 10	fvpr1	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne {+}_{\mathrm{ndx}}\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X\mathrm{Hom}\left(C\right)X⟩,⟨{+}_{\mathrm{ndx}},⟨X,X⟩\mathrm{comp}\left(C\right)X⟩\right\}\left({\mathrm{Base}}_{\mathrm{ndx}}\right)=X\mathrm{Hom}\left(C\right)X$$
12	8 11	mp1i	$$⊢\phi \to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X\mathrm{Hom}\left(C\right)X⟩,⟨{+}_{\mathrm{ndx}},⟨X,X⟩\mathrm{comp}\left(C\right)X⟩\right\}\left({\mathrm{Base}}_{\mathrm{ndx}}\right)=X\mathrm{Hom}\left(C\right)X$$
13	5 7 12	3eqtrd	$$⊢\phi \to {\mathrm{Base}}_{End\left(C\right)\left(X\right)}=X\mathrm{Hom}\left(C\right)X$$