Theorem usgredgleord

Description: In a simple graph the number of edges which contain a given vertex is not greater than the number of vertices. (Contributed by Alexander van der Vekens, 4-Jan-2018) (Revised by AV, 18-Oct-2020) (Proof shortened by AV, 6-Dec-2020)

	Ref	Expression
Hypotheses	usgredgleord.v	|- V = ( Vtx ` G )
	usgredgleord.e	|- E = ( Edg ` G )
Assertion	usgredgleord	|- ( ( G e. USGraph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( # ` V ) )

Proof

Step	Hyp	Ref	Expression
1		usgredgleord.v	|- V = ( Vtx ` G )
2		usgredgleord.e	|- E = ( Edg ` G )
3		usgruspgr	|- ( G e. USGraph -> G e. USPGraph )
4	1 2	uspgredgleord	|- ( ( G e. USPGraph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( # ` V ) )
5	3 4	sylan	|- ( ( G e. USGraph /\ N e. V ) -> ( # ` { e e. E | N e. e } ) <_ ( # ` V ) )