Theorem usgrlimprop

Description: Properties of a local isomorphism of simple pseudographs. (Contributed by AV, 17-Aug-2025)

	Ref	Expression
Hypotheses	usgrlimprop.v	|- V = ( Vtx ` G )
	usgrlimprop.w	|- W = ( Vtx ` H )
	usgrlimprop.n	|- N = ( G ClNeighbVtx v )
	usgrlimprop.m	|- M = ( H ClNeighbVtx ( F ` v ) )
	usgrlimprop.i	|- I = ( Edg ` G )
	usgrlimprop.j	|- J = ( Edg ` H )
	usgrlimprop.k	|- K = { x e. I | x C_ N }
	usgrlimprop.l	|- L = { x e. J | x C_ M }
Assertion	usgrlimprop	|- ( ( G e. USPGraph /\ H e. USPGraph /\ F e. ( G GraphLocIso H ) ) -> ( F : V -1-1-onto-> W /\ A. v e. V E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		usgrlimprop.v	|- V = ( Vtx ` G )
2		usgrlimprop.w	|- W = ( Vtx ` H )
3		usgrlimprop.n	|- N = ( G ClNeighbVtx v )
4		usgrlimprop.m	|- M = ( H ClNeighbVtx ( F ` v ) )
5		usgrlimprop.i	|- I = ( Edg ` G )
6		usgrlimprop.j	|- J = ( Edg ` H )
7		usgrlimprop.k	|- K = { x e. I | x C_ N }
8		usgrlimprop.l	|- L = { x e. J | x C_ M }
9		simp3	|- ( ( G e. USPGraph /\ H e. USPGraph /\ F e. ( G GraphLocIso H ) ) -> F e. ( G GraphLocIso H ) )
10	1 2 3 4 5 6 7 8	uspgrlim	|- ( ( G e. USPGraph /\ H e. USPGraph /\ F e. ( G GraphLocIso H ) ) -> ( F e. ( G GraphLocIso H ) <-> ( F : V -1-1-onto-> W /\ A. v e. V E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) ) ) )
11	9 10	mpbid	|- ( ( G e. USPGraph /\ H e. USPGraph /\ F e. ( G GraphLocIso H ) ) -> ( F : V -1-1-onto-> W /\ A. v e. V E. f ( f : N -1-1-onto-> M /\ E. g ( g : K -1-1-onto-> L /\ A. e e. K ( f " e ) = ( g ` e ) ) ) ) )