Theorem grimf1o

Description: An isomorphism of graphs is a bijection between their vertices. (Contributed by AV, 29-Apr-2025)

	Ref	Expression
Hypotheses	grimprop.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
	grimprop.w	$$⊢W=\mathrm{Vtx}\left(H\right)$$
Assertion	grimf1o	$$⊢F\in \left(G\mathrm{GraphIso}H\right)\to F:V\underset{1-1\; onto}{⟶}W$$

Proof

Step	Hyp	Ref	Expression
1		grimprop.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		grimprop.w	$$⊢W=\mathrm{Vtx}\left(H\right)$$
3		eqid	$$⊢\mathrm{iEdg}\left(G\right)=\mathrm{iEdg}\left(G\right)$$
4		eqid	$$⊢\mathrm{iEdg}\left(H\right)=\mathrm{iEdg}\left(H\right)$$
5	1 2 3 4	grimprop	$$⊢F\in \left(G\mathrm{GraphIso}H\right)\to \left(F:V\underset{1-1\; onto}{⟶}W\wedge \exists j\left(j:\mathrm{dom}\mathrm{iEdg}\left(G\right)\underset{1-1\; onto}{⟶}\mathrm{dom}\mathrm{iEdg}\left(H\right)\wedge \forall i\in \mathrm{dom}\mathrm{iEdg}\left(G\right)\mathrm{iEdg}\left(H\right)\left(j\left(i\right)\right)=F\left[\mathrm{iEdg}\left(G\right)\left(i\right)\right]\right)\right)$$
6	5	simpld	$$⊢F\in \left(G\mathrm{GraphIso}H\right)\to F:V\underset{1-1\; onto}{⟶}W$$