This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| Assertion | hashnbusgrvd | ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hashnbusgrvd.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| 2 | eqid | ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 ) | |
| 3 | 1 2 | nbedgusgr | ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑈 ∈ 𝑒 } ) ) |
| 4 | eqid | ⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 ) | |
| 5 | 1 2 4 | vtxdusgrfvedg | ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) = ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑈 ∈ 𝑒 } ) ) |
| 6 | 3 5 | eqtr4d | ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) ) |