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

Proof

Step Hyp Ref Expression
1 df-grlic 
 |-  ~=lgr = ( `' GraphLocIso " ( _V \ 1o ) )
2 grlimfn 
 |-  GraphLocIso Fn ( _V X. _V )
3 1 2 brwitnlem 
 |-  ( R ~=lgr S <-> ( R GraphLocIso S ) =/= (/) )