Theorem nbedgusgr

Description: The number of neighbors of a vertex is the number of edges at the vertex in a simple graph. (Contributed by AV, 27-Dec-2020) (Proof shortened by AV, 5-May-2021)

	Ref	Expression
Hypotheses	nbusgrf1o.v	|- V = ( Vtx ` G )
	nbusgrf1o.e	|- E = ( Edg ` G )
Assertion	nbedgusgr	|- ( ( G e. USGraph /\ U e. V ) -> ( # ` ( G NeighbVtx U ) ) = ( # ` { e e. E | U e. e } ) )

Proof

Step	Hyp	Ref	Expression
1		nbusgrf1o.v	|- V = ( Vtx ` G )
2		nbusgrf1o.e	|- E = ( Edg ` G )
3		ovex	|- ( G NeighbVtx U ) e. _V
4	1 2	nbusgrf1o	|- ( ( G e. USGraph /\ U e. V ) -> E. f f : ( G NeighbVtx U ) -1-1-onto-> { e e. E | U e. e } )
5		hasheqf1oi	|- ( ( G NeighbVtx U ) e. _V -> ( E. f f : ( G NeighbVtx U ) -1-1-onto-> { e e. E | U e. e } -> ( # ` ( G NeighbVtx U ) ) = ( # ` { e e. E | U e. e } ) ) )
6	3 4 5	mpsyl	|- ( ( G e. USGraph /\ U e. V ) -> ( # ` ( G NeighbVtx U ) ) = ( # ` { e e. E | U e. e } ) )