Metamath Proof Explorer

Theorem hashnbusgrvd

Description: In a simple graph, the number of neighbors of a vertex is the degree of this vertex. This theorem does not hold for (simple) pseudographs, because a vertex connected with itself only by a loop has no neighbors, see uspgrloopnb0 , but degree 2, see uspgrloopvd2 . And it does not hold for multigraphs, because a vertex connected with only one other vertex by two edges has one neighbor, see umgr2v2enb1 , but also degree 2, see umgr2v2evd2 . (Contributed by Alexander van der Vekens, 17-Dec-2017) (Revised by AV, 15-Dec-2020) (Proof shortened by AV, 5-May-2021)

Ref Expression
Hypothesis hashnbusgrvd.v ⊢ V = Vtx ⁡ G
Assertion hashnbusgrvd ⊢ G ∈ USGraph ∧ U ∈ V → G NeighbVtx U = VtxDeg ⁡ G ⁡ U

Proof

Step Hyp Ref Expression
1 hashnbusgrvd.v ⊢ V = Vtx ⁡ G
2 eqid ⊢ Edg ⁡ G = Edg ⁡ G
3 1 2 nbedgusgr ⊢ G ∈ USGraph ∧ U ∈ V → G NeighbVtx U = e ∈ Edg ⁡ G | U ∈ e
4 eqid ⊢ VtxDeg ⁡ G = VtxDeg ⁡ G
5 1 2 4 vtxdusgrfvedg ⊢ G ∈ USGraph ∧ U ∈ V → VtxDeg ⁡ G ⁡ U = e ∈ Edg ⁡ G | U ∈ e
6 3 5 eqtr4d ⊢ G ∈ USGraph ∧ U ∈ V → G NeighbVtx U = VtxDeg ⁡ G ⁡ U