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\in {\mathbb{N}}_0$$
	clnbgr3stgrgrlim.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	clnbgr3stgrgrlim.w	$$⊢W=\mathrm{Vtx}\left(H\right)$$
Assertion	clnbgr3stgrgrlim	Could not format assertion : No typesetting found for |- ( ( ( 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 ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		clnbgr3stgrgrlim.n	$$⊢N\in {\mathbb{N}}_0$$
2		clnbgr3stgrgrlim.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
3		clnbgr3stgrgrlim.w	$$⊢W=\mathrm{Vtx}\left(H\right)$$
4		simp13	Could not format ( ( ( 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 ) : No typesetting found for |- ( ( ( 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 ) with typecode |-
5		usgruhgr	$$⊢H\in \mathrm{USGraph}\to H\in \mathrm{UHGraph}$$
6	5	3ad2ant2	$$⊢\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{USGraph}\wedge F:V\underset{1-1\; onto}{⟶}W\right)\to H\in \mathrm{UHGraph}$$
7	6	adantr	Could not format ( ( ( 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 ) : No typesetting found for |- ( ( ( 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 ) with typecode |-
8	3	clnbgrssvtx	$$⊢HClNeighbVtxF\left(x\right)\subseteq W$$
9	8	a1i	Could not format ( ( ( ( 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 ) : No typesetting found for |- ( ( ( ( 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 ) with typecode |-
10	3	isubgruhgr	$$⊢\left(H\in \mathrm{UHGraph}\wedge HClNeighbVtxF\left(x\right)\subseteq W\right)\to H\mathrm{ISubGr}\left(HClNeighbVtxF\left(x\right)\right)\in \mathrm{UHGraph}$$
11	7 9 10	syl2an2r	Could not format ( ( ( ( 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 ) : No typesetting found for |- ( ( ( ( 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 ) with typecode |-
12		f1of	$$⊢F:V\underset{1-1\; onto}{⟶}W\to F:V⟶W$$
13	12	3ad2ant3	$$⊢\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{USGraph}\wedge F:V\underset{1-1\; onto}{⟶}W\right)\to F:V⟶W$$
14	13	ffvelcdmda	$$⊢\left(\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{USGraph}\wedge F:V\underset{1-1\; onto}{⟶}W\right)\wedge x\in V\right)\to F\left(x\right)\in W$$
15		oveq2	$$⊢y=F\left(x\right)\to HClNeighbVtxy=HClNeighbVtxF\left(x\right)$$
16	15	oveq2d	$$⊢y=F\left(x\right)\to H\mathrm{ISubGr}\left(HClNeighbVtxy\right)=H\mathrm{ISubGr}\left(HClNeighbVtxF\left(x\right)\right)$$
17	16	breq1d	Could not format ( y = ( F ` x ) -> ( ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) <-> ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ~=gr ( StarGr ` N ) ) ) : No typesetting found for |- ( y = ( F ` x ) -> ( ( H ISubGr ( H ClNeighbVtx y ) ) ~=gr ( StarGr ` N ) <-> ( H ISubGr ( H ClNeighbVtx ( F ` x ) ) ) ~=gr ( StarGr ` N ) ) ) with typecode |-
18	17	rspcv	Could not format ( ( 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 ) ) ) : No typesetting found for |- ( ( 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 ) ) ) with typecode |-
19	14 18	syl	Could not format ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-
20	19	impancom	Could not format ( ( ( 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 ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) with typecode |-
21	20	imp	Could not format ( ( ( ( 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 ) ) : No typesetting found for |- ( ( ( ( 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 ) ) with typecode |-
22		gricsym	Could not format ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) with typecode |-
23	11 21 22	sylc	Could not format ( ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( ( 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 ) ) ) ) with typecode |-
24	23	anim1ci	Could not format ( ( ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( ( ( ( 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 ) ) ) ) ) with typecode |-
25		grictr	Could not format ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) with typecode |-
26	24 25	syl	Could not format ( ( ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( ( ( 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 ) ) ) ) with typecode |-
27	26	ex	Could not format ( ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( ( ( 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 ) ) ) ) ) with typecode |-
28	27	ralimdva	Could not format ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) ) with typecode |-
29	28	ex	Could not format ( ( 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 ) ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) ) with typecode |-
30	29	com23	Could not format ( ( 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 ) ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) ) with typecode |-
31	30	3imp	Could not format ( ( ( 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 ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) with typecode |-
32	2	fvexi	$$⊢V\in \mathrm{V}$$
33	32	a1i	$$⊢F:V\underset{1-1\; onto}{⟶}W\to V\in \mathrm{V}$$
34	12 33	fexd	$$⊢F:V\underset{1-1\; onto}{⟶}W\to F\in \mathrm{V}$$
35	34	3anim3i	$$⊢\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{USGraph}\wedge F:V\underset{1-1\; onto}{⟶}W\right)\to \left(G\in \mathrm{USGraph}\wedge H\in \mathrm{USGraph}\wedge F\in \mathrm{V}\right)$$
36	35	3ad2ant1	Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-
37	2 3	isgrlim	$$⊢\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{USGraph}\wedge F\in \mathrm{V}\right)\to \left(F\in \left(G\mathrm{GraphLocIso}H\right)\leftrightarrow \left(F:V\underset{1-1\; onto}{⟶}W\wedge \forall x\in V\left(G\mathrm{ISubGr}\left(GClNeighbVtxx\right)\right){\simeq }_{𝑔𝑟}\left(H\mathrm{ISubGr}\left(HClNeighbVtxF\left(x\right)\right)\right)\right)\right)$$
38	36 37	syl	Could not format ( ( ( 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 ) ) ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) ) ) with typecode |-
39	4 31 38	mpbir2and	Could not format ( ( ( 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 ) ) : No typesetting found for |- ( ( ( 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 ) ) with typecode |-