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

Metamath Proof Explorer

Theorem nbgrcl

Description: If a class X has at least one neighbor, this class must be a vertex. (Contributed by AV, 6-Jun-2021) (Revised by AV, 12-Feb-2022)

Ref Expression
Hypothesis nbgrcl.v 
|- V = ( Vtx ` G )
Assertion nbgrcl 
|- ( N e. ( G NeighbVtx X ) -> X e. V )

Proof

Step Hyp Ref Expression
1 nbgrcl.v 
 |-  V = ( Vtx ` G )
2 df-nbgr 
 |-  NeighbVtx = ( g e. _V , v e. ( Vtx ` g ) |-> { n e. ( ( Vtx ` g ) \ { v } ) | E. e e. ( Edg ` g ) { v , n } C_ e } )
3 2 mpoxeldm 
 |-  ( N e. ( G NeighbVtx X ) -> ( G e. _V /\ X e. [_ G / g ]_ ( Vtx ` g ) ) )
4 csbfv 
 |-  [_ G / g ]_ ( Vtx ` g ) = ( Vtx ` G )
5 4 1 eqtr4i 
 |-  [_ G / g ]_ ( Vtx ` g ) = V
6 5 eleq2i 
 |-  ( X e. [_ G / g ]_ ( Vtx ` g ) <-> X e. V )
7 6 biimpi 
 |-  ( X e. [_ G / g ]_ ( Vtx ` g ) -> X e. V )
8 3 7 simpl2im 
 |-  ( N e. ( G NeighbVtx X ) -> X e. V )