Metamath Proof Explorer


Theorem clnbgrlevtx

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 𝑈 ) ) ≤ ( ♯ ‘ 𝑉 )

Proof

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 𝑈 ) ) ≤ ( ♯ ‘ 𝑉 )