Theorem grlimf1o

Description: A local isomorphism of graphs is a bijection between their vertices. (Contributed by AV, 21-May-2025)

	Ref	Expression
Hypotheses	grlimprop.v	|- V = ( Vtx ` G )
	grlimprop.w	|- W = ( Vtx ` H )
Assertion	grlimf1o	|- ( F e. ( G GraphLocIso H ) -> F : V -1-1-onto-> W )

Proof

Step	Hyp	Ref	Expression
1		grlimprop.v	|- V = ( Vtx ` G )
2		grlimprop.w	|- W = ( Vtx ` H )
3	1 2	grlimprop	|- ( F e. ( G GraphLocIso H ) -> ( F : V -1-1-onto-> W /\ A. v e. V ( G ISubGr ( G ClNeighbVtx v ) ) ~=gr ( H ISubGr ( H ClNeighbVtx ( F ` v ) ) ) ) )
4	3	simpld	|- ( F e. ( G GraphLocIso H ) -> F : V -1-1-onto-> W )