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\in {\mathbb{N}}_0$$
	clnbgr3stgrgrlim.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	clnbgr3stgrgrlim.w	$$⊢W=\mathrm{Vtx}\left(H\right)$$
Assertion	clnbgr3stgrgrlic	Could not format assertion : No typesetting found for |- ( ( ( 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 ) 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	2	fvexi	$$⊢V\in \mathrm{V}$$
5	3	fvexi	$$⊢W\in \mathrm{V}$$
6	4 5	pm3.2i	$$⊢\left(V\in \mathrm{V}\wedge W\in \mathrm{V}\right)$$
7		breng	$$⊢\left(V\in \mathrm{V}\wedge W\in \mathrm{V}\right)\to \left(V\approx W\leftrightarrow \exists ff:V\underset{1-1\; onto}{⟶}W\right)$$
8	6 7	mp1i	$$⊢\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{USGraph}\right)\to \left(V\approx W\leftrightarrow \exists ff:V\underset{1-1\; onto}{⟶}W\right)$$
9		usgruhgr	$$⊢H\in \mathrm{USGraph}\to H\in \mathrm{UHGraph}$$
10	9	adantl	$$⊢\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{USGraph}\right)\to H\in \mathrm{UHGraph}$$
11	10	3ad2ant1	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 |-
12	3	clnbgrssvtx	$$⊢HClNeighbVtxf\left(x\right)\subseteq W$$
13	12	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 |-
14	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}$$
15	11 13 14	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 |-
16		f1of	$$⊢f:V\underset{1-1\; onto}{⟶}W\to f:V⟶W$$
17	16	3ad2ant2	$$⊢\left(\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{USGraph}\right)\wedge f:V\underset{1-1\; onto}{⟶}W\wedge x\in V\right)\to f:V⟶W$$
18		simp3	$$⊢\left(\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{USGraph}\right)\wedge f:V\underset{1-1\; onto}{⟶}W\wedge x\in V\right)\to x\in V$$
19	17 18	ffvelcdmd	$$⊢\left(\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{USGraph}\right)\wedge f:V\underset{1-1\; onto}{⟶}W\wedge x\in V\right)\to f\left(x\right)\in W$$
20		oveq2	$$⊢y=f\left(x\right)\to HClNeighbVtxy=HClNeighbVtxf\left(x\right)$$
21	20	oveq2d	$$⊢y=f\left(x\right)\to H\mathrm{ISubGr}\left(HClNeighbVtxy\right)=H\mathrm{ISubGr}\left(HClNeighbVtxf\left(x\right)\right)$$
22	21	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 |-
23	22	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 |-
24	19 23	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 |-
25	24	3exp	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 |-
26	25	com34	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 |-
27	26	3imp1	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 |-
28		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 |-
29	15 27 28	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 |-
30	29	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 |-
31		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 |-
32	30 31	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 |-
33	32	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 |-
34	33	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 |-
35	34	3exp	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 |-
36	35	com24	Could not format ( ( 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 ) ) ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) ) ) with typecode |-
37	36	imp32	Could not format ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) ) with typecode |-
38	37	ancld	Could not format ( ( ( 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 ) ) ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) ) ) with typecode |-
39	38	eximdv	Could not format ( ( ( 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 ) ) ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) ) ) with typecode |-
40	39	ex	Could not format ( ( 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 ) ) ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) ) ) with typecode |-
41	40	com23	Could not format ( ( 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 ) ) ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) ) ) with typecode |-
42	8 41	sylbid	Could not format ( ( 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 ) ) ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) ) ) with typecode |-
43	42	3impia	Could not format ( ( 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 ) ) ) ) ) ) : No typesetting found for |- ( ( 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 ) ) ) ) ) ) with typecode |-
44	43	3impib	Could not format ( ( ( 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 ) ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) ) with typecode |-
45	2 3	dfgrlic2	$$⊢\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{USGraph}\right)\to \left(G{\simeq }_{𝑙𝑔𝑟}H\leftrightarrow \exists f\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)$$
46	45	3adant3	$$⊢\left(G\in \mathrm{USGraph}\wedge H\in \mathrm{USGraph}\wedge V\approx W\right)\to \left(G{\simeq }_{𝑙𝑔𝑟}H\leftrightarrow \exists f\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)$$
47	46	3ad2ant1	Could not format ( ( ( 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 ) ) ) ) ) ) : No typesetting found for |- ( ( ( 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 ) ) ) ) ) ) with typecode |-
48	44 47	mpbird	Could not format ( ( ( 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 ) : No typesetting found for |- ( ( ( 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 ) with typecode |-