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

Metamath Proof Explorer

Theorem clnbgrisubgrgrim

Description: Isomorphic subgraphs induced by closed neighborhoods of vertices of two graphs. (Contributed by AV, 29-May-2025)

Ref Expression
Hypotheses clnbgrisubgrgrim.i 
|- I = ( iEdg ` G )
clnbgrisubgrgrim.j 
|- J = ( iEdg ` H )
clnbgrisubgrgrim.n 
|- N = ( G ClNeighbVtx X )
clnbgrisubgrgrim.m 
|- M = ( H ClNeighbVtx Y )
clnbgrisubgrgrim.k 
|- K = { x e. dom I | ( I ` x ) C_ N }
clnbgrisubgrgrim.l 
|- L = { x e. dom J | ( J ` x ) C_ M }
Assertion clnbgrisubgrgrim 
|- ( ( G e. U /\ H e. T ) -> ( ( G ISubGr N ) ~=gr ( H ISubGr M ) <-> E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 clnbgrisubgrgrim.i 
 |-  I = ( iEdg ` G )
2 clnbgrisubgrgrim.j 
 |-  J = ( iEdg ` H )
3 clnbgrisubgrgrim.n 
 |-  N = ( G ClNeighbVtx X )
4 clnbgrisubgrgrim.m 
 |-  M = ( H ClNeighbVtx Y )
5 clnbgrisubgrgrim.k 
 |-  K = { x e. dom I | ( I ` x ) C_ N }
6 clnbgrisubgrgrim.l 
 |-  L = { x e. dom J | ( J ` x ) C_ M }
7 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
8 7 clnbgrssvtx 
 |-  ( G ClNeighbVtx X ) C_ ( Vtx ` G )
9 3 8 eqsstri 
 |-  N C_ ( Vtx ` G )
10 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
11 10 clnbgrssvtx 
 |-  ( H ClNeighbVtx Y ) C_ ( Vtx ` H )
12 4 11 eqsstri 
 |-  M C_ ( Vtx ` H )
13 7 10 1 2 5 6 isubgrgrim 
 |-  ( ( ( G e. U /\ H e. T ) /\ ( N C_ ( Vtx ` G ) /\ M C_ ( Vtx ` H ) ) ) -> ( ( G ISubGr N ) ~=gr ( H ISubGr M ) <-> E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )
14 9 12 13 mpanr12 
 |-  ( ( G e. U /\ H e. T ) -> ( ( G ISubGr N ) ~=gr ( H ISubGr M ) <-> E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( f " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) )