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

Metamath Proof Explorer

Theorem nbcplgr

Description: In a complete graph, each vertex has all other vertices as neighbors. (Contributed by Alexander van der Vekens, 12-Oct-2017) (Revised by AV, 3-Nov-2020)

Ref Expression
Hypothesis nbcplgr.v 
|- V = ( Vtx ` G )
Assertion nbcplgr 
|- ( ( G e. ComplGraph /\ N e. V ) -> ( G NeighbVtx N ) = ( V \ { N } ) )

Proof

Step Hyp Ref Expression
1 nbcplgr.v 
 |-  V = ( Vtx ` G )
2 1 cplgruvtxb 
 |-  ( G e. ComplGraph -> ( G e. ComplGraph <-> ( UnivVtx ` G ) = V ) )
3 2 ibi 
 |-  ( G e. ComplGraph -> ( UnivVtx ` G ) = V )
4 3 eqcomd 
 |-  ( G e. ComplGraph -> V = ( UnivVtx ` G ) )
5 4 eleq2d 
 |-  ( G e. ComplGraph -> ( N e. V <-> N e. ( UnivVtx ` G ) ) )
6 5 biimpa 
 |-  ( ( G e. ComplGraph /\ N e. V ) -> N e. ( UnivVtx ` G ) )
7 1 uvtxnbgrb 
 |-  ( N e. V -> ( N e. ( UnivVtx ` G ) <-> ( G NeighbVtx N ) = ( V \ { N } ) ) )
8 7 adantl 
 |-  ( ( G e. ComplGraph /\ N e. V ) -> ( N e. ( UnivVtx ` G ) <-> ( G NeighbVtx N ) = ( V \ { N } ) ) )
9 6 8 mpbid 
 |-  ( ( G e. ComplGraph /\ N e. V ) -> ( G NeighbVtx N ) = ( V \ { N } ) )