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 V = Vtx G
Assertion clnbgrlevtx G ClNeighbVtx U V

Proof

Step Hyp Ref Expression
1 clnbgrlevtx.v V = Vtx G
2 1 fvexi V V
3 1 clnbgrssvtx G ClNeighbVtx U V
4 hashss V V G ClNeighbVtx U V G ClNeighbVtx U V
5 2 3 4 mp2an G ClNeighbVtx U V