Metamath Proof Explorer

Theorem clnbgrn0

Description: The closed neighborhood of a vertex is never empty. (Contributed by AV, 16-May-2025)

Ref Expression
Hypothesis clnbgrn0.v 
|- V = ( Vtx ` G )
Assertion clnbgrn0 
|- ( N e. V -> ( G ClNeighbVtx N ) =/= (/) )

Proof

Step Hyp Ref Expression
1 clnbgrn0.v 
 |-  V = ( Vtx ` G )
2 1 clnbgrvtxel 
 |-  ( N e. V -> N e. ( G ClNeighbVtx N ) )
3 ne0i 
 |-  ( N e. ( G ClNeighbVtx N ) -> ( G ClNeighbVtx N ) =/= (/) )
4 2 3 syl 
 |-  ( N e. V -> ( G ClNeighbVtx N ) =/= (/) )