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=\mathrm{Vtx}\left(G\right)$$
	usgredgleord.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
Assertion	usgredgleord	$$⊢\left(G\in \mathrm{USGraph}\wedge N\in V\right)\to \left|\left\{e\in E|N\in e\right\}\right|\le \left|V\right|$$

Proof

Step	Hyp	Ref	Expression
1		usgredgleord.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		usgredgleord.e	$$⊢E=\mathrm{Edg}\left(G\right)$$
3		usgruspgr	$$⊢G\in \mathrm{USGraph}\to G\in \mathrm{USHGraph}$$
4	1 2	uspgredgleord	$$⊢\left(G\in \mathrm{USHGraph}\wedge N\in V\right)\to \left|\left\{e\in E|N\in e\right\}\right|\le \left|V\right|$$
5	3 4	sylan	$$⊢\left(G\in \mathrm{USGraph}\wedge N\in V\right)\to \left|\left\{e\in E|N\in e\right\}\right|\le \left|V\right|$$