Metamath Proof Explorer


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 φ G Struct X
structgrssvtx.v φ V Y
structgrssvtx.e φ E Z
structgrssvtx.s φ Base ndx V ef ndx E G
Assertion structgrssiedg φ iEdg G = E

Proof

Step Hyp Ref Expression
1 structgrssvtx.g φ G Struct X
2 structgrssvtx.v φ V Y
3 structgrssvtx.e φ E Z
4 structgrssvtx.s φ Base ndx V ef ndx E G
5 1 2 3 4 structgrssvtxlem φ 2 dom G
6 opex Base ndx V V
7 opex ef ndx E V
8 6 7 prss Base ndx V G ef ndx E G Base ndx V ef ndx E G
9 simpr Base ndx V G ef ndx E G ef ndx E G
10 8 9 sylbir Base ndx V ef ndx E G ef ndx E G
11 4 10 syl φ ef ndx E G
12 1 5 3 11 edgfiedgval φ iEdg G = E