Theorem structgrssiedg

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, 14-Oct-2020) (Proof shortened by AV, 12-Nov-2021)

	Ref	Expression
Hypotheses	structgrssvtx.g	|- ( ph -> G Struct X )
	structgrssvtx.v	|- ( ph -> V e. Y )
	structgrssvtx.e	|- ( ph -> E e. Z )
	structgrssvtx.s	|- ( ph -> { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G )
Assertion	structgrssiedg	|- ( ph -> ( iEdg ` G ) = E )

Proof

Step	Hyp	Ref	Expression
1		structgrssvtx.g	|- ( ph -> G Struct X )
2		structgrssvtx.v	|- ( ph -> V e. Y )
3		structgrssvtx.e	|- ( ph -> E e. Z )
4		structgrssvtx.s	|- ( ph -> { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G )
5	1 2 3 4	structgrssvtxlem	|- ( ph -> 2 <_ ( # ` dom G ) )
6		opex	|- <. ( Base ` ndx ) , V >. e. _V
7		opex	|- <. ( .ef ` ndx ) , E >. e. _V
8	6 7	prss	|- ( ( <. ( Base ` ndx ) , V >. e. G /\ <. ( .ef ` ndx ) , E >. e. G ) <-> { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G )
9		simpr	|- ( ( <. ( Base ` ndx ) , V >. e. G /\ <. ( .ef ` ndx ) , E >. e. G ) -> <. ( .ef ` ndx ) , E >. e. G )
10	8 9	sylbir	|- ( { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } C_ G -> <. ( .ef ` ndx ) , E >. e. G )
11	4 10	syl	|- ( ph -> <. ( .ef ` ndx ) , E >. e. G )
12	1 5 3 11	edgfiedgval	|- ( ph -> ( iEdg ` G ) = E )