Theorem grimedgi

Description: Graph isomorphisms map edges onto the corresponding edges. (Contributed by AV, 30-Dec-2025)

	Ref	Expression
Hypotheses	grimedg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	grimedg.i	⊢ 𝐼 = ( Edg ‘ 𝐺 )
	grimedg.e	⊢ 𝐸 = ( Edg ‘ 𝐻 )
Assertion	grimedgi	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐾 ∈ 𝐼 → ( 𝐹 “ 𝐾 ) ∈ 𝐸 ) )

Proof

Step	Hyp	Ref	Expression
1		grimedg.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		grimedg.i	⊢ 𝐼 = ( Edg ‘ 𝐺 )
3		grimedg.e	⊢ 𝐸 = ( Edg ‘ 𝐻 )
4	1 2 3	grimedg	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐾 ∈ 𝐼 ↔ ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) ) )
5		simpl	⊢ ( ( ( 𝐹 “ 𝐾 ) ∈ 𝐸 ∧ 𝐾 ⊆ 𝑉 ) → ( 𝐹 “ 𝐾 ) ∈ 𝐸 )
6	4 5	biimtrdi	⊢ ( ( 𝐺 ∈ UHGraph ∧ 𝐻 ∈ UHGraph ∧ 𝐹 ∈ ( 𝐺 GraphIso 𝐻 ) ) → ( 𝐾 ∈ 𝐼 → ( 𝐹 “ 𝐾 ) ∈ 𝐸 ) )