Metamath Proof Explorer

Theorem endmndlem

Description: A diagonal hom-set in a category equipped with the restriction of the composition has a structure of monoid. See also df-mndtc for converting a monoid to a category. Lemma for bj-endmnd . (Contributed by Zhi Wang, 25-Sep-2024)

Ref Expression
Hypotheses endmndlem.b 
|- B = ( Base ` C )
endmndlem.h 
|- H = ( Hom ` C )
endmndlem.o 
|- .x. = ( comp ` C )
endmndlem.c 
|- ( ph -> C e. Cat )
endmndlem.x 
|- ( ph -> X e. B )
endmndlem.m 
|- ( ph -> ( X H X ) = ( Base ` M ) )
endmndlem.p 
|- ( ph -> ( <. X , X >. .x. X ) = ( +g ` M ) )
Assertion endmndlem 
|- ( ph -> M e. Mnd )

Proof

Step Hyp Ref Expression
1 endmndlem.b 
 |-  B = ( Base ` C )
2 endmndlem.h 
 |-  H = ( Hom ` C )
3 endmndlem.o 
 |-  .x. = ( comp ` C )
4 endmndlem.c 
 |-  ( ph -> C e. Cat )
5 endmndlem.x 
 |-  ( ph -> X e. B )
6 endmndlem.m 
 |-  ( ph -> ( X H X ) = ( Base ` M ) )
7 endmndlem.p 
 |-  ( ph -> ( <. X , X >. .x. X ) = ( +g ` M ) )
8 4 3ad2ant1 
 |-  ( ( ph /\ f e. ( X H X ) /\ g e. ( X H X ) ) -> C e. Cat )
9 5 3ad2ant1 
 |-  ( ( ph /\ f e. ( X H X ) /\ g e. ( X H X ) ) -> X e. B )
10 simp3 
 |-  ( ( ph /\ f e. ( X H X ) /\ g e. ( X H X ) ) -> g e. ( X H X ) )
11 simp2 
 |-  ( ( ph /\ f e. ( X H X ) /\ g e. ( X H X ) ) -> f e. ( X H X ) )
12 1 2 3 8 9 9 9 10 11 catcocl 
 |-  ( ( ph /\ f e. ( X H X ) /\ g e. ( X H X ) ) -> ( f ( <. X , X >. .x. X ) g ) e. ( X H X ) )
13 4 adantr 
 |-  ( ( ph /\ ( f e. ( X H X ) /\ g e. ( X H X ) /\ k e. ( X H X ) ) ) -> C e. Cat )
14 5 adantr 
 |-  ( ( ph /\ ( f e. ( X H X ) /\ g e. ( X H X ) /\ k e. ( X H X ) ) ) -> X e. B )
15 simpr3 
 |-  ( ( ph /\ ( f e. ( X H X ) /\ g e. ( X H X ) /\ k e. ( X H X ) ) ) -> k e. ( X H X ) )
16 simpr2 
 |-  ( ( ph /\ ( f e. ( X H X ) /\ g e. ( X H X ) /\ k e. ( X H X ) ) ) -> g e. ( X H X ) )
17 simpr1 
 |-  ( ( ph /\ ( f e. ( X H X ) /\ g e. ( X H X ) /\ k e. ( X H X ) ) ) -> f e. ( X H X ) )
18 1 2 3 13 14 14 14 15 16 14 17 catass 
 |-  ( ( ph /\ ( f e. ( X H X ) /\ g e. ( X H X ) /\ k e. ( X H X ) ) ) -> ( ( f ( <. X , X >. .x. X ) g ) ( <. X , X >. .x. X ) k ) = ( f ( <. X , X >. .x. X ) ( g ( <. X , X >. .x. X ) k ) ) )
19 eqid 
 |-  ( Id ` C ) = ( Id ` C )
20 1 2 19 4 5 catidcl 
 |-  ( ph -> ( ( Id ` C ) ` X ) e. ( X H X ) )
21 4 adantr 
 |-  ( ( ph /\ f e. ( X H X ) ) -> C e. Cat )
22 5 adantr 
 |-  ( ( ph /\ f e. ( X H X ) ) -> X e. B )
23 simpr 
 |-  ( ( ph /\ f e. ( X H X ) ) -> f e. ( X H X ) )
24 1 2 19 21 22 3 22 23 catlid 
 |-  ( ( ph /\ f e. ( X H X ) ) -> ( ( ( Id ` C ) ` X ) ( <. X , X >. .x. X ) f ) = f )
25 1 2 19 21 22 3 22 23 catrid 
 |-  ( ( ph /\ f e. ( X H X ) ) -> ( f ( <. X , X >. .x. X ) ( ( Id ` C ) ` X ) ) = f )
26 6 7 12 18 20 24 25 ismndd 
 |-  ( ph -> M e. Mnd )