Theorem iedgedg

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

	Ref	Expression
Hypothesis	iedgedg.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
Assertion	iedgedg	$$⊢\left(\mathrm{Fun}E\wedge I\in \mathrm{dom}E\right)\to E\left(I\right)\in \mathrm{Edg}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		iedgedg.e	$$⊢E=\mathrm{iEdg}\left(G\right)$$
2		fvelrn	$$⊢\left(\mathrm{Fun}E\wedge I\in \mathrm{dom}E\right)\to E\left(I\right)\in \mathrm{ran}E$$
3		edgval	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{ran}\mathrm{iEdg}\left(G\right)$$
4	1	rneqi	$$⊢\mathrm{ran}E=\mathrm{ran}\mathrm{iEdg}\left(G\right)$$
5	3 4	eqtr4i	$$⊢\mathrm{Edg}\left(G\right)=\mathrm{ran}E$$
6	2 5	eleqtrrdi	$$⊢\left(\mathrm{Fun}E\wedge I\in \mathrm{dom}E\right)\to E\left(I\right)\in \mathrm{Edg}\left(G\right)$$