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 
|- N e. NN0
clnbgr3stgrgrlim.v 
|- V = ( Vtx ` G )
clnbgr3stgrgrlim.w 
|- W = ( Vtx ` H )
Assertion clnbgr3stgrgrlim 
|- ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) -> F e. ( G GraphLocIso H ) )

Proof

Step Hyp Ref Expression
1 clnbgr3stgrgrlim.n 
 |-  N e. NN0
2 clnbgr3stgrgrlim.v 
 |-  V = ( Vtx ` G )
3 clnbgr3stgrgrlim.w 
 |-  W = ( Vtx ` H )
4 simp13 
 |-  ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) -> F : V -1-1-onto-> W )
5 usgruhgr 
 |-  ( H e. USGraph -> H e. UHGraph )
6 5 3ad2ant2 
 |-  ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) -> H e. UHGraph )
7 6 adantr 
 |-  ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) -> H e. UHGraph )
8 3 clnbgrssvtx 
 |-  ( H ClNeighbVtx ( F ` x ) ) C_ W
9 8 a1i 
 |-  ( ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) /\ x e. V ) -> ( H ClNeighbVtx ( F ` x ) ) C_ W )
10 3 isubgruhgr 
 |-  ( ( H e. UHGraph /\ ( H ClNeighbVtx ( F ` x ) ) C_ W ) -> ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) e. UHGraph )
11 7 9 10 syl2an2r 
 |-  ( ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) /\ x e. V ) -> ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) e. UHGraph )
12 f1of 
 |-  ( F : V -1-1-onto-> W -> F : V --> W )
13 12 3ad2ant3 
 |-  ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) -> F : V --> W )
14 13 ffvelcdmda 
 |-  ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ x e. V ) -> ( F ` x ) e. W )
15 oveq2 
 |-  ( y = ( F ` x ) -> ( H ClNeighbVtx y ) = ( H ClNeighbVtx ( F ` x ) ) )
16 15 oveq2d 
 |-  ( y = ( F ` x ) -> ( H ISubGr ( H ClNeighbVtx y ) ) = ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) )
17 16 breq1d 
 |-  ( y = ( F ` x ) -> ( ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) <-> ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ~=gr ( StarGr ` N ) ) )
18 17 rspcv 
 |-  ( ( F ` x ) e. W -> ( A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) -> ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ~=gr ( StarGr ` N ) ) )
19 14 18 syl 
 |-  ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ x e. V ) -> ( A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) -> ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ~=gr ( StarGr ` N ) ) )
20 19 impancom 
 |-  ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) -> ( x e. V -> ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ~=gr ( StarGr ` N ) ) )
21 20 imp 
 |-  ( ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) /\ x e. V ) -> ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ~=gr ( StarGr ` N ) )
22 gricsym 
 |-  ( ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) e. UHGraph -> ( ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ~=gr ( StarGr ` N ) -> ( StarGr ` N ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ) )
23 11 21 22 sylc 
 |-  ( ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) /\ x e. V ) -> ( StarGr ` N ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) )
24 23 anim1ci 
 |-  ( ( ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) /\ x e. V ) /\ ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) ) -> ( ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) /\ ( StarGr ` N ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ) )
25 grictr 
 |-  ( ( ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) /\ ( StarGr ` N ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ) -> ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) )
26 24 25 syl 
 |-  ( ( ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) /\ x e. V ) /\ ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) ) -> ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) )
27 26 ex 
 |-  ( ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) /\ x e. V ) -> ( ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) -> ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ) )
28 27 ralimdva 
 |-  ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) -> ( A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) -> A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ) )
29 28 ex 
 |-  ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) -> ( A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) -> ( A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) -> A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ) ) )
30 29 com23 
 |-  ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) -> ( A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) -> ( A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) -> A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ) ) )
31 30 3imp 
 |-  ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) -> A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) )
32 2 fvexi 
 |-  V e. _V
33 32 a1i 
 |-  ( F : V -1-1-onto-> W -> V e. _V )
34 12 33 fexd 
 |-  ( F : V -1-1-onto-> W -> F e. _V )
35 34 3anim3i 
 |-  ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) -> ( G e. USGraph /\ H e. USGraph /\ F e. _V ) )
36 35 3ad2ant1 
 |-  ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) -> ( G e. USGraph /\ H e. USGraph /\ F e. _V ) )
37 2 3 isgrlim 
 |-  ( ( G e. USGraph /\ H e. USGraph /\ F e. _V ) -> ( F e. ( G GraphLocIso H ) <-> ( F : V -1-1-onto-> W /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ) ) )
38 36 37 syl 
 |-  ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) -> ( F e. ( G GraphLocIso H ) <-> ( F : V -1-1-onto-> W /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ) ) )
39 4 31 38 mpbir2and 
 |-  ( ( ( G e. USGraph /\ H e. USGraph /\ F : V -1-1-onto-> W ) /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) -> F e. ( G GraphLocIso H ) )