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

Metamath Proof Explorer

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 = Base ndx V ef ⁡ ndx E
Assertion struct2griedg ⊢ V ∈ X ∧ E ∈ Y → iEdg ⁡ G = E

Proof

Step Hyp Ref Expression
1 struct2grvtx.g ⊢ G = Base ndx V ef ⁡ ndx E
2 1 struct2grstr ⊢ G Struct Base ndx ef ⁡ ndx
3 2 a1i ⊢ V ∈ X ∧ E ∈ Y → G Struct Base ndx ef ⁡ ndx
4 simpl ⊢ V ∈ X ∧ E ∈ Y → V ∈ X
5 simpr ⊢ V ∈ X ∧ E ∈ Y → E ∈ Y
6 1 eqimss2i ⊢ Base ndx V ef ⁡ ndx E ⊆ G
7 6 a1i ⊢ V ∈ X ∧ E ∈ Y → Base ndx V ef ⁡ ndx E ⊆ G
8 3 4 5 7 structgrssiedg ⊢ V ∈ X ∧ E ∈ Y → iEdg ⁡ G = E