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