Metamath Proof Explorer
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 |
|
|
|
usgrexmpl.e |
|
|
|
usgrexmpl.g |
|
|
Assertion |
usgrexmplvtx |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
usgrexmpl.v |
|
2 |
|
usgrexmpl.e |
|
3 |
|
usgrexmpl.g |
|
4 |
1 2 3
|
usgrexmpllem |
|
5 |
|
id |
|
6 |
|
fz0to4untppr |
|
7 |
1 6
|
eqtri |
|
8 |
5 7
|
eqtrdi |
|
9 |
8
|
adantr |
|
10 |
4 9
|
ax-mp |
|