dfgrlic3

Description: Alternate, explicit definition of the "is locally isomorphic to" relation for two graphs. (Contributed by AV, 9-Jun-2025)

	Ref	Expression
Hypotheses	dfgrlic2.v	\|- V = ( Vtx ` G )
	dfgrlic2.w	\|- W = ( Vtx ` H )
	dfgrlic3.i	\|- I = ( iEdg ` G )
	dfgrlic3.j	\|- J = ( iEdg ` H )
	dfgrlic3.n	\|- N = ( G ClNeighbVtx v )
	dfgrlic3.m	\|- M = ( H ClNeighbVtx ( f ` v ) )
	dfgrlic3.k	\|- K = { x e. dom I \| ( I ` x ) C_ N }
	dfgrlic3.l	\|- L = { x e. dom J \| ( J ` x ) C_ M }
Assertion	dfgrlic3	\|- ( ( G e. X /\ H e. Y ) -> ( G ~=lgr H <-> E. f ( f : V -1-1-onto-> W /\ A. v e. V E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )

Step	Hyp	Ref	Expression
1		dfgrlic2.v	\|- V = ( Vtx ` G )
2		dfgrlic2.w	\|- W = ( Vtx ` H )
3		dfgrlic3.i	\|- I = ( iEdg ` G )
4		dfgrlic3.j	\|- J = ( iEdg ` H )
5		dfgrlic3.n	\|- N = ( G ClNeighbVtx v )
6		dfgrlic3.m	\|- M = ( H ClNeighbVtx ( f ` v ) )
7		dfgrlic3.k	\|- K = { x e. dom I \| ( I ` x ) C_ N }
8		dfgrlic3.l	\|- L = { x e. dom J \| ( J ` x ) C_ M }
9		brgrlic	\|- ( G ~=lgr H <-> ( G GraphLocIso H ) =/= (/) )
10		n0	\|- ( ( G GraphLocIso H ) =/= (/) <-> E. f f e. ( G GraphLocIso H ) )
11	9 10	bitri	\|- ( G ~=lgr H <-> E. f f e. ( G GraphLocIso H ) )
12	1 2 5 6 3 4 7 8	isgrlim2	\|- ( ( G e. X /\ H e. Y /\ f e. _V ) -> ( f e. ( G GraphLocIso H ) <-> ( f : V -1-1-onto-> W /\ A. v e. V E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )
13	12	el3v3	\|- ( ( G e. X /\ H e. Y ) -> ( f e. ( G GraphLocIso H ) <-> ( f : V -1-1-onto-> W /\ A. v e. V E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )
14	13	exbidv	\|- ( ( G e. X /\ H e. Y ) -> ( E. f f e. ( G GraphLocIso H ) <-> E. f ( f : V -1-1-onto-> W /\ A. v e. V E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )
15	11 14	bitrid	\|- ( ( G e. X /\ H e. Y ) -> ( G ~=lgr H <-> E. f ( f : V -1-1-onto-> W /\ A. v e. V E. j ( j : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. i e. K ( j " ( I ` i ) ) = ( J ` ( g ` i ) ) ) ) ) ) )

Metamath Proof Explorer