Definition df-grlim 47802

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.)

Assertion

Ref	Expression
df-grlim	⊢ GraphLocIso = (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∀𝑣 ∈ (Vtx‘𝑔)(𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣))))})

Distinct variable group:   𝑓,𝑔,ℎ,𝑣

Detailed syntax breakdown of Definition df-grlim

Step	Hyp	Ref	Expression
1		cgrlim 47800	. 2 class GraphLocIso
2		vg	. . 3 setvar 𝑔
3		vh	. . 3 setvar ℎ
4		cvv 3488	. . 3 class V
5	2	cv 1536	. . . . . . 7 class 𝑔
6		cvtx 29031	. . . . . . 7 class Vtx
7	5, 6	cfv 6573	. . . . . 6 class (Vtx‘𝑔)
8	3	cv 1536	. . . . . . 7 class ℎ
9	8, 6	cfv 6573	. . . . . 6 class (Vtx‘ℎ)
10		vf	. . . . . . 7 setvar 𝑓
11	10	cv 1536	. . . . . 6 class 𝑓
12	7, 9, 11	wf1o 6572	. . . . 5 wff 𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ)
13		vv	. . . . . . . . . 10 setvar 𝑣
14	13	cv 1536	. . . . . . . . 9 class 𝑣
15		cclnbgr 47692	. . . . . . . . 9 class ClNeighbVtx
16	5, 14, 15	co 7448	. . . . . . . 8 class (𝑔 ClNeighbVtx 𝑣)
17		cisubgr 47732	. . . . . . . 8 class ISubGr
18	5, 16, 17	co 7448	. . . . . . 7 class (𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣))
19	14, 11	cfv 6573	. . . . . . . . 9 class (𝑓‘𝑣)
20	8, 19, 15	co 7448	. . . . . . . 8 class (ℎ ClNeighbVtx (𝑓‘𝑣))
21	8, 20, 17	co 7448	. . . . . . 7 class (ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣)))
22		cgric 47746	. . . . . . 7 class ≃𝑔𝑟
23	18, 21, 22	wbr 5166	. . . . . 6 wff (𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣)))
24	23, 13, 7	wral 3067	. . . . 5 wff ∀𝑣 ∈ (Vtx‘𝑔)(𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣)))
25	12, 24	wa 395	. . . 4 wff (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∀𝑣 ∈ (Vtx‘𝑔)(𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣))))
26	25, 10	cab 2717	. . 3 class {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∀𝑣 ∈ (Vtx‘𝑔)(𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣))))}
27	2, 3, 4, 4, 26	cmpo 7450	. 2 class (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∀𝑣 ∈ (Vtx‘𝑔)(𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣))))})
28	1, 27	wceq 1537	1 wff GraphLocIso = (𝑔 ∈ V, ℎ ∈ V ↦ {𝑓 ∣ (𝑓:(Vtx‘𝑔)–1-1-onto→(Vtx‘ℎ) ∧ ∀𝑣 ∈ (Vtx‘𝑔)(𝑔 ISubGr (𝑔 ClNeighbVtx 𝑣)) ≃𝑔𝑟 (ℎ ISubGr (ℎ ClNeighbVtx (𝑓‘𝑣))))})

This definition is referenced by:  grlimfn  47803  grlimdmrel  47804  isgrlim  47806