Metamath Proof Explorer

Theorem bj-endval

Description: Value of the monoid of endomorphisms on an object of a category. (Contributed by BJ, 5-Apr-2024)

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 ‘ 𝐶 ) 𝑋 ) ⟩ } )