Theorem isomgrrel

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

	Ref	Expression
Assertion	isomgrrel	$$⊢\mathrm{Rel}\mathrm{IsomGr}$$

Proof

Step	Hyp	Ref	Expression
1		df-isomgr	$$⊢\mathrm{IsomGr}=\left\{⟨x,y⟩|\exists f\left(f:\mathrm{Vtx}\left(x\right)\underset{1-1\; onto}{⟶}\mathrm{Vtx}\left(y\right)\wedge \exists g\left(g:\mathrm{dom}\mathrm{iEdg}\left(x\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(y\right)\wedge \forall i\in \mathrm{dom}\mathrm{iEdg}\left(x\right)f\left[\mathrm{iEdg}\left(x\right)\left(i\right)\right]=\mathrm{iEdg}\left(y\right)\left(g\left(i\right)\right)\right)\right)\right\}$$
2	1	relopabiv	$$⊢\mathrm{Rel}\mathrm{IsomGr}$$