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	$$⊢\phi \to G\mathrm{Struct}X$$
	basvtxval.d	$$⊢\phi \to 2\le \left|\mathrm{dom}G\right|$$
	edgfiedgval.e	$$⊢\phi \to E\in Y$$
	edgfiedgval.f	$$⊢\phi \to ⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\in G$$
Assertion	edgfiedgval	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=E$$

Proof

Step	Hyp	Ref	Expression
1		basvtxval.s	$$⊢\phi \to G\mathrm{Struct}X$$
2		basvtxval.d	$$⊢\phi \to 2\le \left|\mathrm{dom}G\right|$$
3		edgfiedgval.e	$$⊢\phi \to E\in Y$$
4		edgfiedgval.f	$$⊢\phi \to ⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\in G$$
5		structn0fun	$$⊢G\mathrm{Struct}X\to \mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)$$
6	1 5	syl	$$⊢\phi \to \mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)$$
7		funiedgdmge2val	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge 2\le \left|\mathrm{dom}G\right|\right)\to \mathrm{iEdg}\left(G\right)=\mathrm{ef}\left(G\right)$$
8	6 2 7	syl2anc	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=\mathrm{ef}\left(G\right)$$
9		edgfid	$$⊢\mathrm{ef}=\mathrm{Slot}\mathrm{ef}\left(\mathrm{ndx}\right)$$
10		structex	$$⊢G\mathrm{Struct}X\to G\in \mathrm{V}$$
11	1 10	syl	$$⊢\phi \to G\in \mathrm{V}$$
12		structfung	$$⊢G\mathrm{Struct}X\to \mathrm{Fun}{G^{-1}}^{-1}$$
13	1 12	syl	$$⊢\phi \to \mathrm{Fun}{G^{-1}}^{-1}$$
14	9 11 13 4 3	strfv2d	$$⊢\phi \to E=\mathrm{ef}\left(G\right)$$
15	8 14	eqtr4d	$$⊢\phi \to \mathrm{iEdg}\left(G\right)=E$$