Theorem brgrlic

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

	Ref	Expression
Assertion	brgrlic	$$⊢R{\simeq }_{𝑙𝑔𝑟}S\leftrightarrow R\mathrm{GraphLocIso}S\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-grlic	$$⊢{\simeq }_{𝑙𝑔𝑟}={\mathrm{GraphLocIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
2		grlimfn	$$⊢\mathrm{GraphLocIso}Fn\left(\mathrm{V}\times \mathrm{V}\right)$$
3	1 2	brwitnlem	$$⊢R{\simeq }_{𝑙𝑔𝑟}S\leftrightarrow R\mathrm{GraphLocIso}S\ne \varnothing$$