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 clnbgr3stgrgrlic.n 𝑁 ∈ ℕ0
clnbgr3stgrgrlic.v 𝑉 = ( Vtx ‘ 𝐺 )
clnbgr3stgrgrlic.w 𝑊 = ( Vtx ‘ 𝐻 )
Assertion clnbgr3stgrgrlic ( ( ( 𝐺 ∈ USGraph ∧ 𝐻 ∈ USGraph ∧ 𝑉𝑊 ) ∧ ∀ 𝑥𝑉 ( 𝐺 ISubGr ( 𝐺 ClNeighbVtx 𝑥 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ∧ ∀ 𝑦𝑊 ( 𝐻 ISubGr ( 𝐻 ClNeighbVtx 𝑦 ) ) ≃𝑔𝑟 ( StarGr ‘ 𝑁 ) ) → 𝐺𝑙𝑔𝑟 𝐻 )

Proof

Step Hyp Ref Expression
1 clnbgr3stgrgrlic.n 𝑁 ∈ ℕ0
2 clnbgr3stgrgrlic.v 𝑉 = ( Vtx ‘ 𝐺 )
3 clnbgr3stgrgrlic.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 ‘ 𝑁 ) ) → 𝐺𝑙𝑔𝑟 𝐻 )