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 } ) )