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 ∈ USGraph ∧ N ∈ V → e ∈ E | N ∈ e ≤ V

Proof

Step Hyp Ref Expression
1 usgredgleord.v ⊢ V = Vtx ⁡ G
2 usgredgleord.e ⊢ E = Edg ⁡ G
3 usgruspgr ⊢ G ∈ USGraph → G ∈ USHGraph
4 1 2 uspgredgleord ⊢ G ∈ USHGraph ∧ N ∈ V → e ∈ E | N ∈ e ≤ V
5 3 4 sylan ⊢ G ∈ USGraph ∧ N ∈ V → e ∈ E | N ∈ e ≤ V