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