Metamath Proof Explorer

Theorem bj-endmnd

Description: The monoid of endomorphisms on an object of a category is a monoid. (Contributed by BJ, 5-Apr-2024) (Proof modification is discouraged.)

Ref Expression
Hypotheses bj-endval.c 
|- ( ph -> C e. Cat )
bj-endval.x 
|- ( ph -> X e. ( Base ` C ) )
Assertion bj-endmnd 
|- ( ph -> ( ( End ` C ) ` X ) e. Mnd )

Proof

Step Hyp Ref Expression
1 bj-endval.c 
 |-  ( ph -> C e. Cat )
2 bj-endval.x 
 |-  ( ph -> X e. ( Base ` C ) )
3 1 2 bj-endbase 
 |-  ( ph -> ( Base ` ( ( End ` C ) ` X ) ) = ( X ( Hom ` C ) X ) )
4 3 eqcomd 
 |-  ( ph -> ( X ( Hom ` C ) X ) = ( Base ` ( ( End ` C ) ` X ) ) )
5 1 2 bj-endcomp 
 |-  ( ph -> ( +g ` ( ( End ` C ) ` X ) ) = ( <. X , X >. ( comp ` C ) X ) )
6 5 eqcomd 
 |-  ( ph -> ( <. X , X >. ( comp ` C ) X ) = ( +g ` ( ( End ` C ) ` X ) ) )
7 eqid 
 |-  ( Base ` C ) = ( Base ` C )
8 eqid 
 |-  ( Hom ` C ) = ( Hom ` C )
9 eqid 
 |-  ( comp ` C ) = ( comp ` C )
10 1 3ad2ant1 
 |-  ( ( ph /\ x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) ) -> C e. Cat )
11 2 3ad2ant1 
 |-  ( ( ph /\ x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) ) -> X e. ( Base ` C ) )
12 simp3 
 |-  ( ( ph /\ x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) ) -> y e. ( X ( Hom ` C ) X ) )
13 simp2 
 |-  ( ( ph /\ x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) ) -> x e. ( X ( Hom ` C ) X ) )
14 7 8 9 10 11 11 11 12 13 catcocl 
 |-  ( ( ph /\ x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) ) -> ( x ( <. X , X >. ( comp ` C ) X ) y ) e. ( X ( Hom ` C ) X ) )
15 1 adantr 
 |-  ( ( ph /\ ( x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) /\ z e. ( X ( Hom ` C ) X ) ) ) -> C e. Cat )
16 2 adantr 
 |-  ( ( ph /\ ( x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) /\ z e. ( X ( Hom ` C ) X ) ) ) -> X e. ( Base ` C ) )
17 simpr 
 |-  ( ( ph /\ ( x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) /\ z e. ( X ( Hom ` C ) X ) ) ) -> ( x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) /\ z e. ( X ( Hom ` C ) X ) ) )
18 simp3 
 |-  ( ( x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) /\ z e. ( X ( Hom ` C ) X ) ) -> z e. ( X ( Hom ` C ) X ) )
19 17 18 syl 
 |-  ( ( ph /\ ( x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) /\ z e. ( X ( Hom ` C ) X ) ) ) -> z e. ( X ( Hom ` C ) X ) )
20 simp2 
 |-  ( ( x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) /\ z e. ( X ( Hom ` C ) X ) ) -> y e. ( X ( Hom ` C ) X ) )
21 17 20 syl 
 |-  ( ( ph /\ ( x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) /\ z e. ( X ( Hom ` C ) X ) ) ) -> y e. ( X ( Hom ` C ) X ) )
22 simp1 
 |-  ( ( x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) /\ z e. ( X ( Hom ` C ) X ) ) -> x e. ( X ( Hom ` C ) X ) )
23 17 22 syl 
 |-  ( ( ph /\ ( x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) /\ z e. ( X ( Hom ` C ) X ) ) ) -> x e. ( X ( Hom ` C ) X ) )
24 7 8 9 15 16 16 16 19 21 16 23 catass 
 |-  ( ( ph /\ ( x e. ( X ( Hom ` C ) X ) /\ y e. ( X ( Hom ` C ) X ) /\ z e. ( X ( Hom ` C ) X ) ) ) -> ( ( x ( <. X , X >. ( comp ` C ) X ) y ) ( <. X , X >. ( comp ` C ) X ) z ) = ( x ( <. X , X >. ( comp ` C ) X ) ( y ( <. X , X >. ( comp ` C ) X ) z ) ) )
25 eqid 
 |-  ( Id ` C ) = ( Id ` C )
26 7 8 25 1 2 catidcl 
 |-  ( ph -> ( ( Id ` C ) ` X ) e. ( X ( Hom ` C ) X ) )
27 1 adantr 
 |-  ( ( ph /\ x e. ( X ( Hom ` C ) X ) ) -> C e. Cat )
28 2 adantr 
 |-  ( ( ph /\ x e. ( X ( Hom ` C ) X ) ) -> X e. ( Base ` C ) )
29 simpr 
 |-  ( ( ph /\ x e. ( X ( Hom ` C ) X ) ) -> x e. ( X ( Hom ` C ) X ) )
30 7 8 25 27 28 9 28 29 catlid 
 |-  ( ( ph /\ x e. ( X ( Hom ` C ) X ) ) -> ( ( ( Id ` C ) ` X ) ( <. X , X >. ( comp ` C ) X ) x ) = x )
31 7 8 25 27 28 9 28 29 catrid 
 |-  ( ( ph /\ x e. ( X ( Hom ` C ) X ) ) -> ( x ( <. X , X >. ( comp ` C ) X ) ( ( Id ` C ) ` X ) ) = x )
32 4 6 14 24 26 30 31 ismndd 
 |-  ( ph -> ( ( End ` C ) ` X ) e. Mnd )