Theorem iedgedg

Description: An indexed edge is an edge. (Contributed by AV, 19-Dec-2021)

	Ref	Expression
Hypothesis	iedgedg.e	|- E = ( iEdg ` G )
Assertion	iedgedg	|- ( ( Fun E /\ I e. dom E ) -> ( E ` I ) e. ( Edg ` G ) )

Proof

Step	Hyp	Ref	Expression
1		iedgedg.e	|- E = ( iEdg ` G )
2		fvelrn	|- ( ( Fun E /\ I e. dom E ) -> ( E ` I ) e. ran E )
3		edgval	|- ( Edg ` G ) = ran ( iEdg ` G )
4	1	rneqi	|- ran E = ran ( iEdg ` G )
5	3 4	eqtr4i	|- ( Edg ` G ) = ran E
6	2 5	eleqtrrdi	|- ( ( Fun E /\ I e. dom E ) -> ( E ` I ) e. ( Edg ` G ) )