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

Metamath Proof Explorer

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 ) )