This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. USGraph /\ U e. 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 e. USGraph /\ U e. V ) -> ( # ` ( G NeighbVtx U ) ) = ( # ` { e e. ( Edg ` G ) | U e. e } ) )
4 eqid 
 |-  ( VtxDeg ` G ) = ( VtxDeg ` G )
5 1 2 4 vtxdusgrfvedg 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( ( VtxDeg ` G ) ` U ) = ( # ` { e e. ( Edg ` G ) | U e. e } ) )
6 3 5 eqtr4d 
 |-  ( ( G e. USGraph /\ U e. V ) -> ( # ` ( G NeighbVtx U ) ) = ( ( VtxDeg ` G ) ` U ) )