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	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	bj-endval.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
Assertion	bj-endval	⊢ ( 𝜑 → ( ( End ‘ 𝐶 ) ‘ 𝑋 ) = { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } )

Proof

Step	Hyp	Ref	Expression
1		bj-endval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		bj-endval.x	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
3		df-bj-end	⊢ End = ( 𝑐 ∈ Cat ↦ ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) ⟩ } ) )
4		fveq2	⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
5		fveq2	⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
6	5	oveqd	⊢ ( 𝑐 = 𝐶 → ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) = ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) )
7	6	opeq2d	⊢ ( 𝑐 = 𝐶 → ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) ⟩ = ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ⟩ )
8		fveq2	⊢ ( 𝑐 = 𝐶 → ( comp ‘ 𝑐 ) = ( comp ‘ 𝐶 ) )
9	8	oveqd	⊢ ( 𝑐 = 𝐶 → ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) = ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) )
10	9	opeq2d	⊢ ( 𝑐 = 𝐶 → ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) ⟩ = ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ⟩ )
11	7 10	preq12d	⊢ ( 𝑐 = 𝐶 → { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ⟩ } )
12	4 11	mpteq12dv	⊢ ( 𝑐 = 𝐶 → ( 𝑥 ∈ ( Base ‘ 𝑐 ) ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝑐 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝑐 ) 𝑥 ) ⟩ } ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ⟩ } ) )
13		fvex	⊢ ( Base ‘ 𝐶 ) ∈ V
14	13	mptex	⊢ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ⟩ } ) ∈ V
15	14	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ⟩ } ) ∈ V )
16	3 12 1 15	fvmptd3	⊢ ( 𝜑 → ( End ‘ 𝐶 ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ⟩ } ) )
17		id	⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
18	17 17	oveq12d	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
19	18	opeq2d	⊢ ( 𝑥 = 𝑋 → ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ⟩ = ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ )
20	17 17	opeq12d	⊢ ( 𝑥 = 𝑋 → ⟨ 𝑥 , 𝑥 ⟩ = ⟨ 𝑋 , 𝑋 ⟩ )
21	20 17	oveq12d	⊢ ( 𝑥 = 𝑋 → ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) = ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) )
22	21	opeq2d	⊢ ( 𝑥 = 𝑋 → ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ⟩ = ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ )
23	19 22	preq12d	⊢ ( 𝑥 = 𝑋 → { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } )
24	23	adantl	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → { ⟨ ( Base ‘ ndx ) , ( 𝑥 ( Hom ‘ 𝐶 ) 𝑥 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑥 , 𝑥 ⟩ ( comp ‘ 𝐶 ) 𝑥 ) ⟩ } = { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } )
25		prex	⊢ { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } ∈ V
26	25	a1i	⊢ ( 𝜑 → { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } ∈ V )
27	16 24 2 26	fvmptd	⊢ ( 𝜑 → ( ( End ‘ 𝐶 ) ‘ 𝑋 ) = { ⟨ ( Base ‘ ndx ) , ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ⟩ , ⟨ ( +g ‘ ndx ) , ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ⟩ } )