Theorem mhmrcl1

Description: Reverse closure of a monoid homomorphism. (Contributed by Mario Carneiro, 7-Mar-2015)

	Ref	Expression
Assertion	mhmrcl1	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to S\in \mathrm{Mnd}$$

Proof

Step	Hyp	Ref	Expression
1		df-mhm	$$⊢\mathrm{MndHom}=\left(s\in \mathrm{Mnd},t\in \mathrm{Mnd}⟼\left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\left(\forall x\in {\mathrm{Base}}_s\forall y\in {\mathrm{Base}}_{s}f\left(x{+}_{s}y\right)=f\left(x\right){+}_{t}f\left(y\right)\wedge f\left(0_s\right)=0_t\right)\right\}\right)$$
2	1	elmpocl1	$$⊢F\in \left(S\mathrm{MndHom}T\right)\to S\in \mathrm{Mnd}$$