Theorem reldmghm

Description: Lemma for group homomorphisms. (Contributed by Stefan O'Rear, 31-Dec-2014)

	Ref	Expression
Assertion	reldmghm	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{GrpHom}$$

Proof

Step	Hyp	Ref	Expression
1		df-ghm	$$⊢\mathrm{GrpHom}=\left(s\in \mathrm{Grp},t\in \mathrm{Grp}⟼\left\{g|\underset{\dot{}}{[}{\mathrm{Base}}_s/w\underset{\dot{}}{]}\left(g:w⟶{\mathrm{Base}}_t\wedge \forall x\in w\forall y\in wg\left(x{+}_{s}y\right)=g\left(x\right){+}_{t}g\left(y\right)\right)\right\}\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{GrpHom}$$