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 = ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∃ 𝑗 [ ( iEdg ‘ 𝑔 ) / 𝑒 ] [ ( iEdg ‘ ℎ ) / 𝑑 ] ( 𝑗 : dom 𝑒 –1-1-onto→ dom 𝑑 ∧ ∀ 𝑖 ∈ dom 𝑒 ( 𝑑 ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝑓 “ ( 𝑒 ‘ 𝑖 ) ) ) ) } )
2	1	reldmmpo	⊢ Rel dom GraphIso