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 e. _V
3 1 clnbgrssvtx 
 |-  ( G ClNeighbVtx U ) C_ V
4 hashss 
 |-  ( ( V e. _V /\ ( G ClNeighbVtx U ) C_ V ) -> ( # ` ( G ClNeighbVtx U ) ) <_ ( # ` V ) )
5 2 3 4 mp2an 
 |-  ( # ` ( G ClNeighbVtx U ) ) <_ ( # ` V )