Metamath Proof Explorer

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 e. ( R GraphLocIso S ) -> R ~=lgr S )

Proof

Step Hyp Ref Expression
1 ne0i 
 |-  ( F e. ( R GraphLocIso S ) -> ( R GraphLocIso S ) =/= (/) )
2 brgrlic 
 |-  ( R ~=lgr S <-> ( R GraphLocIso S ) =/= (/) )
3 1 2 sylibr 
 |-  ( F e. ( R GraphLocIso S ) -> R ~=lgr S )