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 | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| Assertion | hashnbusgrnn0 | ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) ∈ ℕ0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | hashnbusgrnn0.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
| 2 | 1 | eleq2i | ⊢ ( 𝑈 ∈ 𝑉 ↔ 𝑈 ∈ ( Vtx ‘ 𝐺 ) ) |
| 3 | nbfiusgrfi | ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ ( Vtx ‘ 𝐺 ) ) → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ) | |
| 4 | 2 3 | sylan2b | ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin ) |
| 5 | hashcl | ⊢ ( ( 𝐺 NeighbVtx 𝑈 ) ∈ Fin → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) ∈ ℕ0 ) | |
| 6 | 4 5 | syl | ⊢ ( ( 𝐺 ∈ FinUSGraph ∧ 𝑈 ∈ 𝑉 ) → ( ♯ ‘ ( 𝐺 NeighbVtx 𝑈 ) ) ∈ ℕ0 ) |