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 ℕ_{0}$
	clnbgr3stgrgrlim.v	$⊢ V = Vtx (G)$
	clnbgr3stgrgrlim.w	$⊢ W = Vtx (H)$
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 ℕ_{0}$
2		clnbgr3stgrgrlim.v	$⊢ V = Vtx (G)$
3		clnbgr3stgrgrlim.w	$⊢ W = Vtx (H)$
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 USGraph \to H \in UHGraph$
6	5	3ad2ant2	$⊢ (G \in USGraph \land H \in USGraph \land F : V \underset{1-1 onto}{⟶} W) \to H \in 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	$⊢ H ClNeighbVtx F (x) \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	$⊢ (H \in UHGraph \land H ClNeighbVtx F (x) \subseteq W) \to H ISubGr (H ClNeighbVtx F (x)) \in 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	$⊢ (G \in USGraph \land H \in USGraph \land F : V \underset{1-1 onto}{⟶} W) \to F : V ⟶ W$
14	13	ffvelcdmda	$⊢ ((G \in USGraph \land H \in USGraph \land F : V \underset{1-1 onto}{⟶} W) \land x \in V) \to F (x) \in W$
15		oveq2	$⊢ y = F (x) \to H ClNeighbVtx y = H ClNeighbVtx F (x)$
16	15	oveq2d	$⊢ y = F (x) \to H ISubGr (H ClNeighbVtx y) = H ISubGr (H ClNeighbVtx F (x))$
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 V$
33	32	a1i	$⊢ F : V \underset{1-1 onto}{⟶} W \to V \in V$
34	12 33	fexd	$⊢ F : V \underset{1-1 onto}{⟶} W \to F \in V$
35	34	3anim3i	$⊢ (G \in USGraph \land H \in USGraph \land F : V \underset{1-1 onto}{⟶} W) \to (G \in USGraph \land H \in USGraph \land F \in V)$
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	$⊢ (G \in USGraph \land H \in USGraph \land F \in V) \to (F \in (G GraphLocIso H) \leftrightarrow (F : V \underset{1-1 onto}{⟶} W \land \forall x \in V (G ISubGr (G ClNeighbVtx x)) ≃_{𝑔𝑟} (H ISubGr (H ClNeighbVtx F (x)))))$
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 \|-

Metamath Proof Explorer

Theorem clnbgr3stgrgrlim

Proof