Description: The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. I. e. in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop ), the vertex connected with itself by the loop has degree 2. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 22-Dec-2017) (Revised by AV, 17-Dec-2020) (Proof shortened by AV, 21-Feb-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | uspgrloopvtx.g | |- G = <. V , { <. A , { N } >. } >. |
|
| Assertion | uspgrloopvd2 | |- ( ( V e. W /\ A e. X /\ N e. V ) -> ( ( VtxDeg ` G ) ` N ) = 2 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | uspgrloopvtx.g | |- G = <. V , { <. A , { N } >. } >. |
|
| 2 | 1 | uspgrloopvtx | |- ( V e. W -> ( Vtx ` G ) = V ) |
| 3 | 2 | 3ad2ant1 | |- ( ( V e. W /\ A e. X /\ N e. V ) -> ( Vtx ` G ) = V ) |
| 4 | simp2 | |- ( ( V e. W /\ A e. X /\ N e. V ) -> A e. X ) |
|
| 5 | simp3 | |- ( ( V e. W /\ A e. X /\ N e. V ) -> N e. V ) |
|
| 6 | 1 | uspgrloopiedg | |- ( ( V e. W /\ A e. X ) -> ( iEdg ` G ) = { <. A , { N } >. } ) |
| 7 | 6 | 3adant3 | |- ( ( V e. W /\ A e. X /\ N e. V ) -> ( iEdg ` G ) = { <. A , { N } >. } ) |
| 8 | 3 4 5 7 | 1loopgrvd2 | |- ( ( V e. W /\ A e. X /\ N e. V ) -> ( ( VtxDeg ` G ) ` N ) = 2 ) |