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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion	hashnbusgrvd	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) = ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑈 ) )

Proof

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 ‘ 𝐺 ) ‘ 𝑈 ) )