Theorem isomgrrel

Description: The isomorphy relation for graphs is a relation. (Contributed by AV, 11-Nov-2022)

	Ref	Expression
Assertion	isomgrrel	⊢ Rel IsomGr

Proof

Step	Hyp	Ref	Expression
1		df-isomgr	⊢ IsomGr = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑓 ( 𝑓 : ( Vtx ‘ 𝑥 ) –1-1-onto→ ( Vtx ‘ 𝑦 ) ∧ ∃ 𝑔 ( 𝑔 : dom ( iEdg ‘ 𝑥 ) –1-1-onto→ dom ( iEdg ‘ 𝑦 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝑥 ) ( 𝑓 “ ( ( iEdg ‘ 𝑥 ) ‘ 𝑖 ) ) = ( ( iEdg ‘ 𝑦 ) ‘ ( 𝑔 ‘ 𝑖 ) ) ) ) }
2	1	relopabiv	⊢ Rel IsomGr