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 birani ⊢ ( ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
25 24 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐸 ∈ ( Edg ‘ 𝐺 ) )
26 simp3r ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐴 ∈ 𝐸 )
27 uhgredgrnv ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 ∈ ( Edg ‘ 𝐺 ) ∧ 𝐴 ∈ 𝐸 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
28 22 25 26 27 syl3anc ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
29 eqidd ⊢ ( 𝑣 = 𝐴 → 𝑓 = 𝑓 )
30 oveq2 ⊢ ( 𝑣 = 𝐴 → ( 𝐺 ClNeighbVtx 𝑣 ) = ( 𝐺 ClNeighbVtx 𝐴 ) )
31 fveq2 ⊢ ( 𝑣 = 𝐴 → ( 𝐹 ‘ 𝑣 ) = ( 𝐹 ‘ 𝐴 ) )
32 31 oveq2d ⊢ ( 𝑣 = 𝐴 → ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
33 29 30 32 f1oeq123d ⊢ ( 𝑣 = 𝐴 → ( 𝑓 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ↔ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) )
34 eqidd ⊢ ( 𝑣 = 𝐴 → 𝑔 = 𝑔 )
35 30 sseq2d ⊢ ( 𝑣 = 𝐴 → ( 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) ↔ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) ) )
36 35 rabbidv ⊢ ( 𝑣 = 𝐴 → { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } )
37 32 sseq2d ⊢ ( 𝑣 = 𝐴 → ( 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ↔ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) )
38 37 rabbidv ⊢ ( 𝑣 = 𝐴 → { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } )
39 34 36 38 f1oeq123d ⊢ ( 𝑣 = 𝐴 → ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ↔ 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) )
40 36 raleqdv ⊢ ( 𝑣 = 𝐴 → ( ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ↔ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) )
41 39 40 anbi12d ⊢ ( 𝑣 = 𝐴 → ( ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ↔ ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )
42 41 exbidv ⊢ ( 𝑣 = 𝐴 → ( ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ↔ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) )
43 33 42 anbi12d ⊢ ( 𝑣 = 𝐴 → ( ( 𝑓 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ↔ ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
44 43 exbidv ⊢ ( 𝑣 = 𝐴 → ( ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ↔ ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
45 44 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 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
46 28 45 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 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) ) )
47 eqid ⊢ 𝑓 = 𝑓
48 id ⊢ ( 𝑓 = 𝑓 → 𝑓 = 𝑓 )
49 1 a1i ⊢ ( 𝑓 = 𝑓 → 𝑁 = ( 𝐺 ClNeighbVtx 𝐴 ) )
50 4 a1i ⊢ ( 𝑓 = 𝑓 → 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
51 48 49 50 f1oeq123d ⊢ ( 𝑓 = 𝑓 → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ↔ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) )
52 47 51 ax-mp ⊢ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ↔ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
53 52 biimpri ⊢ ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) → 𝑓 : 𝑁 –1-1-onto→ 𝑀 )
54 53 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → 𝑓 : 𝑁 –1-1-onto→ 𝑀 )
55 54 adantr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → 𝑓 : 𝑁 –1-1-onto→ 𝑀 )
56 eqid ⊢ 𝑔 = 𝑔
57 id ⊢ ( 𝑔 = 𝑔 → 𝑔 = 𝑔 )
58 1 sseq2i ⊢ ( 𝑥 ⊆ 𝑁 ↔ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) )
59 3 58 rabbieq ⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) }
60 59 a1i ⊢ ( 𝑔 = 𝑔 → 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } )
61 4 sseq2i ⊢ ( 𝑥 ⊆ 𝑀 ↔ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
62 6 61 rabbieq ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) }
63 62 a1i ⊢ ( 𝑔 = 𝑔 → 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } )
64 57 60 63 f1oeq123d ⊢ ( 𝑔 = 𝑔 → ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ↔ 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ) )
65 56 64 ax-mp ⊢ ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 ↔ 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } )
66 65 biimpri ⊢ ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } → 𝑔 : 𝐾 –1-1-onto→ 𝐿 )
67 66 adantr ⊢ ( ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → 𝑔 : 𝐾 –1-1-onto→ 𝐿 )
68 67 adantl ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → 𝑔 : 𝐾 –1-1-onto→ 𝐿 )
69 simp3l ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐸 ∈ 𝐼 )
70 eqid ⊢ ( 𝐺 ClNeighbVtx 𝐴 ) = ( 𝐺 ClNeighbVtx 𝐴 )
71 eqid ⊢ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) }
72 70 2 71 clnbgrvtxedg ⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) → 𝐸 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } )
73 22 69 26 72 syl3anc ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → 𝐸 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } )
74 imaeq2 ⊢ ( 𝑒 = 𝐸 → ( 𝑓 “ 𝑒 ) = ( 𝑓 “ 𝐸 ) )
75 fveq2 ⊢ ( 𝑒 = 𝐸 → ( 𝑔 ‘ 𝑒 ) = ( 𝑔 ‘ 𝐸 ) )
76 74 75 eqeq12d ⊢ ( 𝑒 = 𝐸 → ( ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ↔ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )
77 76 rspcv ⊢ ( 𝐸 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } → ( ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) → ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )
78 73 77 syl ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ( ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) → ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )
79 78 adantld ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ( ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )
80 79 adantr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )
81 80 imp ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) )
82 55 68 81 3jca ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) ∧ ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )
83 82 ex ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) ) )
84 83 eximdv ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) ∧ 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) → ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) ) )
85 84 expimpd ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ( ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) ) )
86 85 eximdv ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ( ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝐴 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝐴 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) ) )
87 46 86 syld ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ( ∀ 𝑣 ∈ ( Vtx ‘ 𝐺 ) ∃ 𝑓 ( 𝑓 : ( 𝐺 ClNeighbVtx 𝑣 ) –1-1-onto→ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) ∧ ∃ 𝑔 ( 𝑔 : { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } –1-1-onto→ { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝑣 ) ) } ∧ ∀ 𝑒 ∈ { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ ( 𝐺 ClNeighbVtx 𝑣 ) } ( 𝑓 “ 𝑒 ) = ( 𝑔 ‘ 𝑒 ) ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) ) )
88 87 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→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) ) )
89 19 88 mpd ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐸 ∈ 𝐼 ∧ 𝐴 ∈ 𝐸 ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ 𝐸 ) = ( 𝑔 ‘ 𝐸 ) ) )