Metamath Proof Explorer

Theorem clnbgr3stgrgrlic

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 the two graphs are locally isomorphic. (Contributed by AV, 29-Sep-2025)

Ref Expression
Hypotheses clnbgr3stgrgrlim.n ⊢ 𝑁 ∈ ℕ0
clnbgr3stgrgrlim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
clnbgr3stgrgrlim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
Assertion clnbgr3stgrgrlic ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → 𝐺 ≃𝑙𝑔𝑟 𝐻 )

Proof

Step Hyp Ref Expression
1 clnbgr3stgrgrlim.n ⊢ 𝑁 ∈ ℕ0
2 clnbgr3stgrgrlim.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
3 clnbgr3stgrgrlim.w ⊢ 𝑊 = ( Vtx ‘ 𝐻 )
4 2 fvexi ⊢ 𝑉 ∈ V
5 3 fvexi ⊢ 𝑊 ∈ V
6 4 5 pm3.2i ⊢ ( 𝑉 ∈ V ∧ 𝑊 ∈ V )
7 breng ⊢ ( ( 𝑉 ∈ V ∧ 𝑊 ∈ V ) → ( 𝑉 ≈ 𝑊 ↔ ∃ 𝑓 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) )
8 6 7 mp1i ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) → ( 𝑉 ≈ 𝑊 ↔ ∃ 𝑓 𝑓 : 𝑉 –1-1-onto→ 𝑊 ) )
9 usgruhgr ⊢ ( 𝐻 ∈ USGraph → 𝐻 ∈ UHGraph )
10 9 adantl ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) → 𝐻 ∈ UHGraph )
11 10 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → 𝐻 ∈ UHGraph )
12 3 clnbgrssvtx ⊢ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ⊆ 𝑊
13 12 a1i ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ⊆ 𝑊 )
14 3 isubgruhgr ⊢ ( ( 𝐻 ∈ UHGraph ∧ ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ⊆ 𝑊 ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ∈ UHGraph )
15 11 13 14 syl2an2r ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ∈ UHGraph )
16 f1of ⊢ ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 → 𝑓 : 𝑉 ⟶ 𝑊 )
17 16 3ad2ant2 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑥 ∈ 𝑉 ) → 𝑓 : 𝑉 ⟶ 𝑊 )
18 simp3 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑥 ∈ 𝑉 ) → 𝑥 ∈ 𝑉 )
19 17 18 ffvelcdmd ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑥 ∈ 𝑉 ) → ( 𝑓 ‘ 𝑥 ) ∈ 𝑊 )
20 oveq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝐻 ClNeighbVtx 𝑦 ) = ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) )
21 20 oveq2d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) = ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) )
22 21 breq1d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑥 ) → ( ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ↔ ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) )
23 22 rspcv ⊢ ( ( 𝑓 ‘ 𝑥 ) ∈ 𝑊 → ( ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) )
24 19 23 syl ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ 𝑥 ∈ 𝑉 ) → ( ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) )
25 24 3exp ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) → ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 → ( 𝑥 ∈ 𝑉 → ( ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ) ) )
26 25 com34 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) → ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 → ( ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( 𝑥 ∈ 𝑉 → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ) ) )
27 26 3imp1 ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) )
28 gricsym ⊢ ( ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ∈ UHGraph → ( ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( StarGr ‘ 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) )
29 15 27 28 sylc ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( StarGr ‘ 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) )
30 29 anim1ci ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ( StarGr ‘ 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) )
31 grictr ⊢ ( ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ( StarGr ‘ 𝑁 ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) )
32 30 31 syl ⊢ ( ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) ∧ ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) )
33 32 ex ⊢ ( ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ∧ 𝑥 ∈ 𝑉 ) → ( ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) )
34 33 ralimdva ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) )
35 34 3exp ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) → ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 → ( ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) )
36 35 com24 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) → ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 → ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) )
37 36 imp32 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ ( ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ) → ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 → ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) )
38 37 ancld ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ ( ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ) → ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 → ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) ) )
39 38 eximdv ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) ∧ ( ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) ) → ( ∃ 𝑓 𝑓 : 𝑉 –1-1-onto→ 𝑊 → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) ) )
40 39 ex ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) → ( ( ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ( ∃ 𝑓 𝑓 : 𝑉 –1-1-onto→ 𝑊 → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) )
41 40 com23 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) → ( ∃ 𝑓 𝑓 : 𝑉 –1-1-onto→ 𝑊 → ( ( ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) )
42 8 41 sylbid ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) → ( 𝑉 ≈ 𝑊 → ( ( ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) ) ) )
43 42 3impia ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊 ) → ( ( ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) ) )
44 43 3impib ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) )
45 2 3 dfgrlic2 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ) → ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) ) )
46 45 3adant3 ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊 ) → ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) ) )
47 46 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → ( 𝐺 ≃𝑙𝑔𝑟 𝐻 ↔ ∃ 𝑓 ( 𝑓 : 𝑉 –1-1-onto→ 𝑊 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx ( 𝑓 ‘ 𝑥 ) ) ) ) ) )
48 44 47 mpbird ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉 ≈ 𝑊 ) ∧ ∀ 𝑥 ∈ 𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦 ∈ 𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → 𝐺 ≃𝑙𝑔𝑟 𝐻 )