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	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
	usgredgleord.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
Assertion	usgredgleord	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ) ≤ ( ♯ ‘ 𝑉 ) )

Proof

Step	Hyp	Ref	Expression
1		usgredgleord.v	⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2		usgredgleord.e	⊢ 𝐸 = ( Edg ‘ 𝐺 )
3		usgruspgr	⊢ ( 𝐺 ∈ USGraph → 𝐺 ∈ USPGraph )
4	1 2	uspgredgleord	⊢ ( ( 𝐺 ∈ USPGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ) ≤ ( ♯ ‘ 𝑉 ) )
5	3 4	sylan	⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑁 ∈ 𝑉 ) → ( ♯ ‘ { 𝑒 ∈ 𝐸 ∣ 𝑁 ∈ 𝑒 } ) ≤ ( ♯ ‘ 𝑉 ) )