This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nbgrnvtx0

Description: If a class X is not a vertex of a graph G , then it has no neighbors in G . (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 26-Oct-2020)

Ref Expression
Hypothesis nbgrel.v 
|- V = ( Vtx ` G )
Assertion nbgrnvtx0 
|- ( X e/ V -> ( G NeighbVtx X ) = (/) )

Proof

Step Hyp Ref Expression
1 nbgrel.v 
 |-  V = ( Vtx ` G )
2 csbfv 
 |-  [_ G / g ]_ ( Vtx ` g ) = ( Vtx ` G )
3 1 2 eqtr4i 
 |-  V = [_ G / g ]_ ( Vtx ` g )
4 neleq2 
 |-  ( V = [_ G / g ]_ ( Vtx ` g ) -> ( X e/ V <-> X e/ [_ G / g ]_ ( Vtx ` g ) ) )
5 3 4 ax-mp 
 |-  ( X e/ V <-> X e/ [_ G / g ]_ ( Vtx ` g ) )
6 5 biimpi 
 |-  ( X e/ V -> X e/ [_ G / g ]_ ( Vtx ` g ) )
7 6 olcd 
 |-  ( X e/ V -> ( G e/ _V \/ X e/ [_ G / g ]_ ( Vtx ` g ) ) )
8 df-nbgr 
 |-  NeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> { n e. ( ( Vtx ` g ) \ { v } ) | E. e e. ( Edg ` g ) { v , n } C_ e } )
9 8 mpoxneldm 
 |-  ( ( G e/ _V \/ X e/ [_ G / g ]_ ( Vtx ` g ) ) -> ( G NeighbVtx X ) = (/) )
10 7 9 syl 
 |-  ( X e/ V -> ( G NeighbVtx X ) = (/) )