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 = ( Vtx ` G )
	grimprop.w	|- W = ( Vtx ` H )
Assertion	grimf1o	|- ( F e. ( G GraphIso H ) -> F : V -1-1-onto-> W )

Proof

Step	Hyp	Ref	Expression
1		grimprop.v	|- V = ( Vtx ` G )
2		grimprop.w	|- W = ( Vtx ` H )
3		eqid	|- ( iEdg ` G ) = ( iEdg ` G )
4		eqid	|- ( iEdg ` H ) = ( iEdg ` H )
5	1 2 3 4	grimprop	|- ( F e. ( G GraphIso H ) -> ( F : V -1-1-onto-> W /\ E. j ( j : dom ( iEdg ` G ) -1-1-onto-> dom ( iEdg ` H ) /\ A. i e. dom ( iEdg ` G ) ( ( iEdg ` H ) ` ( j ` i ) ) = ( F " ( ( iEdg ` G ) ` i ) ) ) ) )
6	5	simpld	|- ( F e. ( G GraphIso H ) -> F : V -1-1-onto-> W )