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

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 ∈ V , h ∈ V ⟼ f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgrlim class GraphLocIso
1 vg setvar g
2 cvv class V
3 vh setvar h
4 vf setvar f
5 4 cv setvar f
6 cvtx class Vtx
7 1 cv setvar g
8 7 6 cfv class Vtx ⁡ g
9 3 cv setvar h
10 9 6 cfv class Vtx ⁡ h
11 8 10 5 wf1o wff f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h
12 vv setvar v
13 cisubgr class ISubGr
14 cclnbgr class ClNeighbVtx
15 12 cv setvar v
16 7 15 14 co class g ClNeighbVtx v
17 7 16 13 co class g ISubGr g ClNeighbVtx v
18 cgric class ≃ 𝑔𝑟
19 15 5 cfv class f ⁡ v
20 9 19 14 co class h ClNeighbVtx f ⁡ v
21 9 20 13 co class h ISubGr h ClNeighbVtx f ⁡ v
22 17 21 18 wbr wff g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v
23 22 12 8 wral wff ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v
24 11 23 wa wff f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v
25 24 4 cab class f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v
26 1 3 2 2 25 cmpo class g ∈ V , h ∈ V ⟼ f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v
27 0 26 wceq wff GraphLocIso = g ∈ V , h ∈ V ⟼ f | f : Vtx ⁡ g ⟶ 1-1 onto Vtx ⁡ h ∧ ∀ v ∈ Vtx ⁡ g g ISubGr g ClNeighbVtx v ≃ 𝑔𝑟 h ISubGr h ClNeighbVtx f ⁡ v