Description: The size of the closed neighborhood of a vertex is at most the number of vertices of a graph. (Contributed by AV, 10-May-2025)
Ref | Expression | ||
---|---|---|---|
Hypothesis | clnbgrlevtx.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
Assertion | clnbgrlevtx | ⊢ ( ♯ ‘ ( 𝐺 ClNeighbVtx 𝑈 ) ) ≤ ( ♯ ‘ 𝑉 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | clnbgrlevtx.v | ⊢ 𝑉 = ( Vtx ‘ 𝐺 ) | |
2 | 1 | fvexi | ⊢ 𝑉 ∈ V |
3 | 1 | clnbgrssvtx | ⊢ ( 𝐺 ClNeighbVtx 𝑈 ) ⊆ 𝑉 |
4 | hashss | ⊢ ( ( 𝑉 ∈ V ∧ ( 𝐺 ClNeighbVtx 𝑈 ) ⊆ 𝑉 ) → ( ♯ ‘ ( 𝐺 ClNeighbVtx 𝑈 ) ) ≤ ( ♯ ‘ 𝑉 ) ) | |
5 | 2 3 4 | mp2an | ⊢ ( ♯ ‘ ( 𝐺 ClNeighbVtx 𝑈 ) ) ≤ ( ♯ ‘ 𝑉 ) |