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
|- N e. NN0
clnbgr3stgrgrlic.v
|- V = ( Vtx ` G )
clnbgr3stgrgrlic.w
|- W = ( Vtx ` H )
Assertion clnbgr3stgrgrlic
|- ( ( ( G e. USGraph /\ H e. USGraph /\ V ~~ 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 ~=lgr H )

Proof

Step Hyp Ref Expression
1 clnbgr3stgrgrlic.n
 |-  N e. NN0
2 clnbgr3stgrgrlic.v
 |-  V = ( Vtx ` G )
3 clnbgr3stgrgrlic.w
 |-  W = ( Vtx ` H )
4 2 fvexi
 |-  V e. _V
5 3 fvexi
 |-  W e. _V
6 4 5 pm3.2i
 |-  ( V e. _V /\ W e. _V )
7 breng
 |-  ( ( V e. _V /\ W e. _V ) -> ( V ~~ W <-> E. f f : V -1-1-onto-> W ) )
8 6 7 mp1i
 |-  ( ( G e. USGraph /\ H e. USGraph ) -> ( V ~~ W <-> E. f f : V -1-1-onto-> W ) )
9 usgruhgr
 |-  ( H e. USGraph -> H e. UHGraph )
10 9 adantl
 |-  ( ( G e. USGraph /\ H e. USGraph ) -> H e. UHGraph )
11 10 3ad2ant1
 |-  ( ( ( 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 )
12 3 clnbgrssvtx
 |-  ( H ClNeighbVtx ( f ` x ) ) C_ W
13 12 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 )
14 3 isubgruhgr
 |-  ( ( H e. UHGraph /\ ( H ClNeighbVtx ( f ` x ) ) C_ W ) -> ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) e. UHGraph )
15 11 13 14 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 )
16 f1of
 |-  ( f : V -1-1-onto-> W -> f : V --> W )
17 16 3ad2ant2
 |-  ( ( ( G e. USGraph /\ H e. USGraph ) /\ f : V -1-1-onto-> W /\ x e. V ) -> f : V --> W )
18 simp3
 |-  ( ( ( G e. USGraph /\ H e. USGraph ) /\ f : V -1-1-onto-> W /\ x e. V ) -> x e. V )
19 17 18 ffvelcdmd
 |-  ( ( ( G e. USGraph /\ H e. USGraph ) /\ f : V -1-1-onto-> W /\ x e. V ) -> ( f ` x ) e. W )
20 oveq2
 |-  ( y = ( f ` x ) -> ( H ClNeighbVtx y ) = ( H ClNeighbVtx ( f ` x ) ) )
21 20 oveq2d
 |-  ( y = ( f ` x ) -> ( H ISubGr ( H ClNeighbVtx y ) ) = ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) )
22 21 breq1d
 |-  ( y = ( f ` x ) -> ( ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) <-> ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) ~=gr ( StarGr ` N ) ) )
23 22 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 ) ) )
24 19 23 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 ) ) )
25 24 3exp
 |-  ( ( 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 ) ) ) ) )
26 25 com34
 |-  ( ( 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 ) ) ) ) )
27 26 3imp1
 |-  ( ( ( ( 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 ) )
28 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 ) ) ) ) )
29 15 27 28 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 ) ) ) )
30 29 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 ) ) ) ) )
31 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 ) ) ) )
32 30 31 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 ) ) ) )
33 32 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 ) ) ) ) )
34 33 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 ) ) ) ) )
35 34 3exp
 |-  ( ( 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 ) ) ) ) ) ) )
36 35 com24
 |-  ( ( G e. USGraph /\ H e. USGraph ) -> ( 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 -> A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) ) ) ) )
37 36 imp32
 |-  ( ( ( G e. USGraph /\ H e. USGraph ) /\ ( 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 -> A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) ) )
38 37 ancld
 |-  ( ( ( G e. USGraph /\ H e. USGraph ) /\ ( 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 -> ( f : V -1-1-onto-> W /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) ) ) )
39 38 eximdv
 |-  ( ( ( G e. USGraph /\ H e. USGraph ) /\ ( A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) ) -> ( E. f f : V -1-1-onto-> W -> E. f ( f : V -1-1-onto-> W /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) ) ) )
40 39 ex
 |-  ( ( G e. USGraph /\ H e. USGraph ) -> ( ( A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( StarGr ` N ) /\ A. y e. W ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) ) -> ( E. f f : V -1-1-onto-> W -> E. f ( f : V -1-1-onto-> W /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) ) ) ) )
41 40 com23
 |-  ( ( G e. USGraph /\ H e. USGraph ) -> ( E. f 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 ) ) -> E. f ( f : V -1-1-onto-> W /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) ) ) ) )
42 8 41 sylbid
 |-  ( ( G e. USGraph /\ H e. USGraph ) -> ( V ~~ 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 ) ) -> E. f ( f : V -1-1-onto-> W /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) ) ) ) )
43 42 3impia
 |-  ( ( G e. USGraph /\ H e. USGraph /\ V ~~ 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 ) ) -> E. f ( f : V -1-1-onto-> W /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) ) ) )
44 43 3impib
 |-  ( ( ( G e. USGraph /\ H e. USGraph /\ V ~~ 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 ) ) -> E. f ( f : V -1-1-onto-> W /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) ) )
45 2 3 dfgrlic2
 |-  ( ( G e. USGraph /\ H e. USGraph ) -> ( G ~=lgr H <-> E. f ( f : V -1-1-onto-> W /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) ) ) )
46 45 3adant3
 |-  ( ( G e. USGraph /\ H e. USGraph /\ V ~~ W ) -> ( G ~=lgr H <-> E. f ( f : V -1-1-onto-> W /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) ) ) )
47 46 3ad2ant1
 |-  ( ( ( G e. USGraph /\ H e. USGraph /\ V ~~ 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 ~=lgr H <-> E. f ( f : V -1-1-onto-> W /\ A. x e. V ( G ISubGr ( G ClNeighbVtx x ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` x ) ) ) ) ) )
48 44 47 mpbird
 |-  ( ( ( G e. USGraph /\ H e. USGraph /\ V ~~ 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 ~=lgr H )