Metamath Proof Explorer

Theorem clnbgr3stgrgrlim

Description: If all (closed) neighborhoods of the vertices in two simple graphs with the same order induce a subgraph which is isomorphic to an N-star, then any bijection between the vertices is a local isomorphism between the two graphs. (Contributed by AV, 28-Dec-2025)

Ref Expression
Hypotheses clnbgr3stgrgrlim.n ⊢ 𝑁 ∈ ℕ0
clnbgr3stgrgrlim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
clnbgr3stgrgrlim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
Assertion clnbgr3stgrgrlim ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) )

Proof

Step Hyp Ref Expression
1 clnbgr3stgrgrlim.n ⊢ 𝑁 ∈ ℕ0
2 clnbgr3stgrgrlim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3 clnbgr3stgrgrlim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
4 simp13 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )
5 usgruhgr ⊢ ( 𝐻 ∈ USGraph → 𝐻 ∈ UHGraph )
6 5 3ad2ant2 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → 𝐻 ∈ UHGraph )
7 6 adantr ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → 𝐻 ∈ UHGraph )
8 3 clnbgrssvtx ⊢ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ⊆ 𝑊
9 8 a1i ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ⊆ 𝑊 )
10 3 isubgruhgr ⊢ ( ( 𝐻 ∈ UHGraph ∧ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ⊆ 𝑊 ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ∈ UHGraph )
11 7 9 10 syl2an2r ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ∈ UHGraph )
12 f1of ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 : 𝑉 ⟶ 𝑊 )
13 12 3ad2ant3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → 𝐹 : 𝑉 ⟶ 𝑊 )
14 13 ffvelcdmda ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑊 )
15 oveq2 ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝐻 ClNeighbVtx 𝑦 ) = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) )
16 15 oveq2d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) = ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) )
17 16 breq1d ⊢ ( 𝑦 = ( 𝐹 ‘ 𝑥 ) → ( ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ↔ ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) )
18 17 rspcv ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑊 → ( ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) )
19 14 18 syl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ 𝑥 ∈ 𝑉 ) → ( ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) )
20 19 impancom ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ( 𝑥 ∈ 𝑉 → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) )
21 20 imp ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) )
22 gricsym ⊢ ( ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ∈ UHGraph → ( ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( StarGr ‘ 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ) )
23 11 21 22 sylc ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( StarGr ‘ 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) )
24 23 anim1ci ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ( StarGr ‘ 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ) )
25 grictr ⊢ ( ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ( StarGr ‘ 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) )
26 24 25 syl ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) )
27 26 ex ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ) )
28 27 ralimdva ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ) )
29 28 ex ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
30 29 com23 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
31 30 3imp ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) )
32 2 fvexi ⊢ 𝑉 ∈ V
33 32 a1i ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝑉 ∈ V )
34 12 33 fexd ⊢ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 → 𝐹 ∈ V )
35 34 3anim3i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) → ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 ∈ V ) )
36 35 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 ∈ V ) )
37 2 3 isgrlim ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 ∈ V ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
38 36 37 syl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ( 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ↔ ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑥 ) ) ) ) ) )
39 4 31 38 mpbir2and ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝐹 : 𝑉 –1-1-onto→ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) )