Theorem edgfiedgval

Description: The set of indexed edges of a graph represented as an extensible structure with the indexed edges in the slot for edge functions. (Contributed by AV, 14-Oct-2020) (Revised by AV, 12-Nov-2021)

	Ref	Expression
Hypotheses	basvtxval.s	|- ( ph -> G Struct X )
	basvtxval.d	|- ( ph -> 2 <_ ( # ` dom G ) )
	edgfiedgval.e	|- ( ph -> E e. Y )
	edgfiedgval.f	|- ( ph -> <. ( .ef ` ndx ) , E >. e. G )
Assertion	edgfiedgval	|- ( ph -> ( iEdg ` G ) = E )

Proof

Step	Hyp	Ref	Expression
1		basvtxval.s	|- ( ph -> G Struct X )
2		basvtxval.d	|- ( ph -> 2 <_ ( # ` dom G ) )
3		edgfiedgval.e	|- ( ph -> E e. Y )
4		edgfiedgval.f	|- ( ph -> <. ( .ef ` ndx ) , E >. e. G )
5		structn0fun	|- ( G Struct X -> Fun ( G \ { (/) } ) )
6	1 5	syl	|- ( ph -> Fun ( G \ { (/) } ) )
7		funiedgdmge2val	|- ( ( Fun ( G \ { (/) } ) /\ 2 <_ ( # ` dom G ) ) -> ( iEdg ` G ) = ( .ef ` G ) )
8	6 2 7	syl2anc	|- ( ph -> ( iEdg ` G ) = ( .ef ` G ) )
9		edgfid	|- .ef = Slot ( .ef ` ndx )
10		structex	|- ( G Struct X -> G e. _V )
11	1 10	syl	|- ( ph -> G e. _V )
12		structfung	|- ( G Struct X -> Fun `' `' G )
13	1 12	syl	|- ( ph -> Fun `' `' G )
14	9 11 13 4 3	strfv2d	|- ( ph -> E = ( .ef ` G ) )
15	8 14	eqtr4d	|- ( ph -> ( iEdg ` G ) = E )