Metamath Proof Explorer


Theorem basvtxval

Description: The set of vertices of a graph represented as an extensible structure with the set of vertices as base set. (Contributed by AV, 14-Oct-2020) (Revised by AV, 12-Nov-2021)

Ref Expression
Hypotheses basvtxval.s φ G Struct X
basvtxval.d φ 2 dom G
basvtxval.v φ V Y
basvtxval.b φ Base ndx V G
Assertion basvtxval φ Vtx G = V

Proof

Step Hyp Ref Expression
1 basvtxval.s φ G Struct X
2 basvtxval.d φ 2 dom G
3 basvtxval.v φ V Y
4 basvtxval.b φ Base ndx V G
5 structn0fun G Struct X Fun G
6 1 5 syl φ Fun G
7 funvtxdmge2val Fun G 2 dom G Vtx G = Base G
8 6 2 7 syl2anc φ Vtx G = Base G
9 1 3 4 opelstrbas φ V = Base G
10 8 9 eqtr4d φ Vtx G = V