Metamath Proof Explorer


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 relopabi Rel IsomGr