This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- N e. NN0
clnbgr3stgrgrlim.v 
|- V = ( Vtx ` G )
clnbgr3stgrgrlim.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 clnbgr3stgrgrlim.n 
 |-  N e. NN0
2 clnbgr3stgrgrlim.v 
 |-  V = ( Vtx ` G )
3 clnbgr3stgrgrlim.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 )