Theorem uvtxnbgrb

Description: A vertex is universal iff all the other vertices are its neighbors. (Contributed by Alexander van der Vekens, 13-Jul-2018) (Revised by AV, 3-Nov-2020) (Revised by AV, 23-Mar-2021) (Proof shortened by AV, 14-Feb-2022)

	Ref	Expression
Hypothesis	uvtxnbgr.v	|- V = ( Vtx ` G )
Assertion	uvtxnbgrb	|- ( N e. V -> ( N e. ( UnivVtx ` G ) <-> ( G NeighbVtx N ) = ( V \ { N } ) ) )

Proof

Step	Hyp	Ref	Expression
1		uvtxnbgr.v	|- V = ( Vtx ` G )
2	1	uvtxnbgr	|- ( N e. ( UnivVtx ` G ) -> ( G NeighbVtx N ) = ( V \ { N } ) )
3		simpl	|- ( ( N e. V /\ ( G NeighbVtx N ) = ( V \ { N } ) ) -> N e. V )
4		raleleq	|- ( ( V \ { N } ) = ( G NeighbVtx N ) -> A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) )
5	4	eqcoms	|- ( ( G NeighbVtx N ) = ( V \ { N } ) -> A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) )
6	5	adantl	|- ( ( N e. V /\ ( G NeighbVtx N ) = ( V \ { N } ) ) -> A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) )
7	1	uvtxel	|- ( N e. ( UnivVtx ` G ) <-> ( N e. V /\ A. n e. ( V \ { N } ) n e. ( G NeighbVtx N ) ) )
8	3 6 7	sylanbrc	|- ( ( N e. V /\ ( G NeighbVtx N ) = ( V \ { N } ) ) -> N e. ( UnivVtx ` G ) )
9	8	ex	|- ( N e. V -> ( ( G NeighbVtx N ) = ( V \ { N } ) -> N e. ( UnivVtx ` G ) ) )
10	2 9	impbid2	|- ( N e. V -> ( N e. ( UnivVtx ` G ) <-> ( G NeighbVtx N ) = ( V \ { N } ) ) )