This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem edgstruct

Description: The edges of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 13-Oct-2020)

Ref Expression
Hypothesis edgstruct.s ⊢ G = Base ndx V ef ⁡ ndx E
Assertion edgstruct ⊢ V ∈ W ∧ E ∈ X → Edg ⁡ G = ran ⁡ E

Proof

Step Hyp Ref Expression
1 edgstruct.s ⊢ G = Base ndx V ef ⁡ ndx E
2 edgval ⊢ Edg ⁡ G = ran ⁡ iEdg ⁡ G
3 1 struct2griedg ⊢ V ∈ W ∧ E ∈ X → iEdg ⁡ G = E
4 3 rneqd ⊢ V ∈ W ∧ E ∈ X → ran ⁡ iEdg ⁡ G = ran ⁡ E
5 2 4 eqtrid ⊢ V ∈ W ∧ E ∈ X → Edg ⁡ G = ran ⁡ E