This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = s ∈ Grp , t ∈ Grp ⟼ g | [˙Base s / w]˙ g : w ⟶ Base t ∧ ∀ x ∈ w ∀ y ∈ w g ⁡ x + s y = g ⁡ x + t g ⁡ y
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ GrpHom