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

Metamath Proof Explorer

Theorem struct2grvtx

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

Ref Expression
Hypothesis struct2grvtx.g ⊢ G = Base ndx V ef ⁡ ndx E
Assertion struct2grvtx ⊢ V ∈ X ∧ E ∈ Y → Vtx ⁡ G = V

Proof

Step Hyp Ref Expression
1 struct2grvtx.g ⊢ G = Base ndx V ef ⁡ ndx E
2 edgfndxnn ⊢ ef ⁡ ndx ∈ ℕ
3 basendxltedgfndx ⊢ Base ndx < ef ⁡ ndx
4 2 3 1 structvtxval ⊢ V ∈ X ∧ E ∈ Y → Vtx ⁡ G = V