Metamath Proof Explorer

Theorem grlimprclnbgrvtx

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

Ref Expression
Hypotheses clnbgrvtxedg.n ⊢ 𝑁 = ( 𝐺 ClNeighbVtx 𝐴 )
clnbgrvtxedg.i ⊢ 𝐼 = ( Edg ‘ 𝐺 )
clnbgrvtxedg.k ⊢ 𝐾 = { 𝑥 ∈ 𝐼 ∣ 𝑥 ⊆ 𝑁 }
grlimedgclnbgr.m ⊢ 𝑀 = ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) )
grlimedgclnbgr.j ⊢ 𝐽 = ( Edg ‘ 𝐻 )
grlimedgclnbgr.l ⊢ 𝐿 = { 𝑥 ∈ 𝐽 ∣ 𝑥 ⊆ 𝑀 }
Assertion grlimprclnbgrvtx ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ∃ 𝑓 ( 𝑓 : 𝑁 –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 1 2 3 4 5 6 grlimprclnbgredg ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) )
8 simprl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) → 𝑓 : 𝑁 –1-1-onto→ 𝑀 )
9 sseq1 ⊢ ( 𝑥 = { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } → ( 𝑥 ⊆ 𝑀 ↔ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 ) )
10 9 6 elrab2 ⊢ ( { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ↔ ( { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 ) )
11 10 bilani ⊢ ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) → ( { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 ) )
12 11 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) → ( { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 ) )
13 fvex ⊢ ( 𝑓 ‘ 𝐴 ) ∈ V
14 fvex ⊢ ( 𝑓 ‘ 𝐵 ) ∈ V
15 13 14 prss ⊢ ( ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ↔ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 )
16 uspgrupgr ⊢ ( 𝐻 ∈ USPGraph → 𝐻 ∈ UPGraph )
17 16 adantl ⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) → 𝐻 ∈ UPGraph )
18 17 3ad2ant1 ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → 𝐻 ∈ UPGraph )
19 18 ad2antrr ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) → 𝐻 ∈ UPGraph )
20 4 eleq2i ⊢ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ↔ ( 𝑓 ‘ 𝐴 ) ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
21 5 clnbupgreli ⊢ ( ( 𝐻 ∈ UPGraph ∧ ( 𝑓 ‘ 𝐴 ) ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( ( 𝑓 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) )
22 21 ex ⊢ ( 𝐻 ∈ UPGraph → ( ( 𝑓 ‘ 𝐴 ) ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) → ( ( 𝑓 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ) )
23 20 22 biimtrid ⊢ ( 𝐻 ∈ UPGraph → ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 → ( ( 𝑓 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ) )
24 4 eleq2i ⊢ ( ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ↔ ( 𝑓 ‘ 𝐵 ) ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
25 5 clnbupgreli ⊢ ( ( 𝐻 ∈ UPGraph ∧ ( 𝑓 ‘ 𝐵 ) ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) ) → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) )
26 25 ex ⊢ ( 𝐻 ∈ UPGraph → ( ( 𝑓 ‘ 𝐵 ) ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ) )
27 24 26 biimtrid ⊢ ( 𝐻 ∈ UPGraph → ( ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ) )
28 23 27 anim12d ⊢ ( 𝐻 ∈ UPGraph → ( ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) → ( ( ( 𝑓 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ) ) )
29 19 28 syl ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) → ( ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) → ( ( ( 𝑓 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ) ) )
30 29 imp ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) → ( ( ( 𝑓 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ) )
31 prcom ⊢ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = { ( 𝑓 ‘ 𝐵 ) , ( 𝑓 ‘ 𝐴 ) }
32 preq1 ⊢ ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) → { ( 𝑓 ‘ 𝐵 ) , ( 𝑓 ‘ 𝐴 ) } = { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } )
33 31 32 eqtrid ⊢ ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) → { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } = { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } )
34 33 eleq1d ⊢ ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) → ( { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ↔ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) )
35 34 biimpcd ⊢ ( { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) → { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) )
36 35 adantl ⊢ ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) → { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) )
37 36 adantl ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) → { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) )
38 37 ad2antrr ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) → ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) → { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) )
39 prcom ⊢ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } = { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) }
40 39 eleq1i ⊢ ( { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ↔ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 )
41 40 bilani ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) ∧ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) → { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 )
42 19 ad2antrr ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) ∧ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) → 𝐻 ∈ UPGraph )
43 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
44 14 43 pm3.2i ⊢ ( ( 𝑓 ‘ 𝐵 ) ∈ V ∧ ( 𝐹 ‘ 𝐴 ) ∈ V )
45 44 a1i ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) ∧ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) → ( ( 𝑓 ‘ 𝐵 ) ∈ V ∧ ( 𝐹 ‘ 𝐴 ) ∈ V ) )
46 simpr ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) ∧ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) → { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 )
47 42 45 46 3jca ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) ∧ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) → ( 𝐻 ∈ UPGraph ∧ ( ( 𝑓 ‘ 𝐵 ) ∈ V ∧ ( 𝐹 ‘ 𝐴 ) ∈ V ) ∧ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) )
48 eqid ⊢ ( Vtx ‘ 𝐻 ) = ( Vtx ‘ 𝐻 )
49 48 5 upgrpredgv ⊢ ( ( 𝐻 ∈ UPGraph ∧ ( ( 𝑓 ‘ 𝐵 ) ∈ V ∧ ( 𝐹 ‘ 𝐴 ) ∈ V ) ∧ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) → ( ( 𝑓 ‘ 𝐵 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( Vtx ‘ 𝐻 ) ) )
50 simpr ⊢ ( ( ( 𝑓 ‘ 𝐵 ) ∈ ( Vtx ‘ 𝐻 ) ∧ ( 𝐹 ‘ 𝐴 ) ∈ ( Vtx ‘ 𝐻 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( Vtx ‘ 𝐻 ) )
51 47 49 50 3syl ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) ∧ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( Vtx ‘ 𝐻 ) )
52 48 clnbgrvtxel ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( Vtx ‘ 𝐻 ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
53 4 eleq2i ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝑀 ↔ ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐻 ClNeighbVtx ( 𝐹 ‘ 𝐴 ) ) )
54 52 53 sylibr ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( Vtx ‘ 𝐻 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑀 )
55 51 54 syl ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) ∧ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝑀 )
56 simplrr ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) ∧ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) → ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 )
57 55 56 prssd ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) ∧ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) → { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 )
58 sseq1 ⊢ ( 𝑥 = { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } → ( 𝑥 ⊆ 𝑀 ↔ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 ) )
59 58 6 elrab2 ⊢ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ↔ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ∧ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 ) )
60 41 57 59 sylanbrc ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) ∧ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) → { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 )
61 60 ex ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) → ( { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 → { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) )
62 38 61 orim12d ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) → ( ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) → ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) )
63 62 imp ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) ∧ ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ) → ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) )
64 63 orcomd ⊢ ( ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) ∧ ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ) → ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) )
65 64 ex ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) → ( ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) → ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) ) )
66 65 adantld ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) → ( ( ( ( 𝑓 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐴 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐴 ) ∨ { ( 𝑓 ‘ 𝐵 ) , ( 𝐹 ‘ 𝐴 ) } ∈ 𝐽 ) ) → ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) ) )
67 30 66 mpd ⊢ ( ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) ∧ ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) ) → ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) )
68 67 ex ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) → ( ( ( 𝑓 ‘ 𝐴 ) ∈ 𝑀 ∧ ( 𝑓 ‘ 𝐵 ) ∈ 𝑀 ) → ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) ) )
69 15 68 biimtrrid ⊢ ( ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ) → ( { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 → ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) ) )
70 69 expimpd ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) → ( ( { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐽 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ⊆ 𝑀 ) → ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) ) )
71 12 70 mpd ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) → ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) )
72 8 71 jca ⊢ ( ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) ∧ ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) ) )
73 72 ex ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ( ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) → ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) ) ) )
74 73 eximdv ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ( ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ { ( 𝑓 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ) → ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) ) ) )
75 7 74 mpd ⊢ ( ( ( 𝐺 ∈ USPGraph ∧ 𝐻 ∈ USPGraph ) ∧ 𝐹 ∈ ( 𝐺 GraphLocIso 𝐻 ) ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ∧ { 𝐴 , 𝐵 } ∈ 𝐼 ) ) → ∃ 𝑓 ( 𝑓 : 𝑁 –1-1-onto→ 𝑀 ∧ ( { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐵 ) } ∈ 𝐿 ∨ { ( 𝐹 ‘ 𝐴 ) , ( 𝑓 ‘ 𝐴 ) } ∈ 𝐿 ) ) )