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	|- ~=lgr = ( `' GraphLocIso " ( _V \ 1o ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgrlic	|- ~=lgr
1		cgrlim	|- GraphLocIso
2	1	ccnv	|- `' GraphLocIso
3		cvv	|- _V
4		c1o	|- 1o
5	3 4	cdif	|- ( _V \ 1o )
6	2 5	cima	|- ( `' GraphLocIso " ( _V \ 1o ) )
7	0 6	wceq	|- ~=lgr = ( `' GraphLocIso " ( _V \ 1o ) )