Theorem grimedgi

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

	Ref	Expression
Hypotheses	grimedg.v	|- V = ( Vtx ` G )
	grimedg.i	|- I = ( Edg ` G )
	grimedg.e	|- E = ( Edg ` H )
Assertion	grimedgi	|- ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( K e. I -> ( F " K ) e. E ) )

Proof

Step	Hyp	Ref	Expression
1		grimedg.v	|- V = ( Vtx ` G )
2		grimedg.i	|- I = ( Edg ` G )
3		grimedg.e	|- E = ( Edg ` H )
4	1 2 3	grimedg	|- ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( K e. I <-> ( ( F " K ) e. E /\ K C_ V ) ) )
5		simpl	|- ( ( ( F " K ) e. E /\ K C_ V ) -> ( F " K ) e. E )
6	4 5	biimtrdi	|- ( ( G e. UHGraph /\ H e. UHGraph /\ F e. ( G GraphIso H ) ) -> ( K e. I -> ( F " K ) e. E ) )