This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfgrlic3

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 )
dfgrlic3.i 
|- I = ( iEdg ` G )
dfgrlic3.j 
|- J = ( iEdg ` H )
dfgrlic3.n 
|- N = ( G ClNeighbVtx v )
dfgrlic3.m 
|- M = ( H ClNeighbVtx ( f ` v ) )
dfgrlic3.k 
|- K = { x e. dom I | ( I ` x ) C_ N }
dfgrlic3.l 
|- L = { x e. dom J | ( J ` x ) C_ M }
Assertion dfgrlic3 
|- ( ( G e. X /\ H e. Y ) -> ( G ~=lgr H <-> E. f ( f : V -1-1-onto-> W /\ A. v e. V E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfgrlic2.v 
 |-  V = ( Vtx ` G )
2 dfgrlic2.w 
 |-  W = ( Vtx ` H )
3 dfgrlic3.i 
 |-  I = ( iEdg ` G )
4 dfgrlic3.j 
 |-  J = ( iEdg ` H )
5 dfgrlic3.n 
 |-  N = ( G ClNeighbVtx v )
6 dfgrlic3.m 
 |-  M = ( H ClNeighbVtx ( f ` v ) )
7 dfgrlic3.k 
 |-  K = { x e. dom I | ( I ` x ) C_ N }
8 dfgrlic3.l 
 |-  L = { x e. dom J | ( J ` x ) C_ M }
9 brgrlic 
 |-  ( G ~=lgr H <-> ( G GraphLocIso H ) =/= (/) )
10 n0 
 |-  ( ( G GraphLocIso H ) =/= (/) <-> E. f f e. ( G GraphLocIso H ) )
11 9 10 bitri 
 |-  ( G ~=lgr H <-> E. f f e. ( G GraphLocIso H ) )
12 1 2 5 6 3 4 7 8 isgrlim2 
 |-  ( ( G e. X /\ H e. Y /\ f e. _V ) -> ( f e. ( G GraphLocIso H ) <-> ( f : V -1-1-onto-> W /\ A. v e. V E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )
13 12 el3v3 
 |-  ( ( G e. X /\ H e. Y ) -> ( f e. ( G GraphLocIso H ) <-> ( f : V -1-1-onto-> W /\ A. v e. V E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )
14 13 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 E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )
15 11 14 bitrid 
 |-  ( ( G e. X /\ H e. Y ) -> ( G ~=lgr H <-> E. f ( f : V -1-1-onto-> W /\ A. v e. V E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )