Metamath Proof Explorer

Theorem clnbgr0vtx

Description: In a null graph (with no vertices), all closed neighborhoods are empty. (Contributed by AV, 15-Nov-2020)

Ref Expression
Assertion clnbgr0vtx 
|- ( ( Vtx ` G ) = (/) -> ( G ClNeighbVtx K ) = (/) )

Proof

Step Hyp Ref Expression
1 nel02 
 |-  ( ( Vtx ` G ) = (/) -> -. K e. ( Vtx ` G ) )
2 df-nel 
 |-  ( K e/ ( Vtx ` G ) <-> -. K e. ( Vtx ` G ) )
3 1 2 sylibr 
 |-  ( ( Vtx ` G ) = (/) -> K e/ ( Vtx ` G ) )
4 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 4 clnbgrnvtx0 
 |-  ( K e/ ( Vtx ` G ) -> ( G ClNeighbVtx K ) = (/) )
6 3 5 syl 
 |-  ( ( Vtx ` G ) = (/) -> ( G ClNeighbVtx K ) = (/) )