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=\mathrm{Vtx}\left(G\right)$$
	grlimprop.w	$$⊢W=\mathrm{Vtx}\left(H\right)$$
Assertion	grlimf1o	$$⊢F\in \left(G\mathrm{GraphLocIso}H\right)\to F:V\underset{1-1\; onto}{⟶}W$$

Proof

Step	Hyp	Ref	Expression
1		grlimprop.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		grlimprop.w	$$⊢W=\mathrm{Vtx}\left(H\right)$$
3	1 2	grlimprop	$$⊢F\in \left(G\mathrm{GraphLocIso}H\right)\to \left(F:V\underset{1-1\; onto}{⟶}W\wedge \forall v\in V\left(G\mathrm{ISubGr}\left(GClNeighbVtxv\right)\right){\simeq }_{𝑔𝑟}\left(H\mathrm{ISubGr}\left(HClNeighbVtxF\left(v\right)\right)\right)\right)$$
4	3	simpld	$$⊢F\in \left(G\mathrm{GraphLocIso}H\right)\to F:V\underset{1-1\; onto}{⟶}W$$