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 ) ) ) ) ) )