This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem grlimpredg

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 in H . (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 grlimpredg 
|- ( ( ( 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. J ) )

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 sseq1 
 |-  ( x = { ( f ` A ) , ( f ` B ) } -> ( x C_ M <-> { ( f ` A ) , ( f ` B ) } C_ M ) )
9 8 6 elrab2 
 |-  ( { ( f ` A ) , ( f ` B ) } e. L <-> ( { ( f ` A ) , ( f ` B ) } e. J /\ { ( f ` A ) , ( f ` B ) } C_ M ) )
10 simpl 
 |-  ( ( { ( f ` A ) , ( f ` B ) } e. J /\ { ( f ` A ) , ( f ` B ) } C_ M ) -> { ( f ` A ) , ( f ` B ) } e. J )
11 10 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. J /\ { ( f ` A ) , ( f ` B ) } C_ M ) -> { ( f ` A ) , ( f ` B ) } e. J ) )
12 9 11 biimtrid 
 |-  ( ( ( ( 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 ) )
13 12 imdistanda 
 |-  ( ( ( 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. J ) ) )
14 13 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. J ) ) )
15 7 14 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. J ) )