Metamath Proof Explorer

Theorem grlimedgclnbgr

Description: For two locally isomorphic graphs G and H and a vertex A of G there are two bijections f and g mapping the closed neighborhood N of A onto the closed neighborhood M of ( FA ) and the edges between the vertices in N onto the edges between the vertices in M , so that the mapped vertices of an edge E containing the vertex A is an edge between the vertices in M . (Contributed by AV, 25-Dec-2025)

Ref Expression
Hypotheses clnbgrvtxedg.n 
|- N = ( G ClNeighbVtx A )
clnbgrvtxedg.i 
|- I = ( Edg ` G )
clnbgrvtxedg.k 
|- K = { x e. I | x C_ N }
grlimedgclnbgr.m 
|- M = ( H ClNeighbVtx ( F ` A ) )
grlimedgclnbgr.j 
|- J = ( Edg ` H )
grlimedgclnbgr.l 
|- L = { x e. J | x C_ M }
Assertion grlimedgclnbgr 
|- ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> E. f E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ ( f " E ) = ( g ` E ) ) )

Proof

Step Hyp Ref Expression
1 clnbgrvtxedg.n 
 |-  N = ( G ClNeighbVtx A )
2 clnbgrvtxedg.i 
 |-  I = ( Edg ` G )
3 clnbgrvtxedg.k 
 |-  K = { x e. I | x C_ N }
4 grlimedgclnbgr.m 
 |-  M = ( H ClNeighbVtx ( F ` A ) )
5 grlimedgclnbgr.j 
 |-  J = ( Edg ` H )
6 grlimedgclnbgr.l 
 |-  L = { x e. J | x C_ M }
7 simp1l 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> G e. USPGraph )
8 simp1r 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> H e. USPGraph )
9 simp2 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> F e. ( G GraphLocIso H ) )
10 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
11 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
12 eqid 
 |-  ( G ClNeighbVtx v ) = ( G ClNeighbVtx v )
13 eqid 
 |-  ( H ClNeighbVtx ( F ` v ) ) = ( H ClNeighbVtx ( F ` v ) )
14 sseq1 
 |-  ( x = y -> ( x C_ ( G ClNeighbVtx v ) <-> y C_ ( G ClNeighbVtx v ) ) )
15 14 cbvrabv 
 |-  { x e. I | x C_ ( G ClNeighbVtx v ) } = { y e. I | y C_ ( G ClNeighbVtx v ) }
16 sseq1 
 |-  ( x = y -> ( x C_ ( H ClNeighbVtx ( F ` v ) ) <-> y C_ ( H ClNeighbVtx ( F ` v ) ) ) )
17 16 cbvrabv 
 |-  { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } = { y e. J | y C_ ( H ClNeighbVtx ( F ` v ) ) }
18 10 11 12 13 2 5 15 17 usgrlimprop 
 |-  ( ( G e. USPGraph /\ H e. USPGraph /\ F e. ( G GraphLocIso H ) ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ A. v e. ( Vtx ` G ) E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx v ) } ( f " e ) = ( g ` e ) ) ) ) )
19 7 8 9 18 syl3anc 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ A. v e. ( Vtx ` G ) E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx v ) } ( f " e ) = ( g ` e ) ) ) ) )
20 uspgruhgr 
 |-  ( G e. USPGraph -> G e. UHGraph )
21 20 adantr 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> G e. UHGraph )
22 21 3ad2ant1 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> G e. UHGraph )
23 2 eleq2i 
 |-  ( E e. I <-> E e. ( Edg ` G ) )
24 23 birani 
 |-  ( ( E e. I /\ A e. E ) -> E e. ( Edg ` G ) )
25 24 3ad2ant3 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> E e. ( Edg ` G ) )
26 simp3r 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> A e. E )
27 uhgredgrnv 
 |-  ( ( G e. UHGraph /\ E e. ( Edg ` G ) /\ A e. E ) -> A e. ( Vtx ` G ) )
28 22 25 26 27 syl3anc 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> A e. ( Vtx ` G ) )
29 eqidd 
 |-  ( v = A -> f = f )
30 oveq2 
 |-  ( v = A -> ( G ClNeighbVtx v ) = ( G ClNeighbVtx A ) )
31 fveq2 
 |-  ( v = A -> ( F ` v ) = ( F ` A ) )
32 31 oveq2d 
 |-  ( v = A -> ( H ClNeighbVtx ( F ` v ) ) = ( H ClNeighbVtx ( F ` A ) ) )
33 29 30 32 f1oeq123d 
 |-  ( v = A -> ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) <-> f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) )
34 eqidd 
 |-  ( v = A -> g = g )
35 30 sseq2d 
 |-  ( v = A -> ( x C_ ( G ClNeighbVtx v ) <-> x C_ ( G ClNeighbVtx A ) ) )
36 35 rabbidv 
 |-  ( v = A -> { x e. I | x C_ ( G ClNeighbVtx v ) } = { x e. I | x C_ ( G ClNeighbVtx A ) } )
37 32 sseq2d 
 |-  ( v = A -> ( x C_ ( H ClNeighbVtx ( F ` v ) ) <-> x C_ ( H ClNeighbVtx ( F ` A ) ) ) )
38 37 rabbidv 
 |-  ( v = A -> { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } = { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } )
39 34 36 38 f1oeq123d 
 |-  ( v = A -> ( g : { x e. I | x C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } <-> g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) )
40 36 raleqdv 
 |-  ( v = A -> ( A. e e. { x e. I | x C_ ( G ClNeighbVtx v ) } ( f " e ) = ( g ` e ) <-> A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) )
41 39 40 anbi12d 
 |-  ( v = A -> ( ( g : { x e. I | x C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx v ) } ( f " e ) = ( g ` e ) ) <-> ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) ) )
42 41 exbidv 
 |-  ( v = A -> ( E. g ( g : { x e. I | x C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx v ) } ( f " e ) = ( g ` e ) ) <-> E. g ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) ) )
43 33 42 anbi12d 
 |-  ( v = A -> ( ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx v ) } ( f " e ) = ( g ` e ) ) ) <-> ( f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) ) ) )
44 43 exbidv 
 |-  ( v = A -> ( E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx v ) } ( f " e ) = ( g ` e ) ) ) <-> E. f ( f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) ) ) )
45 44 rspcv 
 |-  ( A e. ( Vtx ` G ) -> ( A. v e. ( Vtx ` G ) E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx v ) } ( f " e ) = ( g ` e ) ) ) -> E. f ( f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) ) ) )
46 28 45 syl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> ( A. v e. ( Vtx ` G ) E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx v ) } ( f " e ) = ( g ` e ) ) ) -> E. f ( f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) ) ) )
47 eqid 
 |-  f = f
48 id 
 |-  ( f = f -> f = f )
49 1 a1i 
 |-  ( f = f -> N = ( G ClNeighbVtx A ) )
50 4 a1i 
 |-  ( f = f -> M = ( H ClNeighbVtx ( F ` A ) ) )
51 48 49 50 f1oeq123d 
 |-  ( f = f -> ( f : N -1-1-onto-> M <-> f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) )
52 47 51 ax-mp 
 |-  ( f : N -1-1-onto-> M <-> f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) )
53 52 biimpri 
 |-  ( f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) -> f : N -1-1-onto-> M )
54 53 adantl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> f : N -1-1-onto-> M )
55 54 adantr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) /\ ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) ) -> f : N -1-1-onto-> M )
56 eqid 
 |-  g = g
57 id 
 |-  ( g = g -> g = g )
58 1 sseq2i 
 |-  ( x C_ N <-> x C_ ( G ClNeighbVtx A ) )
59 3 58 rabbieq 
 |-  K = { x e. I | x C_ ( G ClNeighbVtx A ) }
60 59 a1i 
 |-  ( g = g -> K = { x e. I | x C_ ( G ClNeighbVtx A ) } )
61 4 sseq2i 
 |-  ( x C_ M <-> x C_ ( H ClNeighbVtx ( F ` A ) ) )
62 6 61 rabbieq 
 |-  L = { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) }
63 62 a1i 
 |-  ( g = g -> L = { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } )
64 57 60 63 f1oeq123d 
 |-  ( g = g -> ( g : K -1-1-onto-> L <-> g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } ) )
65 56 64 ax-mp 
 |-  ( g : K -1-1-onto-> L <-> g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } )
66 65 biimpri 
 |-  ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } -> g : K -1-1-onto-> L )
67 66 adantr 
 |-  ( ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) -> g : K -1-1-onto-> L )
68 67 adantl 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) /\ ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) ) -> g : K -1-1-onto-> L )
69 simp3l 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> E e. I )
70 eqid 
 |-  ( G ClNeighbVtx A ) = ( G ClNeighbVtx A )
71 eqid 
 |-  { x e. I | x C_ ( G ClNeighbVtx A ) } = { x e. I | x C_ ( G ClNeighbVtx A ) }
72 70 2 71 clnbgrvtxedg 
 |-  ( ( G e. UHGraph /\ E e. I /\ A e. E ) -> E e. { x e. I | x C_ ( G ClNeighbVtx A ) } )
73 22 69 26 72 syl3anc 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> E e. { x e. I | x C_ ( G ClNeighbVtx A ) } )
74 imaeq2 
 |-  ( e = E -> ( f " e ) = ( f " E ) )
75 fveq2 
 |-  ( e = E -> ( g ` e ) = ( g ` E ) )
76 74 75 eqeq12d 
 |-  ( e = E -> ( ( f " e ) = ( g ` e ) <-> ( f " E ) = ( g ` E ) ) )
77 76 rspcv 
 |-  ( E e. { x e. I | x C_ ( G ClNeighbVtx A ) } -> ( A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) -> ( f " E ) = ( g ` E ) ) )
78 73 77 syl 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> ( A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) -> ( f " E ) = ( g ` E ) ) )
79 78 adantld 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> ( ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) -> ( f " E ) = ( g ` E ) ) )
80 79 adantr 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> ( ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) -> ( f " E ) = ( g ` E ) ) )
81 80 imp 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) /\ ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) ) -> ( f " E ) = ( g ` E ) )
82 55 68 81 3jca 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) /\ ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) ) -> ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ ( f " E ) = ( g ` E ) ) )
83 82 ex 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> ( ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) -> ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ ( f " E ) = ( g ` E ) ) ) )
84 83 eximdv 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) /\ f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) -> ( E. g ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) -> E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ ( f " E ) = ( g ` E ) ) ) )
85 84 expimpd 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> ( ( f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) ) -> E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ ( f " E ) = ( g ` E ) ) ) )
86 85 eximdv 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> ( E. f ( f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx A ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx A ) } ( f " e ) = ( g ` e ) ) ) -> E. f E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ ( f " E ) = ( g ` E ) ) ) )
87 46 86 syld 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> ( A. v e. ( Vtx ` G ) E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx v ) } ( f " e ) = ( g ` e ) ) ) -> E. f E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ ( f " E ) = ( g ` E ) ) ) )
88 87 adantld 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> ( ( F : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) /\ A. v e. ( Vtx ` G ) E. f ( f : ( G ClNeighbVtx v ) -1-1-onto-> ( H ClNeighbVtx ( F ` v ) ) /\ E. g ( g : { x e. I | x C_ ( G ClNeighbVtx v ) } -1-1-onto-> { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } /\ A. e e. { x e. I | x C_ ( G ClNeighbVtx v ) } ( f " e ) = ( g ` e ) ) ) ) -> E. f E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ ( f " E ) = ( g ` E ) ) ) )
89 19 88 mpd 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> E. f E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ ( f " E ) = ( g ` E ) ) )