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 clnbgr3stgrgrlic.n N 0
clnbgr3stgrgrlic.v V = Vtx G
clnbgr3stgrgrlic.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 clnbgr3stgrgrlic.n N 0
2 clnbgr3stgrgrlic.v V = Vtx G
3 clnbgr3stgrgrlic.w W = Vtx H
4 2 fvexi V V
5 3 fvexi W V
6 4 5 pm3.2i V V W V
7 breng V V W V V W f f : V 1-1 onto W
8 6 7 mp1i G USGraph H USGraph V W f f : V 1-1 onto W
9 usgruhgr H USGraph H UHGraph
10 9 adantl G USGraph H USGraph H 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 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 UHGraph H ClNeighbVtx f x W H ISubGr H ClNeighbVtx f x 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 1-1 onto W f : V W
17 16 3ad2ant2 G USGraph H USGraph f : V 1-1 onto W x V f : V W
18 simp3 G USGraph H USGraph f : V 1-1 onto W x V x V
19 17 18 ffvelcdmd G USGraph H USGraph f : V 1-1 onto W x V f x 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 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 USGraph H USGraph G 𝑙𝑔𝑟 H f f : V 1-1 onto W x V G ISubGr G ClNeighbVtx x 𝑔𝑟 H ISubGr H ClNeighbVtx f x
46 45 3adant3 G USGraph H USGraph V W G 𝑙𝑔𝑟 H f f : V 1-1 onto W x 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 |-