Metamath Proof Explorer

Theorem dfgrlic2

Description: Alternate, explicit definition of the "is locally isomorphic to" relation for two graphs. (Contributed by AV, 9-Jun-2025)

Ref Expression
Hypotheses dfgrlic2.v 
|- V = ( Vtx ` G )
dfgrlic2.w 
|- W = ( Vtx ` H )
Assertion dfgrlic2 
|- ( ( G e. X /\ H e. Y ) -> ( G ~=lgr H <-> E. f ( f : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfgrlic2.v 
 |-  V = ( Vtx ` G )
2 dfgrlic2.w 
 |-  W = ( Vtx ` H )
3 brgrlic 
 |-  ( G ~=lgr H <-> ( G GraphLocIso H ) =/= (/) )
4 n0 
 |-  ( ( G GraphLocIso H ) =/= (/) <-> E. f f e. ( G GraphLocIso H ) )
5 3 4 bitri 
 |-  ( G ~=lgr H <-> E. f f e. ( G GraphLocIso H ) )
6 1 2 isgrlim 
 |-  ( ( G e. X /\ H e. Y /\ f e. _V ) -> ( f e. ( G GraphLocIso H ) <-> ( f : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) ) ) )
7 6 el3v3 
 |-  ( ( G e. X /\ H e. Y ) -> ( f e. ( G GraphLocIso H ) <-> ( f : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) ) ) )
8 7 exbidv 
 |-  ( ( G e. X /\ H e. Y ) -> ( E. f f e. ( G GraphLocIso H ) <-> E. f ( f : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) ) ) )
9 5 8 bitrid 
 |-  ( ( G e. X /\ H e. Y ) -> ( G ~=lgr H <-> E. f ( f : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) ) ) )