Theorem efmndsgrp

Description: The monoid of endofunctions on a class A is a semigroup. (Contributed by AV, 28-Jan-2024)

	Ref	Expression
Hypothesis	efmndmgm.g	$$⊢G=\mathrm{EndoFMnd}\left(A\right)$$
Assertion	efmndsgrp	$$⊢G\in \mathrm{Smgrp}$$

Proof

Step	Hyp	Ref	Expression
1		efmndmgm.g	$$⊢G=\mathrm{EndoFMnd}\left(A\right)$$
2	1	efmndmgm	$$⊢G\in \mathrm{Mgm}$$
3		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
4		eqid	$$⊢{+}_G={+}_G$$
5	1 3 4	efmndcl	$$⊢\left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\to x{+}_{G}y\in {\mathrm{Base}}_G$$
6	1 3 4	efmndov	$$⊢\left(x\in {\mathrm{Base}}_G\wedge y\in {\mathrm{Base}}_G\right)\to x{+}_{G}y=x\circ y$$
7	5 6	symggrplem	$$⊢\left(f\in {\mathrm{Base}}_G\wedge g\in {\mathrm{Base}}_G\wedge h\in {\mathrm{Base}}_G\right)\to \left(f{+}_{G}g\right){+}_{G}h=f{+}_G\left(g{+}_{G}h\right)$$
8	7	rgen3	$$⊢\forall f\in {\mathrm{Base}}_G\forall g\in {\mathrm{Base}}_G\forall h\in {\mathrm{Base}}_G\left(f{+}_{G}g\right){+}_{G}h=f{+}_G\left(g{+}_{G}h\right)$$
9	3 4	issgrp	$$⊢G\in \mathrm{Smgrp}\leftrightarrow \left(G\in \mathrm{Mgm}\wedge \forall f\in {\mathrm{Base}}_G\forall g\in {\mathrm{Base}}_G\forall h\in {\mathrm{Base}}_G\left(f{+}_{G}g\right){+}_{G}h=f{+}_G\left(g{+}_{G}h\right)\right)$$
10	2 8 9	mpbir2an	$$⊢G\in \mathrm{Smgrp}$$