Theorem bj-endval

Description: Value 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-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\}$$

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		df-bj-end	$$⊢End=\left(c\in \mathrm{Cat}⟼\left(x\in {\mathrm{Base}}_c⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(c\right)x⟩,⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(c\right)x⟩\right\}\right)\right)$$
4		fveq2	$$⊢c=C\to {\mathrm{Base}}_c={\mathrm{Base}}_C$$
5		fveq2	$$⊢c=C\to \mathrm{Hom}\left(c\right)=\mathrm{Hom}\left(C\right)$$
6	5	oveqd	$$⊢c=C\to x\mathrm{Hom}\left(c\right)x=x\mathrm{Hom}\left(C\right)x$$
7	6	opeq2d	$$⊢c=C\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(c\right)x⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(C\right)x⟩$$
8		fveq2	$$⊢c=C\to \mathrm{comp}\left(c\right)=\mathrm{comp}\left(C\right)$$
9	8	oveqd	$$⊢c=C\to ⟨x,x⟩\mathrm{comp}\left(c\right)x=⟨x,x⟩\mathrm{comp}\left(C\right)x$$
10	9	opeq2d	$$⊢c=C\to ⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(c\right)x⟩=⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(C\right)x⟩$$
11	7 10	preq12d	$$⊢c=C\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}},x\mathrm{Hom}\left(C\right)x⟩,⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(C\right)x⟩\right\}$$
12	4 11	mpteq12dv	$$⊢c=C\to \left(x\in {\mathrm{Base}}_c⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(c\right)x⟩,⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(c\right)x⟩\right\}\right)=\left(x\in {\mathrm{Base}}_C⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(C\right)x⟩,⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(C\right)x⟩\right\}\right)$$
13		fvex	$$⊢{\mathrm{Base}}_C\in \mathrm{V}$$
14	13	mptex	$$⊢\left(x\in {\mathrm{Base}}_C⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(C\right)x⟩,⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(C\right)x⟩\right\}\right)\in \mathrm{V}$$
15	14	a1i	$$⊢\phi \to \left(x\in {\mathrm{Base}}_C⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(C\right)x⟩,⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(C\right)x⟩\right\}\right)\in \mathrm{V}$$
16	3 12 1 15	fvmptd3	$$⊢\phi \to End\left(C\right)=\left(x\in {\mathrm{Base}}_C⟼\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(C\right)x⟩,⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(C\right)x⟩\right\}\right)$$
17		id	$$⊢x=X\to x=X$$
18	17 17	oveq12d	$$⊢x=X\to x\mathrm{Hom}\left(C\right)x=X\mathrm{Hom}\left(C\right)X$$
19	18	opeq2d	$$⊢x=X\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},x\mathrm{Hom}\left(C\right)x⟩=⟨{\mathrm{Base}}_{\mathrm{ndx}},X\mathrm{Hom}\left(C\right)X⟩$$
20	17 17	opeq12d	$$⊢x=X\to ⟨x,x⟩=⟨X,X⟩$$
21	20 17	oveq12d	$$⊢x=X\to ⟨x,x⟩\mathrm{comp}\left(C\right)x=⟨X,X⟩\mathrm{comp}\left(C\right)X$$
22	21	opeq2d	$$⊢x=X\to ⟨{+}_{\mathrm{ndx}},⟨x,x⟩\mathrm{comp}\left(C\right)x⟩=⟨{+}_{\mathrm{ndx}},⟨X,X⟩\mathrm{comp}\left(C\right)X⟩$$
23	19 22	preq12d	$$⊢x=X\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}},X\mathrm{Hom}\left(C\right)X⟩,⟨{+}_{\mathrm{ndx}},⟨X,X⟩\mathrm{comp}\left(C\right)X⟩\right\}$$
24	23	adantl	$$⊢\left(\phi \wedge x=X\right)\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}},X\mathrm{Hom}\left(C\right)X⟩,⟨{+}_{\mathrm{ndx}},⟨X,X⟩\mathrm{comp}\left(C\right)X⟩\right\}$$
25		prex	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},X\mathrm{Hom}\left(C\right)X⟩,⟨{+}_{\mathrm{ndx}},⟨X,X⟩\mathrm{comp}\left(C\right)X⟩\right\}\in \mathrm{V}$$
26	25	a1i	$$⊢\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\}\in \mathrm{V}$$
27	16 24 2 26	fvmptd	$$⊢\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\}$$