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 
|- 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 grlimprclnbgr 
|- ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> E. f E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) )

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 simp3 
 |-  ( ( A e. V /\ B e. W /\ { A , B } e. I ) -> { A , B } e. I )
8 prid1g 
 |-  ( A e. V -> A e. { A , B } )
9 8 3ad2ant1 
 |-  ( ( A e. V /\ B e. W /\ { A , B } e. I ) -> A e. { A , B } )
10 7 9 jca 
 |-  ( ( A e. V /\ B e. W /\ { A , B } e. I ) -> ( { A , B } e. I /\ A e. { A , B } ) )
11 1 2 3 4 5 6 grlimedgclnbgr 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( { A , B } e. I /\ A e. { A , B } ) ) -> E. f E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ ( f " { A , B } ) = ( g ` { A , B } ) ) )
12 10 11 syl3an3 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> E. f E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ ( f " { A , B } ) = ( g ` { A , B } ) ) )
13 simpr1 
 |-  ( ( ( ( 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 /\ g : K -1-1-onto-> L /\ ( f " { A , B } ) = ( g ` { A , B } ) ) ) -> f : N -1-1-onto-> M )
14 simpr2 
 |-  ( ( ( ( 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 /\ g : K -1-1-onto-> L /\ ( f " { A , B } ) = ( g ` { A , B } ) ) ) -> g : K -1-1-onto-> L )
15 f1ofn 
 |-  ( f : N -1-1-onto-> M -> f Fn N )
16 15 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 Fn N )
17 uspgruhgr 
 |-  ( G e. USPGraph -> G e. UHGraph )
18 17 adantr 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> G e. UHGraph )
19 18 3ad2ant1 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> G e. UHGraph )
20 2 eleq2i 
 |-  ( { A , B } e. I <-> { A , B } e. ( Edg ` G ) )
21 20 biimpi 
 |-  ( { A , B } e. I -> { A , B } e. ( Edg ` G ) )
22 21 3ad2ant3 
 |-  ( ( A e. V /\ B e. W /\ { A , B } e. I ) -> { A , B } e. ( Edg ` G ) )
23 22 3ad2ant3 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> { A , B } e. ( Edg ` G ) )
24 9 3ad2ant3 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> A e. { A , B } )
25 uhgredgrnv 
 |-  ( ( G e. UHGraph /\ { A , B } e. ( Edg ` G ) /\ A e. { A , B } ) -> A e. ( Vtx ` G ) )
26 19 23 24 25 syl3anc 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> A e. ( Vtx ` G ) )
27 26 adantr 
 |-  ( ( ( ( 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 ) -> A e. ( Vtx ` G ) )
28 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
29 28 clnbgrvtxel 
 |-  ( A e. ( Vtx ` G ) -> A e. ( G ClNeighbVtx A ) )
30 27 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 ) -> A e. ( G ClNeighbVtx A ) )
31 30 1 eleqtrrdi 
 |-  ( ( ( ( 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 ) -> A e. N )
32 prcom 
 |-  { A , B } = { B , A }
33 32 eleq1i 
 |-  ( { A , B } e. I <-> { B , A } e. I )
34 33 biimpi 
 |-  ( { A , B } e. I -> { B , A } e. I )
35 34 3ad2ant3 
 |-  ( ( A e. V /\ B e. W /\ { A , B } e. I ) -> { B , A } e. I )
36 35 3ad2ant3 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> { B , A } e. I )
37 36 adantr 
 |-  ( ( ( ( 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 ) -> { B , A } e. I )
38 37 olcd 
 |-  ( ( ( ( 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 ) -> ( B = A \/ { B , A } e. I ) )
39 uspgrupgr 
 |-  ( G e. USPGraph -> G e. UPGraph )
40 39 adantr 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> G e. UPGraph )
41 40 3ad2ant1 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> G e. UPGraph )
42 prid2g 
 |-  ( B e. W -> B e. { A , B } )
43 42 3ad2ant2 
 |-  ( ( A e. V /\ B e. W /\ { A , B } e. I ) -> B e. { A , B } )
44 43 3ad2ant3 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> B e. { A , B } )
45 uhgredgrnv 
 |-  ( ( G e. UHGraph /\ { A , B } e. ( Edg ` G ) /\ B e. { A , B } ) -> B e. ( Vtx ` G ) )
46 19 23 44 45 syl3anc 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> B e. ( Vtx ` G ) )
47 41 26 46 3jca 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> ( G e. UPGraph /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) )
48 47 adantr 
 |-  ( ( ( ( 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 ) -> ( G e. UPGraph /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) )
49 28 2 clnbupgrel 
 |-  ( ( G e. UPGraph /\ A e. ( Vtx ` G ) /\ B e. ( Vtx ` G ) ) -> ( B e. ( G ClNeighbVtx A ) <-> ( B = A \/ { B , A } e. I ) ) )
50 48 49 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 ) -> ( B e. ( G ClNeighbVtx A ) <-> ( B = A \/ { B , A } e. I ) ) )
51 38 50 mpbird 
 |-  ( ( ( ( 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 ) -> B e. ( G ClNeighbVtx A ) )
52 51 1 eleqtrrdi 
 |-  ( ( ( ( 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 ) -> B e. N )
53 fnimapr 
 |-  ( ( f Fn N /\ A e. N /\ B e. N ) -> ( f " { A , B } ) = { ( f ` A ) , ( f ` B ) } )
54 16 31 52 53 syl3anc 
 |-  ( ( ( ( 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 , B } ) = { ( f ` A ) , ( f ` B ) } )
55 54 eqeq1d 
 |-  ( ( ( ( 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 , B } ) = ( g ` { A , B } ) <-> { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) )
56 55 biimpd 
 |-  ( ( ( ( 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 , B } ) = ( g ` { A , B } ) -> { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) )
57 56 a1d 
 |-  ( ( ( ( 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 ) -> ( g : K -1-1-onto-> L -> ( ( f " { A , B } ) = ( g ` { A , B } ) -> { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) ) )
58 57 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 -> ( g : K -1-1-onto-> L -> ( ( f " { A , B } ) = ( g ` { A , B } ) -> { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) ) ) )
59 58 3imp2 
 |-  ( ( ( ( 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 /\ g : K -1-1-onto-> L /\ ( f " { A , B } ) = ( g ` { A , B } ) ) ) -> { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) )
60 13 14 59 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 /\ g : K -1-1-onto-> L /\ ( f " { A , B } ) = ( g ` { A , B } ) ) ) -> ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) )
61 60 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 /\ g : K -1-1-onto-> L /\ ( f " { A , B } ) = ( g ` { A , B } ) ) -> ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) ) )
62 61 2eximdv 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> ( E. f E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ ( f " { A , B } ) = ( g ` { A , B } ) ) -> E. f E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) ) )
63 12 62 mpd 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> E. f E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) )