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

Metamath Proof Explorer

Theorem grimdmrel

Description: The domain of the graph isomorphism function is a relation. (Contributed by AV, 28-Apr-2025)

Ref Expression
Assertion grimdmrel ⊢ Rel ⁡ dom ⁡ GraphIso

Proof

Step Hyp Ref Expression
1 df-grim ⊢ GraphIso = g ∈ V , h ∈ V ⟼ f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∃ j [˙ iEdg ⁡ g / e]˙ [˙ iEdg ⁡ h / d]˙ j : dom ⁡ e ⟶ 1-1 onto dom ⁡ d ∧ ∀ i ∈ dom ⁡ e d ⁡ j ⁡ i = f e ⁡ i
2 1 reldmmpo ⊢ Rel ⁡ dom ⁡ GraphIso