Metamath Proof Explorer


Theorem uspgrloopvd2

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 𝐺 = ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩
Assertion uspgrloopvd2 ( ( 𝑉𝑊𝐴𝑋𝑁𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = 2 )

Proof

Step Hyp Ref Expression
1 uspgrloopvtx.g 𝐺 = ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩
2 1 uspgrloopvtx ( 𝑉𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 )
3 2 3ad2ant1 ( ( 𝑉𝑊𝐴𝑋𝑁𝑉 ) → ( Vtx ‘ 𝐺 ) = 𝑉 )
4 simp2 ( ( 𝑉𝑊𝐴𝑋𝑁𝑉 ) → 𝐴𝑋 )
5 simp3 ( ( 𝑉𝑊𝐴𝑋𝑁𝑉 ) → 𝑁𝑉 )
6 1 uspgrloopiedg ( ( 𝑉𝑊𝐴𝑋 ) → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
7 6 3adant3 ( ( 𝑉𝑊𝐴𝑋𝑁𝑉 ) → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
8 3 4 5 7 1loopgrvd2 ( ( 𝑉𝑊𝐴𝑋𝑁𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = 2 )