This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database GRAPH THEORY Vertices and edges Vertices and indexed edges The vertices and edges of a graph represented as extensible structure struct2grstr
Description: A graph represented as an extensible structure with vertices as base set
and indexed edges is actually an extensible structure. (Contributed by AV , 23-Nov-2020)
Ref
Expression
Hypothesis
struct2grvtx.g ⊢ G = Base ndx V ef ndx E
Assertion
struct2grstr ⊢ G Struct Base ndx ef ndx
Proof
Step
Hyp
Ref
Expression
1
struct2grvtx.g ⊢ G = Base ndx V ef ndx E
2
basendxltedgfndx ⊢ Base ndx < ef ndx
3
edgfndxnn ⊢ ef ndx ∈ ℕ
4
1 2 3
2strstr ⊢ G Struct Base ndx ef ndx