This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brgrlic

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

		Ref	Expression
	Assertion	brgrlic	$⊢ R ≃_{𝑙𝑔𝑟} S \leftrightarrow R GraphLocIso S \neq \emptyset$

Step	Hyp	Ref	Expression
1		df-grlic	$⊢ ≃_{𝑙𝑔𝑟} = {GraphLocIso}^{-1} [V ∖ 1_{𝑜}]$
2		grlimfn	$⊢ GraphLocIso Fn (V \times V)$
3	1 2	brwitnlem	$⊢ R ≃_{𝑙𝑔𝑟} S \leftrightarrow R GraphLocIso S \neq \emptyset$