Theorem grlicrel

Description: The "is locally isomorphic to" relation for graphs is a relation. (Contributed by AV, 9-Jun-2025)

	Ref	Expression
Assertion	grlicrel	$$⊢\mathrm{Rel}{\simeq }_{𝑙𝑔𝑟}$$

Proof

Step	Hyp	Ref	Expression
1		df-grlic	$$⊢{\simeq }_{𝑙𝑔𝑟}={\mathrm{GraphLocIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
2		cnvimass	$$⊢{\mathrm{GraphLocIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]\subseteq \mathrm{dom}\mathrm{GraphLocIso}$$
3		grlimfn	$$⊢\mathrm{GraphLocIso}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$
4	3	fndmi	$$⊢\mathrm{dom}\mathrm{GraphLocIso}=\mathrm{V}\times \mathrm{V}$$
5	2 4	sseqtri	$$⊢{\mathrm{GraphLocIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]\subseteq \mathrm{V}\times \mathrm{V}$$
6	1 5	eqsstri	$$⊢{\simeq }_{𝑙𝑔𝑟}\subseteq \mathrm{V}\times \mathrm{V}$$
7		relxp	$$⊢\mathrm{Rel}\left(\mathrm{V}\times \mathrm{V}\right)$$
8		relss	$$⊢{\simeq }_{𝑙𝑔𝑟}\subseteq \mathrm{V}\times \mathrm{V}\to \left(\mathrm{Rel}\left(\mathrm{V}\times \mathrm{V}\right)\to \mathrm{Rel}{\simeq }_{𝑙𝑔𝑟}\right)$$
9	6 7 8	mp2	$$⊢\mathrm{Rel}{\simeq }_{𝑙𝑔𝑟}$$