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 ℕ_{0}$
	clnbgr3stgrgrlim.v	$⊢ V = Vtx (G)$
	clnbgr3stgrgrlim.w	$⊢ W = Vtx (H)$
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 ℕ_{0}$
2		clnbgr3stgrgrlim.v	$⊢ V = Vtx (G)$
3		clnbgr3stgrgrlim.w	$⊢ W = Vtx (H)$
4	2	fvexi	$⊢ V \in V$
5	3	fvexi	$⊢ W \in V$
6	4 5	pm3.2i	$⊢ (V \in V \land W \in V)$
7		breng	$⊢ (V \in V \land W \in V) \to (V \approx W \leftrightarrow \exists f f : V \underset{1-1 onto}{⟶} W)$
8	6 7	mp1i	$⊢ (G \in USGraph \land H \in USGraph) \to (V \approx W \leftrightarrow \exists f f : V \underset{1-1 onto}{⟶} W)$
9		usgruhgr	$⊢ H \in USGraph \to H \in UHGraph$
10	9	adantl	$⊢ (G \in USGraph \land H \in USGraph) \to H \in 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	$⊢ H ClNeighbVtx f (x) \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	$⊢ (H \in UHGraph \land H ClNeighbVtx f (x) \subseteq W) \to H ISubGr (H ClNeighbVtx f (x)) \in 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	$⊢ ((G \in USGraph \land H \in USGraph) \land f : V \underset{1-1 onto}{⟶} W \land x \in V) \to f : V ⟶ W$
18		simp3	$⊢ ((G \in USGraph \land H \in USGraph) \land f : V \underset{1-1 onto}{⟶} W \land x \in V) \to x \in V$
19	17 18	ffvelcdmd	$⊢ ((G \in USGraph \land H \in USGraph) \land f : V \underset{1-1 onto}{⟶} W \land x \in V) \to f (x) \in W$
20		oveq2	$⊢ y = f (x) \to H ClNeighbVtx y = H ClNeighbVtx f (x)$
21	20	oveq2d	$⊢ y = f (x) \to H ISubGr (H ClNeighbVtx y) = H ISubGr (H ClNeighbVtx f (x))$
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	$⊢ (G \in USGraph \land H \in USGraph) \to (G ≃_{𝑙𝑔𝑟} H \leftrightarrow \exists f (f : V \underset{1-1 onto}{⟶} W \land \forall x \in V (G ISubGr (G ClNeighbVtx x)) ≃_{𝑔𝑟} (H ISubGr (H ClNeighbVtx f (x)))))$
46	45	3adant3	$⊢ (G \in USGraph \land H \in USGraph \land V \approx W) \to (G ≃_{𝑙𝑔𝑟} H \leftrightarrow \exists f (f : V \underset{1-1 onto}{⟶} W \land \forall x \in V (G ISubGr (G ClNeighbVtx x)) ≃_{𝑔𝑟} (H ISubGr (H ClNeighbVtx f (x)))))$
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 \|-

Metamath Proof Explorer

Theorem clnbgr3stgrgrlic

Proof