Theorem brgrlic

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

	Ref	Expression
Assertion	brgrlic	⊢ ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ↔ ( 𝑅 GraphLocIso 𝑆 ) ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-grlic	⊢ ≃𝑙𝑔𝑟 = ( ◡ GraphLocIso “ ( V ∖ 1o ) )
2		grlimfn	⊢ GraphLocIso Fn ( V × V )
3	1 2	brwitnlem	⊢ ( 𝑅 ≃𝑙𝑔𝑟 𝑆 ↔ ( 𝑅 GraphLocIso 𝑆 ) ≠ ∅ )