This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ ( 𝜑 → 𝐶 ∈ Cat )
bj-endval.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
Assertion bj-endmnd ( 𝜑 → ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ∈ Mnd )

Proof

Step Hyp Ref Expression
1 bj-endval.c ⊢ ( 𝜑 → 𝐶 ∈ Cat )
2 bj-endval.x ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝐶 ) )
3 1 2 bj-endbase ⊢ ( 𝜑 → ( Base ‘ ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ) = ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
4 3 eqcomd ⊢ ( 𝜑 → ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) = ( Base ‘ ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ) )
5 1 2 bj-endcomp ⊢ ( 𝜑 → ( +g ‘ ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ) = ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) )
6 5 eqcomd ⊢ ( 𝜑 → ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) = ( +g ‘ ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ) )
7 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
8 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
9 eqid ⊢ ( comp ‘ 𝐶 ) = ( comp ‘ 𝐶 )
10 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝐶 ∈ Cat )
11 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
12 simp3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
13 simp2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
14 7 8 9 10 11 11 11 12 13 catcocl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( 𝑥 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑦 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
15 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝐶 ∈ Cat )
16 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
17 simpr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) )
18 simp3 ⊢ ( ( 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑧 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
19 17 18 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑧 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
20 simp2 ⊢ ( ( 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
21 17 20 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
22 simp1 ⊢ ( ( 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
23 17 22 syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
24 7 8 9 15 16 16 16 19 21 16 23 catass ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑦 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ∧ 𝑧 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) ) → ( ( 𝑥 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑦 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑧 ) = ( 𝑥 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( 𝑦 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑧 ) ) )
25 eqid ⊢ ( Id ‘ 𝐶 ) = ( Id ‘ 𝐶 )
26 7 8 25 1 2 catidcl ⊢ ( 𝜑 → ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
27 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝐶 ∈ Cat )
28 2 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑋 ∈ ( Base ‘ 𝐶 ) )
29 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) → 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) )
30 7 8 25 27 28 9 28 29 catlid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) 𝑥 ) = 𝑥 )
31 7 8 25 27 28 9 28 29 catrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑋 ( Hom ‘ 𝐶 ) 𝑋 ) ) → ( 𝑥 ( ⟨ 𝑋 , 𝑋 ⟩ ( comp ‘ 𝐶 ) 𝑋 ) ( ( Id ‘ 𝐶 ) ‘ 𝑋 ) ) = 𝑥 )
32 4 6 14 24 26 30 31 ismndd ⊢ ( 𝜑 → ( ( End ‘ 𝐶 ) ‘ 𝑋 ) ∈ Mnd )