Definition df-grlic

Description: Two graphs are said to be locally isomorphic iff they are connected by at least one local isomorphism. (Contributed by AV, 27-Apr-2025)

	Ref	Expression
Assertion	df-grlic	$$⊢{\simeq }_{𝑙𝑔𝑟}={\mathrm{GraphLocIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgrlic	$$class{\simeq }_{𝑙𝑔𝑟}$$
1		cgrlim	$$class\mathrm{GraphLocIso}$$
2	1	ccnv	$$class{\mathrm{GraphLocIso}}^{-1}$$
3		cvv	$$class\mathrm{V}$$
4		c1o	$$class{1}_{𝑜}$$
5	3 4	cdif	$$class\left(\mathrm{V}\setminus 1_{𝑜}\right)$$
6	2 5	cima	$$class{\mathrm{GraphLocIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$
7	0 6	wceq	$$wff{\simeq }_{𝑙𝑔𝑟}={\mathrm{GraphLocIso}}^{-1}\left[\mathrm{V}\setminus 1_{𝑜}\right]$$