Theorem brgrilci

Description: Prove that two graphs are locally isomorphic by an explicit local isomorphism. (Contributed by AV, 9-Jun-2025)

	Ref	Expression
Assertion	brgrilci	$$⊢F\in \left(R\mathrm{GraphLocIso}S\right)\to R{\simeq }_{𝑙𝑔𝑟}S$$

Proof

Step	Hyp	Ref	Expression
1		ne0i	$$⊢F\in \left(R\mathrm{GraphLocIso}S\right)\to R\mathrm{GraphLocIso}S\ne \varnothing$$
2		brgrlic	$$⊢R{\simeq }_{𝑙𝑔𝑟}S\leftrightarrow R\mathrm{GraphLocIso}S\ne \varnothing$$
3	1 2	sylibr	$$⊢F\in \left(R\mathrm{GraphLocIso}S\right)\to R{\simeq }_{𝑙𝑔𝑟}S$$