Metamath Proof Explorer


Theorem usgrexmplvtx

Description: The vertices 0 , 1 , 2 , 3 , 4 of the graph G = <. V , E >. . (Contributed by AV, 12-Jan-2020) (Revised by AV, 21-Oct-2020)

Ref Expression
Hypotheses usgrexmpl.v V = 0 4
usgrexmpl.e E = ⟨“ 0 1 1 2 2 0 0 3 ”⟩
usgrexmpl.g G = V E
Assertion usgrexmplvtx Vtx G = 0 1 2 3 4

Proof

Step Hyp Ref Expression
1 usgrexmpl.v V = 0 4
2 usgrexmpl.e E = ⟨“ 0 1 1 2 2 0 0 3 ”⟩
3 usgrexmpl.g G = V E
4 1 2 3 usgrexmpllem Vtx G = V iEdg G = E
5 id Vtx G = V Vtx G = V
6 fz0to4untppr 0 4 = 0 1 2 3 4
7 1 6 eqtri V = 0 1 2 3 4
8 5 7 eqtrdi Vtx G = V Vtx G = 0 1 2 3 4
9 8 adantr Vtx G = V iEdg G = E Vtx G = 0 1 2 3 4
10 4 9 ax-mp Vtx G = 0 1 2 3 4