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=\mathrm{Vtx}\left(G\right)$$
Assertion	clnbgrlevtx	Could not format assertion : No typesetting found for |- ( # ` ( G ClNeighbVtx U ) ) <_ ( # ` V ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		clnbgrlevtx.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2	1	fvexi	$$⊢V\in \mathrm{V}$$
3	1	clnbgrssvtx	Could not format ( G ClNeighbVtx U ) C_ V : No typesetting found for |- ( G ClNeighbVtx U ) C_ V with typecode |-
4		hashss	Could not format ( ( V e. _V /\ ( G ClNeighbVtx U ) C_ V ) -> ( # ` ( G ClNeighbVtx U ) ) <_ ( # ` V ) ) : No typesetting found for |- ( ( V e. _V /\ ( G ClNeighbVtx U ) C_ V ) -> ( # ` ( G ClNeighbVtx U ) ) <_ ( # ` V ) ) with typecode |-
5	2 3 4	mp2an	Could not format ( # ` ( G ClNeighbVtx U ) ) <_ ( # ` V ) : No typesetting found for |- ( # ` ( G ClNeighbVtx U ) ) <_ ( # ` V ) with typecode |-