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	⊢ ≃𝑙𝑔𝑟 = ( ◡ GraphLocIso “ ( V ∖ 1o ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgrlic	⊢ ≃𝑙𝑔𝑟
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	⊢ ≃𝑙𝑔𝑟 = ( ◡ GraphLocIso “ ( V ∖ 1o ) )