Metamath Proof Explorer

Definition df-grlim

Description: A local isomorphism of graphs is a bijection between the sets of vertices of two graphs that preserves local adjacency, i.e. the subgraph induced by the closed neighborhood of a vertex of the first graph and the subgraph induced by the closed neighborhood of the associated vertex of the second graph are isomorphic. See the following chat in mathoverflow: https://mathoverflow.net/questions/491133/locally-isomorphic-graphs . (Contributed by AV, 27-Apr-2025)

Ref Expression
Assertion df-grlim 
|- GraphLocIso = ( g e. _V , h e. _V |-> { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ A. v e. ( Vtx ` g ) ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgrlim 
 |-  GraphLocIso
1 vg 
 |-  g
2 cvv 
 |-  _V
3 vh 
 |-  h
4 vf 
 |-  f
5 4 cv 
 |-  f
6 cvtx 
 |-  Vtx
7 1 cv 
 |-  g
8 7 6 cfv 
 |-  ( Vtx ` g )
9 3 cv 
 |-  h
10 9 6 cfv 
 |-  ( Vtx ` h )
11 8 10 5 wf1o 
 |-  f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h )
12 vv 
 |-  v
13 cisubgr 
 |-  ISubGr
14 cclnbgr 
 |-  ClNeighbVtx
15 12 cv 
 |-  v
16 7 15 14 co 
 |-  ( g ClNeighbVtx v )
17 7 16 13 co 
 |-  ( g ISubGr ( g ClNeighbVtx v ) )
18 cgric 
 |-  ~=gr
19 15 5 cfv 
 |-  ( f ` v )
20 9 19 14 co 
 |-  ( h ClNeighbVtx ( f ` v ) )
21 9 20 13 co 
 |-  ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) )
22 17 21 18 wbr 
 |-  ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) )
23 22 12 8 wral 
 |-  A. v e. ( Vtx ` g ) ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) )
24 11 23 wa 
 |-  ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ A. v e. ( Vtx ` g ) ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) )
25 24 4 cab 
 |-  { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ A. v e. ( Vtx ` g ) ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) ) }
26 1 3 2 2 25 cmpo 
 |-  ( g e. _V , h e. _V |-> { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ A. v e. ( Vtx ` g ) ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) ) } )
27 0 26 wceq 
 |-  GraphLocIso = ( g e. _V , h e. _V |-> { f | ( f : ( Vtx ` g ) -1-1-onto-> ( Vtx ` h ) /\ A. v e. ( Vtx ` g ) ( g ISubGr ( g ClNeighbVtx v ) ) ~=gr ( h ISubGr ( h ClNeighbVtx ( f ` v ) ) ) ) } )