Theorem struct2griedg

Description: The set of indexed edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 23-Sep-2020) (Proof shortened by AV, 12-Nov-2021)

	Ref	Expression
Hypothesis	struct2grvtx.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\right\}$$
Assertion	struct2griedg	$$⊢\left(V\in X\wedge E\in Y\right)\to \mathrm{iEdg}\left(G\right)=E$$

Proof

Step	Hyp	Ref	Expression
1		struct2grvtx.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\right\}$$
2	1	struct2grstr	$$⊢G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)⟩$$
3	2	a1i	$$⊢\left(V\in X\wedge E\in Y\right)\to G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)⟩$$
4		simpl	$$⊢\left(V\in X\wedge E\in Y\right)\to V\in X$$
5		simpr	$$⊢\left(V\in X\wedge E\in Y\right)\to E\in Y$$
6	1	eqimss2i	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\right\}\subseteq G$$
7	6	a1i	$$⊢\left(V\in X\wedge E\in Y\right)\to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\right\}\subseteq G$$
8	3 4 5 7	structgrssiedg	$$⊢\left(V\in X\wedge E\in Y\right)\to \mathrm{iEdg}\left(G\right)=E$$