bj-endmnd

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

	Ref	Expression
Hypotheses	bj-endval.c	$⊢ φ \to C \in Cat$
	bj-endval.x	$⊢ φ \to X \in {Base}_{C}$
Assertion	bj-endmnd	Could not format assertion : No typesetting found for \|- ( ph -> ( ( End ` C ) ` X ) e. Mnd ) with typecode \|-

Proof

Step	Hyp	Ref	Expression
1		bj-endval.c	$⊢ φ \to C \in Cat$
2		bj-endval.x	$⊢ φ \to X \in {Base}_{C}$
3	1 2	bj-endbase	Could not format ( ph -> ( Base ` ( ( End ` C ) ` X ) ) = ( X ( Hom ` C ) X ) ) : No typesetting found for \|- ( ph -> ( Base ` ( ( End ` C ) ` X ) ) = ( X ( Hom ` C ) X ) ) with typecode \|-
4	3	eqcomd	Could not format ( ph -> ( X ( Hom ` C ) X ) = ( Base ` ( ( End ` C ) ` X ) ) ) : No typesetting found for \|- ( ph -> ( X ( Hom ` C ) X ) = ( Base ` ( ( End ` C ) ` X ) ) ) with typecode \|-
5	1 2	bj-endcomp	Could not format ( ph -> ( +g ` ( ( End ` C ) ` X ) ) = ( <. X , X >. ( comp ` C ) X ) ) : No typesetting found for \|- ( ph -> ( +g ` ( ( End ` C ) ` X ) ) = ( <. X , X >. ( comp ` C ) X ) ) with typecode \|-
6	5	eqcomd	Could not format ( ph -> ( <. X , X >. ( comp ` C ) X ) = ( +g ` ( ( End ` C ) ` X ) ) ) : No typesetting found for \|- ( ph -> ( <. X , X >. ( comp ` C ) X ) = ( +g ` ( ( End ` C ) ` X ) ) ) with typecode \|-
7		eqid	$⊢ {Base}_{C} = {Base}_{C}$
8		eqid	$⊢ Hom (C) = Hom (C)$
9		eqid	$⊢ comp (C) = comp (C)$
10	1	3ad2ant1	$⊢ (φ \land x \in (X Hom (C) X) \land y \in (X Hom (C) X)) \to C \in Cat$
11	2	3ad2ant1	$⊢ (φ \land x \in (X Hom (C) X) \land y \in (X Hom (C) X)) \to X \in {Base}_{C}$
12		simp3	$⊢ (φ \land x \in (X Hom (C) X) \land y \in (X Hom (C) X)) \to y \in (X Hom (C) X)$
13		simp2	$⊢ (φ \land x \in (X Hom (C) X) \land y \in (X Hom (C) X)) \to x \in (X Hom (C) X)$
14	7 8 9 10 11 11 11 12 13	catcocl	$⊢ (φ \land x \in (X Hom (C) X) \land y \in (X Hom (C) X)) \to x (⟨X, X⟩ comp (C) X) y \in (X Hom (C) X)$
15	1	adantr	$⊢ (φ \land (x \in (X Hom (C) X) \land y \in (X Hom (C) X) \land z \in (X Hom (C) X))) \to C \in Cat$
16	2	adantr	$⊢ (φ \land (x \in (X Hom (C) X) \land y \in (X Hom (C) X) \land z \in (X Hom (C) X))) \to X \in {Base}_{C}$
17		simpr	$⊢ (φ \land (x \in (X Hom (C) X) \land y \in (X Hom (C) X) \land z \in (X Hom (C) X))) \to (x \in (X Hom (C) X) \land y \in (X Hom (C) X) \land z \in (X Hom (C) X))$
18		simp3	$⊢ (x \in (X Hom (C) X) \land y \in (X Hom (C) X) \land z \in (X Hom (C) X)) \to z \in (X Hom (C) X)$
19	17 18	syl	$⊢ (φ \land (x \in (X Hom (C) X) \land y \in (X Hom (C) X) \land z \in (X Hom (C) X))) \to z \in (X Hom (C) X)$
20		simp2	$⊢ (x \in (X Hom (C) X) \land y \in (X Hom (C) X) \land z \in (X Hom (C) X)) \to y \in (X Hom (C) X)$
21	17 20	syl	$⊢ (φ \land (x \in (X Hom (C) X) \land y \in (X Hom (C) X) \land z \in (X Hom (C) X))) \to y \in (X Hom (C) X)$
22		simp1	$⊢ (x \in (X Hom (C) X) \land y \in (X Hom (C) X) \land z \in (X Hom (C) X)) \to x \in (X Hom (C) X)$
23	17 22	syl	$⊢ (φ \land (x \in (X Hom (C) X) \land y \in (X Hom (C) X) \land z \in (X Hom (C) X))) \to x \in (X Hom (C) X)$
24	7 8 9 15 16 16 16 19 21 16 23	catass	$⊢ (φ \land (x \in (X Hom (C) X) \land y \in (X Hom (C) X) \land z \in (X Hom (C) X))) \to (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	$⊢ φ \to Id (C) (X) \in (X Hom (C) X)$
27	1	adantr	$⊢ (φ \land x \in (X Hom (C) X)) \to C \in Cat$
28	2	adantr	$⊢ (φ \land x \in (X Hom (C) X)) \to X \in {Base}_{C}$
29		simpr	$⊢ (φ \land x \in (X Hom (C) X)) \to x \in (X Hom (C) X)$
30	7 8 25 27 28 9 28 29	catlid	$⊢ (φ \land x \in (X Hom (C) X)) \to Id (C) (X) (⟨X, X⟩ comp (C) X) x = x$
31	7 8 25 27 28 9 28 29	catrid	$⊢ (φ \land x \in (X Hom (C) X)) \to x (⟨X, X⟩ comp (C) X) Id (C) (X) = x$
32	4 6 14 24 26 30 31	ismndd	Could not format ( ph -> ( ( End ` C ) ` X ) e. Mnd ) : No typesetting found for \|- ( ph -> ( ( End ` C ) ` X ) e. Mnd ) with typecode \|-

Metamath Proof Explorer

Theorem bj-endmnd

Proof