Theorem efmndcl

Description: The group operation of the monoid of endofunctions on A is closed. (Contributed by AV, 27-Jan-2024)

	Ref	Expression
Hypotheses	efmndtset.g	No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
	efmndplusg.b	$$⊢B={\mathrm{Base}}_G$$
	efmndplusg.p	$$⊢\underset{\dot{}}{+}={+}_G$$
Assertion	efmndcl	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$

Proof

Step	Hyp	Ref	Expression
1		efmndtset.g	Could not format G = ( EndoFMnd ` A ) : No typesetting found for |- G = ( EndoFMnd ` A ) with typecode |-
2		efmndplusg.b	$$⊢B={\mathrm{Base}}_G$$
3		efmndplusg.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4	1 2 3	efmndov	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y=X\circ Y$$
5	1 2	efmndbasf	$$⊢X\in B\to X:A⟶A$$
6	1 2	efmndbasf	$$⊢Y\in B\to Y:A⟶A$$
7		fco	$$⊢\left(X:A⟶A\wedge Y:A⟶A\right)\to \left(X\circ Y\right):A⟶A$$
8	5 6 7	syl2an	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(X\circ Y\right):A⟶A$$
9		coexg	$$⊢\left(X\in B\wedge Y\in B\right)\to X\circ Y\in \mathrm{V}$$
10	1 2	elefmndbas2	$$⊢X\circ Y\in \mathrm{V}\to \left(X\circ Y\in B\leftrightarrow \left(X\circ Y\right):A⟶A\right)$$
11	9 10	syl	$$⊢\left(X\in B\wedge Y\in B\right)\to \left(X\circ Y\in B\leftrightarrow \left(X\circ Y\right):A⟶A\right)$$
12	8 11	mpbird	$$⊢\left(X\in B\wedge Y\in B\right)\to X\circ Y\in B$$
13	4 12	eqeltrd	$$⊢\left(X\in B\wedge Y\in B\right)\to X\underset{\dot{}}{+}Y\in B$$