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	No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
Assertion	efmndsgrp	Could not format assertion : No typesetting found for |- G e. Smgrp with typecode |-

Proof

Step	Hyp	Ref	Expression
1		efmndmgm.g	Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
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	Could not format ( G e. Smgrp <-> ( G e. Mgm /\ A. f e. ( Base ` G ) A. g e. ( Base ` G ) A. h e. ( Base ` G ) ( ( f ( +g ` G ) g ) ( +g ` G ) h ) = ( f ( +g ` G ) ( g ( +g ` G ) h ) ) ) ) : No typesetting found for |- ( G e. Smgrp <-> ( G e. Mgm /\ A. f e. ( Base ` G ) A. g e. ( Base ` G ) A. h e. ( Base ` G ) ( ( f ( +g ` G ) g ) ( +g ` G ) h ) = ( f ( +g ` G ) ( g ( +g ` G ) h ) ) ) ) with typecode |-
10	2 8 9	mpbir2an	Could not format G e. Smgrp : No typesetting found for |- G e. Smgrp with typecode |-