Metamath Proof Explorer

Theorem hashnbusgrnn0

Description: The number of neighbors of a vertex in a finite simple graph is a nonnegative integer. (Contributed by Alexander van der Vekens, 14-Jul-2018) (Revised by AV, 15-Dec-2020)

Ref Expression
Hypothesis hashnbusgrnn0.v ⊢ V = Vtx ⁡ G
Assertion hashnbusgrnn0 ⊢ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U ∈ ℕ 0

Proof

Step Hyp Ref Expression
1 hashnbusgrnn0.v ⊢ V = Vtx ⁡ G
2 1 eleq2i ⊢ U ∈ V ↔ U ∈ Vtx ⁡ G
3 nbfiusgrfi ⊢ G ∈ FinUSGraph ∧ U ∈ Vtx ⁡ G → G NeighbVtx U ∈ Fin
4 2 3 sylan2b ⊢ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U ∈ Fin
5 hashcl ⊢ G NeighbVtx U ∈ Fin → G NeighbVtx U ∈ ℕ 0
6 4 5 syl ⊢ G ∈ FinUSGraph ∧ U ∈ V → G NeighbVtx U ∈ ℕ 0