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 
|- N = ( G ClNeighbVtx A )
clnbgrvtxedg.i 
|- I = ( Edg ` G )
clnbgrvtxedg.k 
|- K = { x e. I | x C_ N }
grlimedgclnbgr.m 
|- M = ( H ClNeighbVtx ( F ` A ) )
grlimedgclnbgr.j 
|- J = ( Edg ` H )
grlimedgclnbgr.l 
|- L = { x e. J | x C_ M }
Assertion grlimprclnbgrvtx 
|- ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> E. f ( f : N -1-1-onto-> M /\ ( { ( F ` A ) , ( f ` B ) } e. L \/ { ( F ` A ) , ( f ` A ) } e. L ) ) )

Proof

Step Hyp Ref Expression
1 clnbgrvtxedg.n 
 |-  N = ( G ClNeighbVtx A )
2 clnbgrvtxedg.i 
 |-  I = ( Edg ` G )
3 clnbgrvtxedg.k 
 |-  K = { x e. I | x C_ N }
4 grlimedgclnbgr.m 
 |-  M = ( H ClNeighbVtx ( F ` A ) )
5 grlimedgclnbgr.j 
 |-  J = ( Edg ` H )
6 grlimedgclnbgr.l 
 |-  L = { x e. J | x C_ M }
7 1 2 3 4 5 6 grlimprclnbgredg 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> E. f ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) )
8 simprl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) -> f : N -1-1-onto-> M )
9 sseq1 
 |-  ( x = { ( f ` A ) , ( f ` B ) } -> ( x C_ M <-> { ( f ` A ) , ( f ` B ) } C_ M ) )
10 9 6 elrab2 
 |-  ( { ( f ` A ) , ( f ` B ) } e. L <-> ( { ( f ` A ) , ( f ` B ) } e. J /\ { ( f ` A ) , ( f ` B ) } C_ M ) )
11 10 biimpi 
 |-  ( { ( f ` A ) , ( f ` B ) } e. L -> ( { ( f ` A ) , ( f ` B ) } e. J /\ { ( f ` A ) , ( f ` B ) } C_ M ) )
12 11 adantl 
 |-  ( ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) -> ( { ( f ` A ) , ( f ` B ) } e. J /\ { ( f ` A ) , ( f ` B ) } C_ M ) )
13 12 adantl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) -> ( { ( f ` A ) , ( f ` B ) } e. J /\ { ( f ` A ) , ( f ` B ) } C_ M ) )
14 fvex 
 |-  ( f ` A ) e. _V
15 fvex 
 |-  ( f ` B ) e. _V
16 14 15 prss 
 |-  ( ( ( f ` A ) e. M /\ ( f ` B ) e. M ) <-> { ( f ` A ) , ( f ` B ) } C_ M )
17 uspgrupgr 
 |-  ( H e. USPGraph -> H e. UPGraph )
18 17 adantl 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> H e. UPGraph )
19 18 3ad2ant1 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> H e. UPGraph )
20 19 ad2antrr 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) -> H e. UPGraph )
21 4 eleq2i 
 |-  ( ( f ` A ) e. M <-> ( f ` A ) e. ( H ClNeighbVtx ( F ` A ) ) )
22 5 clnbupgreli 
 |-  ( ( H e. UPGraph /\ ( f ` A ) e. ( H ClNeighbVtx ( F ` A ) ) ) -> ( ( f ` A ) = ( F ` A ) \/ { ( f ` A ) , ( F ` A ) } e. J ) )
23 22 ex 
 |-  ( H e. UPGraph -> ( ( f ` A ) e. ( H ClNeighbVtx ( F ` A ) ) -> ( ( f ` A ) = ( F ` A ) \/ { ( f ` A ) , ( F ` A ) } e. J ) ) )
24 21 23 biimtrid 
 |-  ( H e. UPGraph -> ( ( f ` A ) e. M -> ( ( f ` A ) = ( F ` A ) \/ { ( f ` A ) , ( F ` A ) } e. J ) ) )
25 4 eleq2i 
 |-  ( ( f ` B ) e. M <-> ( f ` B ) e. ( H ClNeighbVtx ( F ` A ) ) )
26 5 clnbupgreli 
 |-  ( ( H e. UPGraph /\ ( f ` B ) e. ( H ClNeighbVtx ( F ` A ) ) ) -> ( ( f ` B ) = ( F ` A ) \/ { ( f ` B ) , ( F ` A ) } e. J ) )
27 26 ex 
 |-  ( H e. UPGraph -> ( ( f ` B ) e. ( H ClNeighbVtx ( F ` A ) ) -> ( ( f ` B ) = ( F ` A ) \/ { ( f ` B ) , ( F ` A ) } e. J ) ) )
28 25 27 biimtrid 
 |-  ( H e. UPGraph -> ( ( f ` B ) e. M -> ( ( f ` B ) = ( F ` A ) \/ { ( f ` B ) , ( F ` A ) } e. J ) ) )
29 24 28 anim12d 
 |-  ( H e. UPGraph -> ( ( ( f ` A ) e. M /\ ( f ` B ) e. M ) -> ( ( ( f ` A ) = ( F ` A ) \/ { ( f ` A ) , ( F ` A ) } e. J ) /\ ( ( f ` B ) = ( F ` A ) \/ { ( f ` B ) , ( F ` A ) } e. J ) ) ) )
30 20 29 syl 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) -> ( ( ( f ` A ) e. M /\ ( f ` B ) e. M ) -> ( ( ( f ` A ) = ( F ` A ) \/ { ( f ` A ) , ( F ` A ) } e. J ) /\ ( ( f ` B ) = ( F ` A ) \/ { ( f ` B ) , ( F ` A ) } e. J ) ) ) )
31 30 imp 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) -> ( ( ( f ` A ) = ( F ` A ) \/ { ( f ` A ) , ( F ` A ) } e. J ) /\ ( ( f ` B ) = ( F ` A ) \/ { ( f ` B ) , ( F ` A ) } e. J ) ) )
32 prcom 
 |-  { ( f ` A ) , ( f ` B ) } = { ( f ` B ) , ( f ` A ) }
33 preq1 
 |-  ( ( f ` B ) = ( F ` A ) -> { ( f ` B ) , ( f ` A ) } = { ( F ` A ) , ( f ` A ) } )
34 32 33 eqtrid 
 |-  ( ( f ` B ) = ( F ` A ) -> { ( f ` A ) , ( f ` B ) } = { ( F ` A ) , ( f ` A ) } )
35 34 eleq1d 
 |-  ( ( f ` B ) = ( F ` A ) -> ( { ( f ` A ) , ( f ` B ) } e. L <-> { ( F ` A ) , ( f ` A ) } e. L ) )
36 35 biimpcd 
 |-  ( { ( f ` A ) , ( f ` B ) } e. L -> ( ( f ` B ) = ( F ` A ) -> { ( F ` A ) , ( f ` A ) } e. L ) )
37 36 adantl 
 |-  ( ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) -> ( ( f ` B ) = ( F ` A ) -> { ( F ` A ) , ( f ` A ) } e. L ) )
38 37 adantl 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) -> ( ( f ` B ) = ( F ` A ) -> { ( F ` A ) , ( f ` A ) } e. L ) )
39 38 ad2antrr 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) -> ( ( f ` B ) = ( F ` A ) -> { ( F ` A ) , ( f ` A ) } e. L ) )
40 prcom 
 |-  { ( f ` B ) , ( F ` A ) } = { ( F ` A ) , ( f ` B ) }
41 40 eleq1i 
 |-  ( { ( f ` B ) , ( F ` A ) } e. J <-> { ( F ` A ) , ( f ` B ) } e. J )
42 41 biimpi 
 |-  ( { ( f ` B ) , ( F ` A ) } e. J -> { ( F ` A ) , ( f ` B ) } e. J )
43 42 adantl 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) /\ { ( f ` B ) , ( F ` A ) } e. J ) -> { ( F ` A ) , ( f ` B ) } e. J )
44 20 ad2antrr 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) /\ { ( f ` B ) , ( F ` A ) } e. J ) -> H e. UPGraph )
45 fvex 
 |-  ( F ` A ) e. _V
46 15 45 pm3.2i 
 |-  ( ( f ` B ) e. _V /\ ( F ` A ) e. _V )
47 46 a1i 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) /\ { ( f ` B ) , ( F ` A ) } e. J ) -> ( ( f ` B ) e. _V /\ ( F ` A ) e. _V ) )
48 simpr 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) /\ { ( f ` B ) , ( F ` A ) } e. J ) -> { ( f ` B ) , ( F ` A ) } e. J )
49 44 47 48 3jca 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) /\ { ( f ` B ) , ( F ` A ) } e. J ) -> ( H e. UPGraph /\ ( ( f ` B ) e. _V /\ ( F ` A ) e. _V ) /\ { ( f ` B ) , ( F ` A ) } e. J ) )
50 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
51 50 5 upgrpredgv 
 |-  ( ( H e. UPGraph /\ ( ( f ` B ) e. _V /\ ( F ` A ) e. _V ) /\ { ( f ` B ) , ( F ` A ) } e. J ) -> ( ( f ` B ) e. ( Vtx ` H ) /\ ( F ` A ) e. ( Vtx ` H ) ) )
52 simpr 
 |-  ( ( ( f ` B ) e. ( Vtx ` H ) /\ ( F ` A ) e. ( Vtx ` H ) ) -> ( F ` A ) e. ( Vtx ` H ) )
53 49 51 52 3syl 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) /\ { ( f ` B ) , ( F ` A ) } e. J ) -> ( F ` A ) e. ( Vtx ` H ) )
54 50 clnbgrvtxel 
 |-  ( ( F ` A ) e. ( Vtx ` H ) -> ( F ` A ) e. ( H ClNeighbVtx ( F ` A ) ) )
55 4 eleq2i 
 |-  ( ( F ` A ) e. M <-> ( F ` A ) e. ( H ClNeighbVtx ( F ` A ) ) )
56 54 55 sylibr 
 |-  ( ( F ` A ) e. ( Vtx ` H ) -> ( F ` A ) e. M )
57 53 56 syl 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) /\ { ( f ` B ) , ( F ` A ) } e. J ) -> ( F ` A ) e. M )
58 simplrr 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) /\ { ( f ` B ) , ( F ` A ) } e. J ) -> ( f ` B ) e. M )
59 57 58 prssd 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) /\ { ( f ` B ) , ( F ` A ) } e. J ) -> { ( F ` A ) , ( f ` B ) } C_ M )
60 sseq1 
 |-  ( x = { ( F ` A ) , ( f ` B ) } -> ( x C_ M <-> { ( F ` A ) , ( f ` B ) } C_ M ) )
61 60 6 elrab2 
 |-  ( { ( F ` A ) , ( f ` B ) } e. L <-> ( { ( F ` A ) , ( f ` B ) } e. J /\ { ( F ` A ) , ( f ` B ) } C_ M ) )
62 43 59 61 sylanbrc 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) /\ { ( f ` B ) , ( F ` A ) } e. J ) -> { ( F ` A ) , ( f ` B ) } e. L )
63 62 ex 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) -> ( { ( f ` B ) , ( F ` A ) } e. J -> { ( F ` A ) , ( f ` B ) } e. L ) )
64 39 63 orim12d 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) -> ( ( ( f ` B ) = ( F ` A ) \/ { ( f ` B ) , ( F ` A ) } e. J ) -> ( { ( F ` A ) , ( f ` A ) } e. L \/ { ( F ` A ) , ( f ` B ) } e. L ) ) )
65 64 imp 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) /\ ( ( f ` B ) = ( F ` A ) \/ { ( f ` B ) , ( F ` A ) } e. J ) ) -> ( { ( F ` A ) , ( f ` A ) } e. L \/ { ( F ` A ) , ( f ` B ) } e. L ) )
66 65 orcomd 
 |-  ( ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) /\ ( ( f ` B ) = ( F ` A ) \/ { ( f ` B ) , ( F ` A ) } e. J ) ) -> ( { ( F ` A ) , ( f ` B ) } e. L \/ { ( F ` A ) , ( f ` A ) } e. L ) )
67 66 ex 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) -> ( ( ( f ` B ) = ( F ` A ) \/ { ( f ` B ) , ( F ` A ) } e. J ) -> ( { ( F ` A ) , ( f ` B ) } e. L \/ { ( F ` A ) , ( f ` A ) } e. L ) ) )
68 67 adantld 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) -> ( ( ( ( f ` A ) = ( F ` A ) \/ { ( f ` A ) , ( F ` A ) } e. J ) /\ ( ( f ` B ) = ( F ` A ) \/ { ( f ` B ) , ( F ` A ) } e. J ) ) -> ( { ( F ` A ) , ( f ` B ) } e. L \/ { ( F ` A ) , ( f ` A ) } e. L ) ) )
69 31 68 mpd 
 |-  ( ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) /\ ( ( f ` A ) e. M /\ ( f ` B ) e. M ) ) -> ( { ( F ` A ) , ( f ` B ) } e. L \/ { ( F ` A ) , ( f ` A ) } e. L ) )
70 69 ex 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) -> ( ( ( f ` A ) e. M /\ ( f ` B ) e. M ) -> ( { ( F ` A ) , ( f ` B ) } e. L \/ { ( F ` A ) , ( f ` A ) } e. L ) ) )
71 16 70 biimtrrid 
 |-  ( ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) /\ { ( f ` A ) , ( f ` B ) } e. J ) -> ( { ( f ` A ) , ( f ` B ) } C_ M -> ( { ( F ` A ) , ( f ` B ) } e. L \/ { ( F ` A ) , ( f ` A ) } e. L ) ) )
72 71 expimpd 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) -> ( ( { ( f ` A ) , ( f ` B ) } e. J /\ { ( f ` A ) , ( f ` B ) } C_ M ) -> ( { ( F ` A ) , ( f ` B ) } e. L \/ { ( F ` A ) , ( f ` A ) } e. L ) ) )
73 13 72 mpd 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) -> ( { ( F ` A ) , ( f ` B ) } e. L \/ { ( F ` A ) , ( f ` A ) } e. L ) )
74 8 73 jca 
 |-  ( ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) /\ ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) -> ( f : N -1-1-onto-> M /\ ( { ( F ` A ) , ( f ` B ) } e. L \/ { ( F ` A ) , ( f ` A ) } e. L ) ) )
75 74 ex 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> ( ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) -> ( f : N -1-1-onto-> M /\ ( { ( F ` A ) , ( f ` B ) } e. L \/ { ( F ` A ) , ( f ` A ) } e. L ) ) ) )
76 75 eximdv 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> ( E. f ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) -> E. f ( f : N -1-1-onto-> M /\ ( { ( F ` A ) , ( f ` B ) } e. L \/ { ( F ` A ) , ( f ` A ) } e. L ) ) ) )
77 7 76 mpd 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> E. f ( f : N -1-1-onto-> M /\ ( { ( F ` A ) , ( f ` B ) } e. L \/ { ( F ` A ) , ( f ` A ) } e. L ) ) )