Theorem iedgedg

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

	Ref	Expression
Hypothesis	iedgedg.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
Assertion	iedgedg	⊢ ( ( Fun 𝐸 ∧ 𝐼 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐼 ) ∈ ( Edg ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		iedgedg.e	⊢ 𝐸 = ( iEdg ‘ 𝐺 )
2		fvelrn	⊢ ( ( Fun 𝐸 ∧ 𝐼 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐼 ) ∈ ran 𝐸 )
3		edgval	⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
4	1	rneqi	⊢ ran 𝐸 = ran ( iEdg ‘ 𝐺 )
5	3 4	eqtr4i	⊢ ( Edg ‘ 𝐺 ) = ran 𝐸
6	2 5	eleqtrrdi	⊢ ( ( Fun 𝐸 ∧ 𝐼 ∈ dom 𝐸 ) → ( 𝐸 ‘ 𝐼 ) ∈ ( Edg ‘ 𝐺 ) )