Theorem reldmghm

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

	Ref	Expression
Assertion	reldmghm	⊢ Rel dom GrpHom

Proof

Step	Hyp	Ref	Expression
1		df-ghm	⊢ GrpHom = ( 𝑠 ∈ Grp , 𝑡 ∈ Grp ↦ { 𝑔 ∣ [ ( Base ‘ 𝑠 ) / 𝑤 ] ( 𝑔 : 𝑤 ⟶ ( Base ‘ 𝑡 ) ∧ ∀ 𝑥 ∈ 𝑤 ∀ 𝑦 ∈ 𝑤 ( 𝑔 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑔 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑔 ‘ 𝑦 ) ) ) } )
2	1	reldmmpo	⊢ Rel dom GrpHom