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	Could not format assertion : No typesetting found for |- ( ph -> ( ( End ` C ) ` X ) = { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ) with typecode |-

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	Could not format End = ( c e. Cat |-> ( x e. ( Base ` c ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. } ) ) : No typesetting found for |- End = ( c e. Cat |-> ( x e. ( Base ` c ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` c ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` c ) x ) >. } ) ) with typecode |-
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	Could not format ( ph -> ( End ` C ) = ( x e. ( Base ` C ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` C ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` C ) x ) >. } ) ) : No typesetting found for |- ( ph -> ( End ` C ) = ( x e. ( Base ` C ) |-> { <. ( Base ` ndx ) , ( x ( Hom ` C ) x ) >. , <. ( +g ` ndx ) , ( <. x , x >. ( comp ` C ) x ) >. } ) ) with typecode |-
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	Could not format ( ph -> ( ( End ` C ) ` X ) = { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ) : No typesetting found for |- ( ph -> ( ( End ` C ) ` X ) = { <. ( Base ` ndx ) , ( X ( Hom ` C ) X ) >. , <. ( +g ` ndx ) , ( <. X , X >. ( comp ` C ) X ) >. } ) with typecode |-