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 biimpi 
 |-  ( E e. I -> E e. ( Edg ` G ) )
25 24 adantr 
 |-  ( ( E e. I /\ A e. E ) -> E e. ( Edg ` G ) )
26 25 3ad2ant3 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> E e. ( Edg ` G ) )
27 simp3r 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> A e. E )
28 uhgredgrnv 
 |-  ( ( G e. UHGraph /\ E e. ( Edg ` G ) /\ A e. E ) -> A e. ( Vtx ` G ) )
29 22 26 27 28 syl3anc 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> A e. ( Vtx ` G ) )
30 eqidd 
 |-  ( v = A -> f = f )
31 oveq2 
 |-  ( v = A -> ( G ClNeighbVtx v ) = ( G ClNeighbVtx A ) )
32 fveq2 
 |-  ( v = A -> ( F ` v ) = ( F ` A ) )
33 32 oveq2d 
 |-  ( v = A -> ( H ClNeighbVtx ( F ` v ) ) = ( H ClNeighbVtx ( F ` A ) ) )
34 30 31 33 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 ) ) ) )
35 eqidd 
 |-  ( v = A -> g = g )
36 31 sseq2d 
 |-  ( v = A -> ( x C_ ( G ClNeighbVtx v ) <-> x C_ ( G ClNeighbVtx A ) ) )
37 36 rabbidv 
 |-  ( v = A -> { x e. I | x C_ ( G ClNeighbVtx v ) } = { x e. I | x C_ ( G ClNeighbVtx A ) } )
38 33 sseq2d 
 |-  ( v = A -> ( x C_ ( H ClNeighbVtx ( F ` v ) ) <-> x C_ ( H ClNeighbVtx ( F ` A ) ) ) )
39 38 rabbidv 
 |-  ( v = A -> { x e. J | x C_ ( H ClNeighbVtx ( F ` v ) ) } = { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } )
40 35 37 39 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 ) ) } ) )
41 37 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 ) ) )
42 40 41 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 ) ) ) )
43 42 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 ) ) ) )
44 34 43 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 ) ) ) ) )
45 44 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 ) ) ) ) )
46 45 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 ) ) ) ) )
47 29 46 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 ) ) ) ) )
48 eqid 
 |-  f = f
49 id 
 |-  ( f = f -> f = f )
50 1 a1i 
 |-  ( f = f -> N = ( G ClNeighbVtx A ) )
51 4 a1i 
 |-  ( f = f -> M = ( H ClNeighbVtx ( F ` A ) ) )
52 49 50 51 f1oeq123d 
 |-  ( f = f -> ( f : N -1-1-onto-> M <-> f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) ) )
53 48 52 ax-mp 
 |-  ( f : N -1-1-onto-> M <-> f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) )
54 53 biimpri 
 |-  ( f : ( G ClNeighbVtx A ) -1-1-onto-> ( H ClNeighbVtx ( F ` A ) ) -> f : N -1-1-onto-> M )
55 54 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 )
56 55 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 )
57 eqid 
 |-  g = g
58 id 
 |-  ( g = g -> g = g )
59 1 sseq2i 
 |-  ( x C_ N <-> x C_ ( G ClNeighbVtx A ) )
60 3 59 rabbieq 
 |-  K = { x e. I | x C_ ( G ClNeighbVtx A ) }
61 60 a1i 
 |-  ( g = g -> K = { x e. I | x C_ ( G ClNeighbVtx A ) } )
62 4 sseq2i 
 |-  ( x C_ M <-> x C_ ( H ClNeighbVtx ( F ` A ) ) )
63 6 62 rabbieq 
 |-  L = { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) }
64 63 a1i 
 |-  ( g = g -> L = { x e. J | x C_ ( H ClNeighbVtx ( F ` A ) ) } )
65 58 61 64 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 ) ) } ) )
66 57 65 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 ) ) } )
67 66 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 )
68 67 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 )
69 68 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 )
70 simp3l 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( E e. I /\ A e. E ) ) -> E e. I )
71 eqid 
 |-  ( G ClNeighbVtx A ) = ( G ClNeighbVtx A )
72 eqid 
 |-  { x e. I | x C_ ( G ClNeighbVtx A ) } = { x e. I | x C_ ( G ClNeighbVtx A ) }
73 71 2 72 clnbgrvtxedg 
 |-  ( ( G e. UHGraph /\ E e. I /\ A e. E ) -> E e. { x e. I | x C_ ( G ClNeighbVtx A ) } )
74 22 70 27 73 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 ) } )
75 imaeq2 
 |-  ( e = E -> ( f " e ) = ( f " E ) )
76 fveq2 
 |-  ( e = E -> ( g ` e ) = ( g ` E ) )
77 75 76 eqeq12d 
 |-  ( e = E -> ( ( f " e ) = ( g ` e ) <-> ( f " E ) = ( g ` E ) ) )
78 77 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 ) ) )
79 74 78 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 ) ) )
80 79 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 ) ) )
81 80 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 ) ) )
82 81 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 ) )
83 56 69 82 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 ) ) )
84 83 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 ) ) ) )
85 84 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 ) ) ) )
86 85 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 ) ) ) )
87 86 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 ) ) ) )
88 47 87 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 ) ) ) )
89 88 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 ) ) ) )
90 19 89 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 ) ) )