Theorem grilcbri

Description: Implications of two graphs being locally isomorphic. (Contributed by AV, 9-Jun-2025)

	Ref	Expression
Hypotheses	dfgrlic2.v	|- V = ( Vtx ` G )
	dfgrlic2.w	|- W = ( Vtx ` H )
Assertion	grilcbri	|- ( G ~=lgr H -> E. f ( f : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfgrlic2.v	|- V = ( Vtx ` G )
2		dfgrlic2.w	|- W = ( Vtx ` H )
3		grlicrcl	|- ( G ~=lgr H -> ( G e. _V /\ H e. _V ) )
4	1 2	dfgrlic2	|- ( ( G e. _V /\ H e. _V ) -> ( G ~=lgr H <-> E. f ( f : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) ) ) )
5	3 4	syl	|- ( G ~=lgr H -> ( G ~=lgr H <-> E. f ( f : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) ) ) )
6	5	ibi	|- ( G ~=lgr H -> E. f ( f : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( f ` v ) ) ) ) )