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 = ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgrlim ⊢ GraphLocIso
1 vg ⊢ 𝑔
2 cvv ⊢ V
3 vh ⊢ ℎ
4 vf ⊢ 𝑓
5 4 cv ⊢ 𝑓
6 cvtx ⊢ Vtx
7 1 cv ⊢ 𝑔
8 7 6 cfv ⊢ ( Vtx ‘ 𝑔 )
9 3 cv ⊢ ℎ
10 9 6 cfv ⊢ ( Vtx ‘ ℎ )
11 8 10 5 wf1o ⊢ 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ )
12 vv ⊢ 𝑣
13 cisubgr ⊢ ISubGr
14 cclnbgr ⊢ ClNeighbVtx
15 12 cv ⊢ 𝑣
16 7 15 14 co ⊢ ( 𝑔 ClNeighbVtx 𝑣 )
17 7 16 13 co ⊢ ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) )
18 cgric ⊢ ≃𝑔𝑟
19 15 5 cfv ⊢ ( 𝑓 ‘ 𝑣 )
20 9 19 14 co ⊢ ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) )
21 9 20 13 co ⊢ ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) )
22 17 21 18 wbr ⊢ ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) )
23 22 12 8 wral ⊢ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) )
24 11 23 wa ⊢ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) )
25 24 4 cab ⊢ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) }
26 1 3 2 2 25 cmpo ⊢ ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } )
27 0 26 wceq ⊢ GraphLocIso = ( 𝑔 ∈ V , ℎ ∈ V ↦ { 𝑓 ∣ ( 𝑓 : ( Vtx ‘ 𝑔 ) –1-1-onto→ ( Vtx ‘ ℎ ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝑔 ) ( 𝑔 ISubGr ( 𝑔 ClNeighbVtx 𝑣 ) ) ≃𝑔𝑟 ( ℎ ISubGr ( ℎ ClNeighbVtx ( 𝑓 ‘ 𝑣 ) ) ) ) } )