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 e. X /\ E e. Y ) -> ( Vtx ` G ) = V ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | struct2grvtx.g | |- G = { <. ( Base ` ndx ) , V >. , <. ( .ef ` ndx ) , E >. } |
|
2 | edgfndxnn | |- ( .ef ` ndx ) e. NN |
|
3 | baseltedgf | |- ( Base ` ndx ) < ( .ef ` ndx ) |
|
4 | 2 3 1 | structvtxval | |- ( ( V e. X /\ E e. Y ) -> ( Vtx ` G ) = V ) |