This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝐴 )
clnbgrvtxedg.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
clnbgrvtxedg.k ⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
grlimedgclnbgr.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) )
grlimedgclnbgr.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
grlimedgclnbgr.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
Assertion grlimedgclnbgr ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )

Proof

Step Hyp Ref Expression
1 clnbgrvtxedg.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝐴 )
2 clnbgrvtxedg.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
3 clnbgrvtxedg.k ⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
4 grlimedgclnbgr.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) )
5 grlimedgclnbgr.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
6 grlimedgclnbgr.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
7 simp1l ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐺 ∈ USPGraph )
8 simp1r ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐻 ∈ USPGraph )
9 simp2 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) )
10 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
11 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
12 eqid ⊢ ( 𝐺 ClNeighbVtx 𝑣 ) = ( 𝐺 ClNeighbVtx 𝑣 )
13 eqid ⊢ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) )
14 sseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) ↔ 𝑦 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) ) )
15 14 cbvrabv ⊢ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } = { 𝑦 ∈ 𝐼 ∣ 𝑦 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) }
16 sseq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ↔ 𝑦 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ) )
17 16 cbvrabv ⊢ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } = { 𝑦 ∈ 𝐽 ∣ 𝑦 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) }
18 10 11 12 13 2 5 15 17 usgrlimprop ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ) → ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
19 7 8 9 18 syl3anc ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
20 uspgruhgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph )
21 20 adantr ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → 𝐺 ∈ UHGraph )
22 21 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐺 ∈ UHGraph )
23 2 eleq2i ⊢ ( 𝐸 ∈ 𝐼 ↔ 𝐸 ∈ ( Edg ‘ 𝐺 ) )
24 23 biimpi ⊢ ( 𝐸 ∈ 𝐼 → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
25 24 adantr ⊢ ( ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
26 25 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
27 simp3r ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐴 ∈ 𝐸 )
28 uhgredgrnv ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝐴 ∈ 𝐸 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
29 22 26 27 28 syl3anc ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
30 eqidd ⊢ ( 𝑣 = 𝐴 → 𝑓 = 𝑓 )
31 oveq2 ⊢ ( 𝑣 = 𝐴 → ( 𝐺 ClNeighbVtx 𝑣 ) = ( 𝐺 ClNeighbVtx 𝐴 ) )
32 fveq2 ⊢ ( 𝑣 = 𝐴 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) )
33 32 oveq2d ⊢ ( 𝑣 = 𝐴 → ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
34 30 31 33 f1oeq123d ⊢ ( 𝑣 = 𝐴 → ( 𝑓 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ↔ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) )
35 eqidd ⊢ ( 𝑣 = 𝐴 → 𝑔 = 𝑔 )
36 31 sseq2d ⊢ ( 𝑣 = 𝐴 → ( 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) ↔ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) ) )
37 36 rabbidv ⊢ ( 𝑣 = 𝐴 → { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } )
38 33 sseq2d ⊢ ( 𝑣 = 𝐴 → ( 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ↔ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) )
39 38 rabbidv ⊢ ( 𝑣 = 𝐴 → { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } )
40 35 37 39 f1oeq123d ⊢ ( 𝑣 = 𝐴 → ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ↔ 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) )
41 37 raleqdv ⊢ ( 𝑣 = 𝐴 → ( ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ↔ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) )
42 40 41 anbi12d ⊢ ( 𝑣 = 𝐴 → ( ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ↔ ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )
43 42 exbidv ⊢ ( 𝑣 = 𝐴 → ( ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ↔ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )
44 34 43 anbi12d ⊢ ( 𝑣 = 𝐴 → ( ( 𝑓 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ↔ ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
45 44 exbidv ⊢ ( 𝑣 = 𝐴 → ( ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
46 45 rspcv ⊢ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
47 29 46 syl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
48 eqid ⊢ 𝑓 = 𝑓
49 id ⊢ ( 𝑓 = 𝑓 → 𝑓 = 𝑓 )
50 1 a1i ⊢ ( 𝑓 = 𝑓 → 𝑁 = ( 𝐺 ClNeighbVtx 𝐴 ) )
51 4 a1i ⊢ ( 𝑓 = 𝑓 → 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
52 49 50 51 f1oeq123d ⊢ ( 𝑓 = 𝑓 → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ↔ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) )
53 48 52 ax-mp ⊢ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ↔ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
54 53 biimpri ⊢ ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) → 𝑓 : 𝑁 –1-1-onto→ 𝑀 )
55 54 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → 𝑓 : 𝑁 –1-1-onto→ 𝑀 )
56 55 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → 𝑓 : 𝑁 –1-1-onto→ 𝑀 )
57 eqid ⊢ 𝑔 = 𝑔
58 id ⊢ ( 𝑔 = 𝑔 → 𝑔 = 𝑔 )
59 1 sseq2i ⊢ ( 𝑥 ⊆ 𝑁 ↔ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) )
60 3 59 rabbieq ⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) }
61 60 a1i ⊢ ( 𝑔 = 𝑔 → 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } )
62 4 sseq2i ⊢ ( 𝑥 ⊆ 𝑀 ↔ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
63 6 62 rabbieq ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) }
64 63 a1i ⊢ ( 𝑔 = 𝑔 → 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } )
65 58 61 64 f1oeq123d ⊢ ( 𝑔 = 𝑔 → ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ↔ 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) )
66 57 65 ax-mp ⊢ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ↔ 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } )
67 66 biimpri ⊢ ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } → 𝑔 : 𝐾 –1-1-onto→ 𝐿 )
68 67 adantr ⊢ ( ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → 𝑔 : 𝐾 –1-1-onto→ 𝐿 )
69 68 adantl ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → 𝑔 : 𝐾 –1-1-onto→ 𝐿 )
70 simp3l ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐸 ∈ 𝐼 )
71 eqid ⊢ ( 𝐺 ClNeighbVtx 𝐴 ) = ( 𝐺 ClNeighbVtx 𝐴 )
72 eqid ⊢ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) }
73 71 2 72 clnbgrvtxedg ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) → 𝐸 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } )
74 22 70 27 73 syl3anc ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐸 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } )
75 imaeq2 ⊢ ( 𝑒 = 𝐸 → ( 𝑓 “ 𝑒 ) = ( 𝑓 “ 𝐸 ) )
76 fveq2 ⊢ ( 𝑒 = 𝐸 → ( 𝑔 ‘ 𝑒 ) = ( 𝑔 ‘ 𝐸 ) )
77 75 76 eqeq12d ⊢ ( 𝑒 = 𝐸 → ( ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ↔ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )
78 77 rspcv ⊢ ( 𝐸 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } → ( ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) → ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )
79 74 78 syl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ( ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) → ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )
80 79 adantld ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ( ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )
81 80 adantr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )
82 81 imp ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) )
83 56 69 82 3jca ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )
84 83 ex ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) ) )
85 84 eximdv ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) ) )
86 85 expimpd ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ( ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) ) )
87 86 eximdv ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ( ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) ) )
88 47 87 syld ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) ) )
89 88 adantld ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ( ( 𝐹 : ( Vtx ‘ 𝐺 ) –1-1-onto→ ( Vtx ‘ 𝐻 ) ∧ ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) ) )
90 19 89 mpd ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )