Metamath Proof Explorer

Theorem grlimprclnbgredg

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 . (Contributed by AV, 27-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 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 ) )

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 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 } ) ) )
8 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 ) , ( f ` B ) } = ( g ` { A , B } ) ) ) -> f : N -1-1-onto-> M )
9 f1of 
 |-  ( g : K -1-1-onto-> L -> g : K --> L )
10 9 3ad2ant2 
 |-  ( ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) -> g : K --> L )
11 10 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 /\ g : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) ) -> g : K --> L )
12 uspgruhgr 
 |-  ( G e. USPGraph -> G e. UHGraph )
13 12 adantr 
 |-  ( ( G e. USPGraph /\ H e. USPGraph ) -> G e. UHGraph )
14 13 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 )
15 simp33 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> { A , B } e. I )
16 prid1g 
 |-  ( A e. V -> A e. { A , B } )
17 16 3ad2ant1 
 |-  ( ( A e. V /\ B e. W /\ { A , B } e. I ) -> A e. { A , B } )
18 17 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 } )
19 14 15 18 3jca 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> ( G e. UHGraph /\ { A , B } e. I /\ A e. { A , B } ) )
20 19 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 : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) ) -> ( G e. UHGraph /\ { A , B } e. I /\ A e. { A , B } ) )
21 1 2 3 clnbgrvtxedg 
 |-  ( ( G e. UHGraph /\ { A , B } e. I /\ A e. { A , B } ) -> { A , B } e. K )
22 20 21 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 /\ g : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) ) -> { A , B } e. K )
23 11 22 ffvelcdmd 
 |-  ( ( ( ( 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 ) , ( f ` B ) } = ( g ` { A , B } ) ) ) -> ( g ` { A , B } ) e. L )
24 eleq1 
 |-  ( { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) -> ( { ( f ` A ) , ( f ` B ) } e. L <-> ( g ` { A , B } ) e. L ) )
25 24 3ad2ant3 
 |-  ( ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) -> ( { ( f ` A ) , ( f ` B ) } e. L <-> ( g ` { A , B } ) e. L ) )
26 25 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 /\ g : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) ) -> ( { ( f ` A ) , ( f ` B ) } e. L <-> ( g ` { A , B } ) e. L ) )
27 23 26 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 /\ g : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) ) -> { ( f ` A ) , ( f ` B ) } e. L )
28 8 27 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 /\ g : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) ) -> ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) )
29 28 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 ) , ( f ` B ) } = ( g ` { A , B } ) ) -> ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) )
30 29 exlimdv 
 |-  ( ( ( G e. USPGraph /\ H e. USPGraph ) /\ F e. ( G GraphLocIso H ) /\ ( A e. V /\ B e. W /\ { A , B } e. I ) ) -> ( E. g ( f : N -1-1-onto-> M /\ g : K -1-1-onto-> L /\ { ( f ` A ) , ( f ` B ) } = ( g ` { A , B } ) ) -> ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) )
31 30 eximdv 
 |-  ( ( ( 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 } ) ) -> E. f ( f : N -1-1-onto-> M /\ { ( f ` A ) , ( f ` B ) } e. L ) ) )
32 7 31 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 ) )