Theorem edgstruct

Description: The edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 13-Oct-2020)

	Ref	Expression
Hypothesis	edgstruct.s	|- G = { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. }
Assertion	edgstruct	|- ( ( V e. W /\ E e. X ) -> ( Edg ` G ) = ran E )

Proof

Step	Hyp	Ref	Expression
1		edgstruct.s	|- G = { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. }
2		edgval	|- ( Edg ` G ) = ran ( iEdg ` G )
3	1	struct2griedg	|- ( ( V e. W /\ E e. X ) -> ( iEdg ` G ) = E )
4	3	rneqd	|- ( ( V e. W /\ E e. X ) -> ran ( iEdg ` G ) = ran E )
5	2 4	syl5eq	|- ( ( V e. W /\ E e. X ) -> ( Edg ` G ) = ran E )