Theorem grimdmrel

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

	Ref	Expression
Assertion	grimdmrel	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{GraphIso}$$

Proof

Step	Hyp	Ref	Expression
1		df-grim	$$⊢\mathrm{GraphIso}=\left(g\in \mathrm{V},h\in \mathrm{V}⟼\left\{f|\left(f:\mathrm{Vtx}\left(g\right)\underset{1-1\; onto}{⟶}\mathrm{Vtx}\left(h\right)\wedge \exists j\underset{\dot{}}{[}\mathrm{iEdg}\left(g\right)/e\underset{\dot{}}{]}\underset{\dot{}}{[}\mathrm{iEdg}\left(h\right)/d\underset{\dot{}}{]}\left(j:\mathrm{dom}e\underset{1-1\; onto}{⟶}\mathrm{dom}d\wedge \forall i\in \mathrm{dom}ed\left(j\left(i\right)\right)=f\left[e\left(i\right)\right]\right)\right)\right\}\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{GraphIso}$$