Theorem grlimdmrel

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

	Ref	Expression
Assertion	grlimdmrel	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{GraphLocIso}$$

Proof

Step	Hyp	Ref	Expression
1		df-grlim	$$⊢\mathrm{GraphLocIso}=\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 \forall v\in \mathrm{Vtx}\left(g\right)\left(g\mathrm{ISubGr}\left(gClNeighbVtxv\right)\right){\simeq }_{𝑔𝑟}\left(h\mathrm{ISubGr}\left(hClNeighbVtxf\left(v\right)\right)\right)\right)\right\}\right)$$
2	1	reldmmpo	$$⊢\mathrm{Rel}\mathrm{dom}\mathrm{GraphLocIso}$$