Theorem grimf1o

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

	Ref	Expression
Hypotheses	grimprop.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	grimprop.w	⊢ 𝑊 = ( Vtx ‘ 𝐻 )
Assertion	grimf1o	⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )

Proof

Step	Hyp	Ref	Expression
1		grimprop.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		grimprop.w	⊢ 𝑊 = ( Vtx ‘ 𝐻 )
3		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
4		eqid	⊢ ( iEdg ‘ 𝐻 ) = ( iEdg ‘ 𝐻 )
5	1 2 3 4	grimprop	⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → ( 𝐹 : 𝑉 –1-1-onto→ 𝑊 ∧ ∃ 𝑗 ( 𝑗 : dom ( iEdg ‘ 𝐺 ) –1-1-onto→ dom ( iEdg ‘ 𝐻 ) ∧ ∀ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) ( ( iEdg ‘ 𝐻 ) ‘ ( 𝑗 ‘ 𝑖 ) ) = ( 𝐹 “ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) ) ) )
6	5	simpld	⊢ ( 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) → 𝐹 : 𝑉 –1-1-onto→ 𝑊 )