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

Metamath Proof Explorer

Theorem grlimprclnbgr

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 { A , B } 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 grlimprclnbgr ( ( ( 𝐺 ∈ 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 simp3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → { 𝐴 , 𝐵 } ∈ 𝐼 )
8 prid1g ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ { 𝐴 , 𝐵 } )
9 8 3ad2ant1 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
10 7 9 jca ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → ( { 𝐴 , 𝐵 } ∈ 𝐼 ∧ 𝐴 ∈ { 𝐴 , 𝐵 } ) )
11 1 2 3 4 5 6 grlimedgclnbgr ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( { 𝐴 , 𝐵 } ∈ 𝐼 ∧ 𝐴 ∈ { 𝐴 , 𝐵 } ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) )
12 10 11 syl3an3 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) )
13 simpr1 ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) → 𝑓 : 𝑁 –1-1-onto→ 𝑀 )
14 simpr2 ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) → 𝑔 : 𝐾 –1-1-onto→ 𝐿 )
15 f1ofn ⊢ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 → 𝑓 Fn 𝑁 )
16 15 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → 𝑓 Fn 𝑁 )
17 uspgruhgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UHGraph )
18 17 adantr ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → 𝐺 ∈ UHGraph )
19 18 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → 𝐺 ∈ UHGraph )
20 2 eleq2i ⊢ ( { 𝐴 , 𝐵 } ∈ 𝐼 ↔ { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) )
21 20 biimpi ⊢ ( { 𝐴 , 𝐵 } ∈ 𝐼 → { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) )
22 21 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) )
23 22 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) )
24 9 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → 𝐴 ∈ { 𝐴 , 𝐵 } )
25 uhgredgrnv ⊢ ( ( 𝐺 ∈ UHGraph ∧ { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ 𝐴 ∈ { 𝐴 , 𝐵 } ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
26 19 23 24 25 syl3anc ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
27 26 adantr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) )
28 eqid ⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
29 28 clnbgrvtxel ⊢ ( 𝐴 ∈ ( Vtx ‘ 𝐺 ) → 𝐴 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) )
30 27 29 syl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → 𝐴 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) )
31 30 1 eleqtrrdi ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → 𝐴 ∈ 𝑁 )
32 prcom ⊢ { 𝐴 , 𝐵 } = { 𝐵 , 𝐴 }
33 32 eleq1i ⊢ ( { 𝐴 , 𝐵 } ∈ 𝐼 ↔ { 𝐵 , 𝐴 } ∈ 𝐼 )
34 33 biimpi ⊢ ( { 𝐴 , 𝐵 } ∈ 𝐼 → { 𝐵 , 𝐴 } ∈ 𝐼 )
35 34 3ad2ant3 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → { 𝐵 , 𝐴 } ∈ 𝐼 )
36 35 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → { 𝐵 , 𝐴 } ∈ 𝐼 )
37 36 adantr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → { 𝐵 , 𝐴 } ∈ 𝐼 )
38 37 olcd ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( 𝐵 = 𝐴 ∨ { 𝐵 , 𝐴 } ∈ 𝐼 ) )
39 uspgrupgr ⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
40 39 adantr ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → 𝐺 ∈ UPGraph )
41 40 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → 𝐺 ∈ UPGraph )
42 prid2g ⊢ ( 𝐵 ∈ 𝑊 → 𝐵 ∈ { 𝐴 , 𝐵 } )
43 42 3ad2ant2 ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) → 𝐵 ∈ { 𝐴 , 𝐵 } )
44 43 3ad2ant3 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → 𝐵 ∈ { 𝐴 , 𝐵 } )
45 uhgredgrnv ⊢ ( ( 𝐺 ∈ UHGraph ∧ { 𝐴 , 𝐵 } ∈ ( Edg ‘ 𝐺 ) ∧ 𝐵 ∈ { 𝐴 , 𝐵 } ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
46 19 23 44 45 syl3anc ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → 𝐵 ∈ ( Vtx ‘ 𝐺 ) )
47 41 26 46 3jca ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) )
48 47 adantr ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) )
49 28 2 clnbupgrel ⊢ ( ( 𝐺 ∈ UPGraph ∧ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ∧ 𝐵 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐵 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) ↔ ( 𝐵 = 𝐴 ∨ { 𝐵 , 𝐴 } ∈ 𝐼 ) ) )
50 48 49 syl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( 𝐵 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) ↔ ( 𝐵 = 𝐴 ∨ { 𝐵 , 𝐴 } ∈ 𝐼 ) ) )
51 38 50 mpbird ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → 𝐵 ∈ ( 𝐺 ClNeighbVtx 𝐴 ) )
52 51 1 eleqtrrdi ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → 𝐵 ∈ 𝑁 )
53 fnimapr ⊢ ( ( 𝑓 Fn 𝑁 ∧ 𝐴 ∈ 𝑁 ∧ 𝐵 ∈ 𝑁 ) → ( 𝑓 “ { 𝐴 , 𝐵 } ) = { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } )
54 16 31 52 53 syl3anc ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( 𝑓 “ { 𝐴 , 𝐵 } ) = { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } )
55 54 eqeq1d ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ↔ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) )
56 55 biimpd ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) → { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) )
57 56 a1d ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ 𝑓 : 𝑁 –1-1-onto→ 𝑀 ) → ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 → ( ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) → { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) )
58 57 ex ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 → ( 𝑔 : 𝐾 –1-1-onto→ 𝐿 → ( ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) → { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) ) )
59 58 3imp2 ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) → { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) )
60 13 14 59 3jca ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) )
61 60 ex ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) )
62 61 2eximdv ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ( ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ ( 𝑓 “ { 𝐴 , 𝐵 } ) = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) ) )
63 12 62 mpd ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ∃ 𝑓 ∃ 𝑔 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ 𝑔 : 𝐾 –1-1-onto→ 𝐿 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = ( 𝑔 ‘ { 𝐴 , 𝐵 } ) ) )